Skip to main content

A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow

Author(s): Amtoft, T; Dodds, J; Zhang, Z; Appel, Andrew W.; Beringer, L; et al

To refer to this page use:
Abstract: In previous work, we have proposed a compositional framework for stating and automatically verifying complex conditional information flow policies using a relational Hoare logic. The framework allows developers and verifiers to work directly with the source code using source-level code contracts. In this work, we extend that approach so that the algorithm for verifying code compliance to an information flow contract emits formal certificates of correctness that are checked in the Coq proof assistant. This framework is implemented in the context of SPARK - a subset of Ada that has been used in a number of industrial contexts for implementing certified safety and security critical systems.
Publication Date: 2012
Citation: Amtoft, T, Dodds, J, Zhang, Z, Appel, A. "Certificate Infrastructure for MachineChecked Proofs of Conditional Information Flow" Principles of Security And Trust, Lecture Notes in Computer Science, 7215, 369 - 389, doi:10.1007/978-3-642-28641-4_20
DOI: doi:10.1007/978-3-642-28641-4_20
Pages: 369 - 389
Type of Material: Conference Article
Series/Report no.: Lecture Notes in Computer Science;
Journal/Proceeding Title: Principles of Security And Trust
Version: This is the author’s final manuscript. All rights reserved to author(s).

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