This web page contains artifacts associated with the POST submission:
A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow by Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew Appel, Lennart Beringer, John Hatcliff, Xinming Ou, Andrew Cousino.
- Detail description of evidence and correctness proofs: (.pdf)
- Coq representation of evidence and proof of correctness: .html
- Example procedures with evidence output: .html