Paper Info
Title
A certificate infrastructure for machine-checked proofs of conditional information flow
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.
Year
DOI
Venue
2012
10.1007/978-3-642-28641-4_20
POST
Keywords
Field
DocType
verifying code compliance,certificate infrastructure,certified safety,information flow contract,source code,compositional framework,formal certificate,previous work,coq proof assistant,complex conditional information flow,machine-checked proof,source-level code contract
Information flow (information theory),Programming language,Computer science,Source code,Hoare logic,Design by contract,Correctness,Theoretical computer science,Mathematical proof,Proof assistant,Certificate
Conference
Volume
ISSN
Citations 
7215
0302-9743
14
PageRank 
References 
Authors
0.58
26
8
Name
Order
Citations
PageRank
Torben Amtoft136429.25
Josiah Dodds2171.29
Zhi Zhang3141.26
Andrew W. Appel42599292.71
Lennart Beringer524019.14
John Hatcliff62373212.83
Xinming Ou7108155.30
Andrew Cousino8140.58