Many security problems today stem from bugs in software. Although there has been significant effort in reducing bugs through better testing, fuzzing, model checking, and so on, subtle bugs remain and continue to be exploited. This proposal explores the use of formal verification to prove security of a file system implementation along with an example application in the form of a mail server. Machine-checked verification is a powerful approach that can eliminate a large class of bugs in software by proving that an implementation meets a precise specification. As long as the specification rules out a certain class of bugs, the machine-checked proof will ensure no such bugs can exist in the implementation. This project develops techniques for proving security of sophisticated applications, such as proving that a mail server will not inappropriately disclose confidential email messages. At the high level, the impact of this work will be a more secure software infrastructure. The key technical challenge that this project focuses on is data confidentiality. The project explores approaches for specifying confidentiality of systems software, including a mail server and a POSIX file system, as well as a framework for implementation and machine-checked verification of confidentiality properties for these applications. The project also develops common infrastructure that such applications depend on, including a formal security specification for a POSIX file system and verified implementations of a mail server and a file system with proofs of security, which will be useful to the broader community. Finally, part of the project involves developing course modules focused on machine-checked proofs of correctness and security for systems software.
SaTC: CORE: Small: verifying security for data non-interference