Compiling Information-Flow Security to Minimal Trusted Computing Bases

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

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)

Cites Work

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

Related Items (1)

Automated Verification of Dynamic Root of Trust Protocols

Uses Software

• Jif
• Flicker

Recommendations

• Title not available (Why is that?) 👍 👎
• A formal treatment of the role of verified compilers in secure computation 👍 👎
• A minimal model for secure computation (extended abstract) 👍 👎
• Secure information flow by self-composition 👍 👎
• Theorem Proving in Higher Order Logics 👍 👎

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)