Skip to content
@secure-compilation

secure-compilation

SECOMP: Efficient Formally Secure Compilers to a Tagged Architecture https://secure-compilation.github.io and https://secure-compilation.zulipchat.com/register

Pinned Loading

  1. SECOMP SECOMP Public

    Forked from AbsInt/CompCert

    SECOMP formally secure compiler for compartmentalized C programs (based on CompCert)

    Rocq Prover 12 4

  2. when-good-components-go-bad when-good-components-go-bad Public

    Coq formalization for "When Good Components Go Bad" paper, with various later extensions

    Coq 8 1

  3. fslh-rocq fslh-rocq Public

    FSLH: Flexible Mechanized Speculative Load Hardening

    Coq 3

Repositories

Showing 10 of 12 repositories
  • SECOMP Public Forked from AbsInt/CompCert

    SECOMP formally secure compiler for compartmentalized C programs (based on CompCert)

    secure-compilation/SECOMP's past year of commit activity
    Rocq Prover 12 312 6 2 Updated Jun 16, 2026
  • Triosecuris Public

    Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking

    secure-compilation/Triosecuris's past year of commit activity
    Rocq Prover 3 1 0 0 Updated Apr 14, 2026
  • exploring-robust-property-preservation Public

    Coq development for "Journey Beyond Full Abstraction" paper

    secure-compilation/exploring-robust-property-preservation's past year of commit activity
    Rocq Prover 10 Apache-2.0 0 0 0 Updated Mar 22, 2026
  • secure-compilation.github.io Public

    Code for SECOMP project website: https://secure-compilation.github.io

    secure-compilation/secure-compilation.github.io's past year of commit activity
    HTML 1 0 0 0 Updated Dec 13, 2025
  • nanopass-bt Public

    Rocq development for the paper Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs

    secure-compilation/nanopass-bt's past year of commit activity
    Rocq Prover 0 0 0 0 Updated Sep 22, 2025
  • comparing_speculative_semantics_rocq Public
    secure-compilation/comparing_speculative_semantics_rocq's past year of commit activity
    Rocq Prover 0 0 0 0 Updated Aug 21, 2025
  • when-good-components-go-bad Public

    Coq formalization for "When Good Components Go Bad" paper, with various later extensions

    secure-compilation/when-good-components-go-bad's past year of commit activity
    Coq 8 Apache-2.0 1 1 1 Updated Aug 11, 2025
  • fslh-rocq Public

    FSLH: Flexible Mechanized Speculative Load Hardening

    secure-compilation/fslh-rocq's past year of commit activity
    Coq 3 0 0 0 Updated May 16, 2025
  • different_traces Public

    The Coq development for "Trace-Relating Compiler Correctness and Secure Compilation" paper

    secure-compilation/different_traces's past year of commit activity
    Coq 2 Apache-2.0 0 0 0 Updated May 8, 2025
  • SecurePtrs Public

    Coq formalization for "SecurePtrs" paper

    secure-compilation/SecurePtrs's past year of commit activity
    Coq 3 Apache-2.0 0 0 0 Updated Jun 3, 2022
View all repositories