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

doi:10.1007/978-3-642-28641-4_20

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 proceeding › Conference contribution

19 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 language	English (US)
Title of host publication	Principles 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
Pages	369-389
Number of pages	21
DOIs	https://doi.org/10.1007/978-3-642-28641-4_20
State	Published - 2012
Externally published	Yes
Event	1st 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 2012 → Apr 1 2012

Publication series

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

Other

Other	1st 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
Country/Territory	Estonia
City	Tallinn
Period	3/24/12 → 4/1/12

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-28641-4_20

Cite this

Amtoft, T., Dodds, J., Zhang, Z., Appel, A., Beringer, L., Hatcliff, J., Ou, X., & Cousino, A. (2012). A certificate infrastructure for machine-checked proofs of conditional information flow. In Principles 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 (pp. 369-389). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7215 LNCS). https://doi.org/10.1007/978-3-642-28641-4_20

Amtoft, Torben ; Dodds, Josiah ; Zhang, Zhi et al. / A certificate infrastructure for machine-checked proofs of conditional information flow. Principles 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. 2012. pp. 369-389 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{557343132b8d4f928600595297b5da92,

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.",

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

year = "2012",

doi = "10.1007/978-3-642-28641-4_20",

language = "English (US)",

isbn = "9783642286407",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "369--389",

booktitle = "Principles 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",

note = "1st 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 ; Conference date: 24-03-2012 Through 01-04-2012",

}

Amtoft, T, Dodds, J, Zhang, Z, Appel, A, Beringer, L, Hatcliff, J, Ou, X & Cousino, A 2012, A certificate infrastructure for machine-checked proofs of conditional information flow. in Principles 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7215 LNCS, pp. 369-389, 1st 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, 3/24/12. https://doi.org/10.1007/978-3-642-28641-4_20

A certificate infrastructure for machine-checked proofs of conditional information flow. / Amtoft, Torben; Dodds, Josiah; Zhang, Zhi et al.
Principles 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. 2012. p. 369-389 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7215 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Amtoft, Torben

AU - Dodds, Josiah

AU - Zhang, Zhi

AU - Appel, Andrew

AU - Beringer, Lennart

AU - Hatcliff, John

AU - Ou, Xinming

AU - Cousino, Andrew

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84859309070&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84859309070&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-28641-4_20

DO - 10.1007/978-3-642-28641-4_20

M3 - Conference contribution

AN - SCOPUS:84859309070

SN - 9783642286407

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 369

EP - 389

BT - Principles 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

T2 - 1st 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

Y2 - 24 March 2012 through 1 April 2012

ER -

Amtoft T, Dodds J, Zhang Z, Appel A, Beringer L, Hatcliff J et al. A certificate infrastructure for machine-checked proofs of conditional information flow. In Principles 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. 2012. p. 369-389. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-28641-4_20

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

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this