Compiling Information-Flow Security to Minimal Trusted Computing Bases

DOI10.1007/978-3-642-19718-5_12zbMATH Open1326.68075OpenAlexW2105075717MaRDI QIDQ3000581FDOQ3000581

Cédric Fournet, Jérémy Planul

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

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

Mathematics Subject Classification ID

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

Cites Work

• New directions in cryptography
• A lattice model of secure information flow
• Cryptographically sound implementations for typed information-flow security
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• A Semantic Framework for Declassification and Endorsement

Cited In (2)

• Automated Verification of Dynamic Root of Trust Protocols
• Title not available (Why is that?)

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)