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

Popular repositories Loading

  1. exploring-robust-property-preservation exploring-robust-property-preservation Public

    Coq development for "Journey Beyond Full Abstraction" paper

    Coq 8

  2. SECOMP SECOMP Public

    Forked from AbsInt/CompCert

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

    Coq 8 2

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

    Coq formalization for "When Good Components Go Bad" paper

    Coq 7 1

  4. beyond-good-and-evil beyond-good-and-evil Public

    Auxiliary materials for "Beyond Good and Evil" paper

    Coq 3

  5. SecurePtrs SecurePtrs Public

    Coq formalization for "SecurePtrs" paper

    Coq 3

  6. different_traces different_traces Public

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

    Coq 2

Repositories

Showing 9 of 9 repositories
  • when-good-components-go-bad Public

    Coq formalization for "When Good Components Go Bad" paper

    Coq 7 Apache-2.0 1 1 1 Updated Apr 15, 2025
  • nanopass-bt Public

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

    Coq 0 0 0 0 Updated Apr 11, 2025
  • SECOMP Public Forked from AbsInt/CompCert

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

    Coq 8 283 5 2 Updated Jan 13, 2025
  • secure-compilation.github.io Public

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

    HTML 1 0 0 0 Updated Dec 27, 2024
  • exploring-robust-property-preservation Public

    Coq development for "Journey Beyond Full Abstraction" paper

    Coq 8 Apache-2.0 0 0 0 Updated Aug 26, 2022
  • SecurePtrs Public

    Coq formalization for "SecurePtrs" paper

    Coq 3 Apache-2.0 0 0 0 Updated Jun 3, 2022
  • different_traces Public

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

    Coq 2 Apache-2.0 0 0 0 Updated Aug 4, 2020
  • ds-2018 Public

    Materials of Dagstuhl Seminar 18201 on Secure Compilation (May 13-18, 2018)

    0 0 0 0 Updated Nov 9, 2018
  • beyond-good-and-evil Public

    Auxiliary materials for "Beyond Good and Evil" paper

    Coq 3 Apache-2.0 0 2 0 Updated Feb 16, 2018

Top languages

Coq HTML