Information Security Seminar 

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.