Secure Information Flow by Self-Composition

11 years 10 months ago
Secure Information Flow by Self-Composition
Non-interference is a high-level security property that guarantees the absence of illicit information leakages through executing programs. More precisely, non-interference for a program assumes a separation between secret inputs and public inputs on the one hand, and secret outputs and public outputs on the other hand, and requires that the value of public outputs does not depend on the value of secret inputs. A common means to enforce non-interference is to use an information flow type system. However, such type systems are inherently imprecise, and reject many secure programs, even for simple programming languages. The purpose of this paper is to investigate logical formulations of non-interference that allow a more precise analysis of programs. It appears that such formulations are often sound and complete, and also amenable to interactive or automated verification techniques, such as theorem-proving or model-checking. We illustrate the applicability of our method in several scenar...
Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where CSFW
Authors Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk
Comments (0)