30/05/2008, 16:30 — 17:30 — Room P3.10, Mathematics Building
Gérard Boudol, INRIA, Sophia-Antipolis Méditérranée
Secure Information Flow as a Safety Property
In this work we argue that, in the perspective of developing
"security-minded" programming languages, the secure information
flow property should be defined (as well as disciplined access) as
a standard safety property, based on a notion of a security error,
namely that one should not put in a public location a value
elaborated using confidential information. We show that this is the
property guaranteed by a standard security type system, and that,
for a simple language, it is strictly stronger than
non-interference. Moreover, we show that this notion of secure
information flow allows us to give natural semantics to various
security-minded programming constructs, including declassification.
This seminar will be held in the Alameda campus!
