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. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Amtoft, T., Dodds, J., Zhang, Z., Appel, A., Beringer, L., Hatcliff, J., … Cousino, A. (2012). A certificate infrastructure for machine-checked proofs of conditional information flow. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7215 LNCS, pp. 369–389). https://doi.org/10.1007/978-3-642-28641-4_20
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
