Skip to main content

Modular Verification for Computer Security

Author(s): Appel, Andrew W

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr11z4b
Full metadata record
DC FieldValueLanguage
dc.contributor.authorAppel, Andrew W-
dc.date.accessioned2021-10-08T19:44:35Z-
dc.date.available2021-10-08T19:44:35Z-
dc.date.issued2016en_US
dc.identifier.citationAppel, Andrew W. "Modular Verification for Computer Security." In 2016 IEEE 29th Computer Security Foundations Symposium (CSF), (2018): pp. 1-8. doi: 10.1109/CSF.2016.8en_US
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr11z4b-
dc.description.abstractFor 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.en_US
dc.format.extent1 - 8en_US
dc.language.isoen_USen_US
dc.relation.ispartof2016 IEEE 29th Computer Security Foundations Symposium (CSF)en_US
dc.rightsAuthor's manuscripten_US
dc.titleModular Verification for Computer Securityen_US
dc.typeConference Articleen_US
dc.identifier.doidoi:10.1109/CSF.2016.8-
dc.identifier.eissn2374-8303-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
Modular+Verification+for+Computer+Security.pdf728.66 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.