Modular verification for computer security

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations


For many software components, it is useful and important to verify their security. This can be done by an analysis of the software itself, or by isolating the software behind a protection mechanism such as an operating system kernel (virtual-memory protection) or cryptographic authentication (don't accepted untrusted inputs). But the protection mechanisms themselves must then be verified not just for safety but for functional correctness. Several recent projects have demonstrated that formal, deductive functional-correctness verification is now possible for kernels, crypto, and compilers. Here I explain some of the modularity principles that make these verifications possible.

Original languageEnglish (US)
Title of host publicationProceedings - IEEE 29th Computer Security Foundations Symposium, CSF 2016
PublisherIEEE Computer Society
ISBN (Electronic)9781509026074
StatePublished - Aug 8 2016
Event29th IEEE Computer Security Foundations Symposium, CSF 2016 - Lisbon, Portugal
Duration: Jun 27 2016Jul 1 2016

Publication series

NameProceedings - IEEE Computer Security Foundations Symposium
ISSN (Print)1940-1434


Other29th IEEE Computer Security Foundations Symposium, CSF 2016

All Science Journal Classification (ASJC) codes

  • General Engineering


Dive into the research topics of 'Modular verification for computer security'. Together they form a unique fingerprint.

Cite this