@inproceedings{a45a71ce6a7444bfa7f5f18c85f71f1d,
title = "Modular verification for computer security",
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.",
author = "Appel, {Andrew W.}",
note = "Publisher Copyright: {\textcopyright} 2016 IEEE.; 29th IEEE Computer Security Foundations Symposium, CSF 2016 ; Conference date: 27-06-2016 Through 01-07-2016",
year = "2016",
month = aug,
day = "8",
doi = "10.1109/CSF.2016.8",
language = "English (US)",
series = "Proceedings - IEEE Computer Security Foundations Symposium",
publisher = "IEEE Computer Society",
booktitle = "Proceedings - IEEE 29th Computer Security Foundations Symposium, CSF 2016",
address = "United States",
}