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.
Room 1.4. Note the exceptional date and location.
