Skip to content

akramelkorashy/when-good-components-go-bad

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

When Good Components Go Bad

This repository contains the Coq development of the paper:

Prerequisites

This development requires Coq v8.7.1 to work, as well as the following libraries:

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)

About

Coq formalization for "When Good Components Go Bad" paper

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Coq 99.2%
  • Other 0.8%