Auxiliary materials for "Beyond Good and Evil" paper
Coq OCaml Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
sfa-to-scc-coq
simple-instance-coq
trace-mapping-testing
.gitignore
LICENSE
README.md
simple-instance.org

README.md

Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation

This repository contains auxiliary materials for the following paper:

  • Yannis Juglaret, Cătălin Hriţcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. In 29th IEEE Symposium on Computer Security Foundations (CSF), pages 45–60. IEEE Computer Society Press, July 2016. Technical report https://arxiv.org/abs/1602.04503

In particular, these materials include:

  • sfa-to-scc-coq: a Coq proof for Theorem 3.4 showing that Structured Full Abstraction instantiated to components implies Secure Compartmentalizing Compilation (SCC)
  • simple-instance.organd simple-instance-coq: technical details and proofs showing that the simple compiler from Section 4 satisfies SCC (both on paper and in Coq)
  • trace-mapping-testing: a trace mapping algorithm in OCaml using property-based testing to check the Definability assumption from Section 4

The code in this repository is licensed under the Apache License, Version 2.0 (see LICENSE)