Accession Number : AD1015496


Title :   End-to-End Verification of Information-Flow Security for C and Assembly Programs


Descriptive Note : Technical Report


Corporate Author : YALE UNIV NEW HAVEN CT NEW HAVEN United States


Personal Author(s) : Costanzo,David ; Shao,Zhong ; Gu,Ronghui


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/1015496.pdf


Report Date : 01 Apr 2016


Pagination or Media Count : 21


Abstract : Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing todays 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 todays 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.


Descriptors :   Semantics , computer program verification , information assurance , computer security software , assemblers (computer programs)


Subject Categories : Computer Programming and Software
      Computer Systems Management and Standards


Distribution Statement : APPROVED FOR PUBLIC RELEASE