Skip to content

@secure-compilation secure-compilation

All

    Repositories list

    12 repositories

    • Triosecuris

      Public
      Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
      Rocq Prover
      •1•3•0•0•Updated Oct 23, 2026Oct 23, 2026

    • when-good-components-go-bad

      Public
      Coq formalization for "When Good Components Go Bad" paper, with various later extensions
      coqundefined-behaviorcompartmentalization
      coqundefined-behaviorcompartmentalizationsecure-compilationtagged-architecturessoftware-fault-isolation
      Coq
      •
      Apache License 2.0
      •1•8•1•1•Updated Oct 21, 2026Oct 21, 2026

    • SECOMP

      Public
      SECOMP formally secure compiler for compartmentalized C programs (based on CompCert)
      Rocq Prover
      •
      Other
      •268•12•19•9•Updated Sep 29, 2026Sep 29, 2026

    • exploring-robust-property-preservation

      Public
      Coq development for "Journey Beyond Full Abstraction" paper
      Rocq Prover
      •
      Apache License 2.0
      •0•10•0•0•Updated Mar 22, 2026Mar 22, 2026

    • secure-compilation.github.io

      Public
      Code for SECOMP project website: https://secure-compilation.github.io
      HTML
      •0•1•0•0•Updated Dec 13, 2025Dec 13, 2025

    • nanopass-bt

      Public
      Rocq development for the paper Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
      Rocq Prover
      •0•0•0•0•Updated Sep 22, 2025Sep 22, 2025

    • comparing_speculative_semantics_rocq

      Public
      Rocq Prover
      •0•0•0•0•Updated Aug 21, 2025Aug 21, 2025

    • fslh-rocq

      Public
      FSLH: Flexible Mechanized Speculative Load Hardening
      Coq
      •0•3•0•0•Updated May 16, 2025May 16, 2025

    • different_traces

      Public
      The Coq development for "Trace-Relating Compiler Correctness and Secure Compilation" paper
      Coq
      •
      Apache License 2.0
      •0•2•0•0•Updated May 8, 2025May 8, 2025

    • SecurePtrs

      Public
      Coq formalization for "SecurePtrs" paper
      coqcapabilitiescompartmentalization
      coqcapabilitiescompartmentalizationsecure-compilation
      Coq
      •
      Apache License 2.0
      •0•3•0•0•Updated Jun 3, 2022Jun 3, 2022

    • ds-2018

      Public
      Materials of Dagstuhl Seminar 18201 on Secure Compilation (May 13-18, 2018)
      0•0•0•0•Updated Nov 9, 2018Nov 9, 2018

    • beyond-good-and-evil

      Public
      Auxiliary materials for "Beyond Good and Evil" paper
      Coq
      •
      Apache License 2.0
      •0•3•2•0•Updated Feb 16, 2018Feb 16, 2018
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.