A Cryptographic Compiler for Information-Flow Security

Joint work with Tamara Rezk and Gurvan le Guernic (MSR-INRIA Joint Centre http://msr-inria.inria.fr/projects/sec)

We relate two notions of security: one simple and abstract, based on information flows in programs, the other more concrete, based on cryptography.

In language-based security, confidentiality and integrity policies specify the permitted flows of information between parts of a system with different levels of trust. These policies enable a simple treatment of security, but their enforcement is delicate.

We consider cryptographic enforcement mechanisms for distributed programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. We develop a compiler from a small imperative language with locality and security annotations down to cryptographic implementations in F#. In source programs, security depends on a policy for reading and writing the shared variables. In their implementations, shared memory is unprotected, and security depends instead on encryption and signing.

We rely on standard primitives and hypotheses for cryptography, stated in terms of probabilistic polynomial-time algorithms and games. Relying on a new type system, we show that our compiler preserves all information-flow properties: an adversary that interacts with the trusted components of our code and entirely controls its untrusted components gains illegal information only with negligible probability.