A Cryptographic Compiler for Information-Flow Security
------------------------------------------------------
Cedric Fournet

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.