Secure Information Flow by Self-Composition

TitleSecure Information Flow by Self-Composition
Publication TypeConference Paper
Year of Publication2004
AuthorsBarthe, G, D'Argenio, PR, Rezk, T
Conference Name17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004)
PublisherIEEE Computer Society
ISBN Number0-7695-2169-X
AbstractNon-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 an 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 scenarii, including a simple imperative language, a non-deterministic language, and finally a language with shared mutable data structures.
PDF (Full text): 
Powered by Drupal