Abstract | ||
---|---|---|
Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is to formally verify that the end-to-end behavior of the computing system really satisfies various information-flow policies. Unfortunately, because today's system software still consists of both C and assembly programs, the end-to-end verification necessarily requires that we not only prove the security properties of individual components, but also carefully preserve these properties through compilation and cross-language linking. In this paper, we present a novel methodology for formally verifying end-to-end security of a software system that consists of both C and assembly programs. We introduce a general definition of observation function that unifies the concepts of policy specification, state indistinguishability, and whole-execution behaviors. We show how to use different observation functions for different levels of abstraction, and how to link different security proofs across abstraction levels using a special kind of simulation that is guaranteed to preserve state indistinguishability. To demonstrate the effectiveness of our new methodology, we have successfully constructed an end-to-end security proof, fully formalized in the Coq proof assistant, of a nontrivial operating system kernel (running on an extended CompCert x86 assembly machine model). Some parts of the kernel are written in C and some are written in assembly; we verify all of the code, regardless of language. |
Year | DOI | Venue |
---|---|---|
2016 | 10.1145/2908080.2908100 | PLDI |
Keywords | Field | DocType |
Verification,Security,Reliability,Languages,Design,Information Flow Control,Security Policy Specification,Security-Preserving Simulation,Program Verification,Certified OS Kernels | System software,x86,Information flow (information theory),Information assurance,Programming language,Computer science,Software system,Theoretical computer science,Mathematical proof,Computer security model,Proof assistant | Conference |
Volume | Issue | ISSN |
51 | 6 | 0362-1340 |
Citations | PageRank | References |
8 | 0.46 | 16 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
David Costanzo | 1 | 66 | 3.89 |
Zhong Shao | 2 | 897 | 68.80 |
Ronghui Gu | 3 | 64 | 7.82 |