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