Modular verification for computer security

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

3 Scopus citations

Abstract

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
DOIs
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
Volume2016-August
ISSN (Print)1940-1434

Other

Other29th IEEE Computer Security Foundations Symposium, CSF 2016
CountryPortugal
CityLisbon
Period6/27/167/1/16

All Science Journal Classification (ASJC) codes

  • Engineering(all)

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

  • Cite this

    Appel, A. W. (2016). Modular verification for computer security. In Proceedings - IEEE 29th Computer Security Foundations Symposium, CSF 2016 [7536361] (Proceedings - IEEE Computer Security Foundations Symposium; Vol. 2016-August). IEEE Computer Society. https://doi.org/10.1109/CSF.2016.8