Cryptographically sound implementations for typed information-flow security

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they can often be verified by typing. However, their enforcement in concrete systems involves delicate compilation issues. We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an access-control policy for reading and writing the shared memory. In their implementations, shared memory is unprotected and security depends instead on encryption and signing. We build a translation from well-typed source programs and policies to cryptographic implementations. To establish its correctness, we develop a type system for the target language. Our typing rules enforce a ...

• Type: Conference
• Year: 2008
• Where: POPL
• Authors: Cédric Fournet, Tamara Rezk
• Keywords: Delicate Compilation Issues, Keywords Secure Information, POPL 2008, Programming Languages, Translation Preserves Typability