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

DOI10.1007/978-3-642-28641-4_20MaRDI QIDQ2894335zbMATH OpenOpenAlexFDO

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

Publication date 29 June 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-28641-4_20

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Cryptography (94A60)

Recommendations

• Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays
• Information flow certificates
• A verified information-flow architecture
• Secure information flow by self-composition
• scientific article; zbMATH DE number 2163030

Cited in

(7)

• Information flow certificates
• CoSMed: a confidentiality-verified social media platform
• Hoare logic for disjunctive information flow
• Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays
• Content dependent information flow control
• scientific article; zbMATH DE number 6741937 (Why is no real title available?)
• On mixed connectivity certificates

Describes a project that uses

Uses Software

• Coq
• Toolchain

This page was built for publication: A certificate infrastructure for machine-checked proofs of conditional information flow

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2894335)