When Good Components Go Bad

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.

Prerequisites

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

Replaying the proofs

$ make -j4

Running the tests

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.

Top-level theorems

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 in RSC_DC_MD_Sigs.v (Section 3.5)
• RSC_DC_MD_Instance.v: an instantiation of the assumptions from RSC_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 in RSC_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 model
• RSC_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) and RSC_DC.Z_p_equivalent (proof of equivalence between the proof-friendly and the paper definitions) in the simple trace model
• RSC_DC_4_compcert.Z_class (proof-friendly definition) and RSC_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 model
• RSC_DC_4_compcert.main_thm in the CompCert trace model

License

• 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 the common and lib 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 (see Compcert/LICENSE)