Secure Information Flow as a Safety Property

In this paper 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.