Information Security Seminar 

03/04/2007, 16:30 — 17:30 — Tagus-1.1
Tamara Rezk, INRIA Microsoft Research Joint Centre

Cryptographically secure implementations of non-interferent programs

Confidentiality and integrity properties in language-based security are specified with the help of a set of security levels, and a partial order that describes permitted flows of information. Security levels associated to variables of programs describe different policies specifying e.g. who can read (confidentiality) and who can write (integrity) a given piece of data. Preservation of specified confidentiality and integrity policies associated with variables can be proved using the definition of non-interference that states that the attacker knowledge is not augmented by execution of programs.
In a distributed setting, a permitted flow of information from one variable to another variable may require communication over untrusted channels, e.g. shared memory that can be access (read and modify) by active adversaries. In this case, primitives for encryption and signing are necessary. However, classical non-interference properties are too strict to express that attacker knowledge is not augmented by execution of programs with cryptography. Hence preservation of specified confidentiality and integrity policies cannot be proved using non-interference. Computational non-interference allows one to specify preservation of confidentiality and integrity properties, using computational hypotheses about the cryptography used in the language.
In this work we propose a sound translation from programs with private communication satisfying non-interference to programs with shared-memory communication and cryptography. To this end, we propose type systems for each language, and prove that the translation is typability preserving. Joint work with Cédric Fournet, Microsoft Research Cambridge.