A certificate infrastructure for machine-checked proofs of conditional information flow

Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew Appel, Lennart Beringer, John Hatcliff, Xinming Ou, Andrew Cousino

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationPrinciples of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings
Pages369-389
Number of pages21
DOIs
StatePublished - Apr 9 2012
Event1st International Conference on Principles of Security and Trust, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 - Tallinn, Estonia
Duration: Mar 24 2012Apr 1 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7215 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st International Conference on Principles of Security and Trust, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
CountryEstonia
CityTallinn
Period3/24/124/1/12

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A certificate infrastructure for machine-checked proofs of conditional information flow'. Together they form a unique fingerprint.

Cite this