Compiling Information-Flow Security to Minimal Trusted Computing Bases

DOI10.1007/978-3-642-19718-5_12MaRDI QIDQ3000581zbMATH OpenOpenAlexFDO

Authors Jérémy Planul, Cédric Fournet

Publication date 19 May 2011

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19718-5_12

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Recommendations

• scientific article; zbMATH DE number 1692935
• A minimal model for secure computation (extended abstract)
• Secure information flow by self-composition
• Theorem Proving in Higher Order Logics
• A formal treatment of the role of verified compilers in secure computation

Cites work

• A lattice model of secure information flow
• A semantic framework for declassification and endorsement
• Cryptographically sound implementations for typed information-flow security
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• New directions in cryptography

Cited in

(6)

• Automated Verification of Dynamic Root of Trust Protocols
• Cryptographically sound implementations for typed information-flow security
• Using security policies to write secure software
• scientific article; zbMATH DE number 1832235 (Why is no real title available?)
• A verified information-flow architecture
• Foundations of Software Science and Computation Structures

Describes a project that uses

Uses Software

• Jif
• Flicker

This page was built for publication: Compiling Information-Flow Security to Minimal Trusted Computing Bases

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