This repository contains the Coq development of the paper:
- Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, Andrew Tolmach. When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. In 25th ACM Conference on Computer and Communications Security (CCS 2018), October 2018.
This development requires Coq v8.7.1 to work, as well as the following libraries:
- Mathematical Components 1.6.4
- Extensional Structures 0.1
- CoqUtils 0.1
$ make -j4
Our tests are known to work with QuickChick branch 8.7 and OCaml from 4.02.3 to 4.06.
Running the tests (to be simplified):
$ make clean
$ make -j4
$ ./run_extracted_examples.sh --force-extraction
$ rm sfi_safety_properties.exe
$ ./run_sfi_tests.sh
More thorough mutation tests are on the nora-testing-experiments
branch.
At the top level, the development provides high-level proofs with the following entry points:
RSC_DC_MD.v
: generic secure compilation proof against the assumptions inRSC_DC_MD_Sigs.v
(Section 3.5)RSC_DC_MD_Instance.v
: an instantiation of the assumptions fromRSC_DC_MD_Sigs.v
to our compilation chain (Section 4.3)RSC_DC.v
: general proofs about the class of properties preserved by RSC^DC (Appendix A)RSC_DC_4_compcert.v
: proofs inRSC_DC.v
adapted to the general CompCert trace model (Appendix A)
The correspondences between the main definitions and results in the paper and in Coq are as follows.
Definition 3.2: Robustly Safe Compilation with Dynamic Compromise (RSC^DC)
RSC_DC.RSC_dc
in the simple trace modelRSC_DC_4_compcert.RSC_dc
in the CompCert trace model
Definition 3.3: Robustly Safe Compilation with Dynamic Compromise and Mutual Distrust (RSC^DC_MD)
RSC_DC_MD.RSC_DC_MD
Definition A.1: Z_P class of safety properties preserved by RSC^DC
RSC_DC.Z_class
(proof-friendly definition) andRSC_DC.Z_p_equivalent
(proof of equivalence between the proof-friendly and the paper definitions) in the simple trace modelRSC_DC_4_compcert.Z_class
(proof-friendly definition) andRSC_DC_4_compcert.Z_p_equivalent
(proof of equivalence between the proof-friendly and the paper definitions) in the CompCert trace model
Theorem A.2: RSC^DC characterization via Z_P
RSC_DC.main_thm
in the simple trace modelRSC_DC_4_compcert.main_thm
in the CompCert trace model
- This code is licensed under the Apache License, Version 2.0 (see
LICENSE
) - The code in the
CompCert
dir is adapted based on files in thecommon
andlib
dirs of CompCert and is thus dual-licensed under the INRIA Non-Commercial License Agreement and the GNU General Public License version 2 or later (seeCompcert/LICENSE
)