Dissertation Title: Formal End-to-End Verification of Information-Flow Security
for Complex Systems
[Dissertation PDF]
Coq proofs (known to compile without error using Coq v8.4pl3):
Behavior-Preserving Separation Logic (Chapter 2):
[concrete logic]
[HTML]
[HTML, no proofs]
[PDF]
[PDF, no proofs]
[abstract logic]
[HTML]
[HTML, no proofs]
[PDF]
[PDF, no proofs]
Security-Aware Separation Logic (Chapter 3):
[Coq file]
[HTML]
[HTML, no proofs]
[PDF]
[PDF, no proofs]
mCertiKOS-secure (Chapters 4-7):
[Browsable HTML]
mCertiKOS-secure with virtualized time (Chapter 8):
[Browsable HTML]
(the above two links sometimes don't work; just keep trying until they do)
Defense date: August 17, 2016 @ 3:30pm EDT