Supplementary material for Exploring Robust Property Preservation for Secure Compilation
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
Alternative2FR.v RrelationalP expressed in terms of families of (hyper)properties Nov 9, 2018
ClassicalExtras.v
CommonST.v
Criteria.v
Events.v
LICENSE
Makefile start polishing, topology and program components as Records May 30, 2018
Properties.v Add a small header to each coq file that describes what it does Nov 1, 2018
README.md
Robustdef.v
SemanticsSafetyLike.v
TEP.txt
TechnicalLemmas.v Add a small header to each coq file that describes what it does Nov 1, 2018
Topology.v Add a small header to each coq file that describes what it does Nov 1, 2018
TopologyTrace.v coq proof for thm 33 Oct 5, 2018
TraceModel.v
_CoqProject
appendix.pdf
nd_ctxs.v
r2RSC_teq.v Add a small header to each coq file that describes what it does Nov 1, 2018
reflection.v
separation-results.txt Ill-typed source contexts have to be rejected statically Nov 1, 2018
separation.v
tep_teq.v

README.md

Exploring Robust Property Preservation for Secure Compilation

This repository contains the supplementary materials of the paper:

Entry points

The best entry points into this work are the paper above followed by the online appendix in this repo, which includes direct pointers to various Coq and text files.

Prerequisites for the Coq proofs

The Coq development is known to work with Coq v8.7.X, but it has very few dependencies, so it will likely work with other versions as well.

Replaying the Coq proofs

$ make -j4

License

  • The Coq development in this repository is licensed under the Apache License, Version 2.0 (see LICENSE)
  • The PDF and text documents in this repository are licensed under the Creative Commons Attribution 4.0 International License (CC BY 4.0)