<-- Back to the seminar list

Security by Logic : Characterizing Non-Interference in Temporal Logic.

Henri-Charles Blondeel

Project Everest, INRIA Sophia Antipolis

Wednesday, December the 12th 2007, 2:30pm, Fermat Jaune

Abstract:

The information security community has still not reached consensus on how the notion of Non-Interference can be expressed for concurrent programs. Intuitive ly, Non-Interference expresses that the observation of public data during the execution of a program should not reveal information about private data. An at tacker can infer information in many different ways, for instance by observing whether an execution terminates, or by studying the stochastic behaviour of a program. As a step towards unifying the different proposals of Non-Interference, we have re-expressed them over a uniform program model. This program model captures the behaviour of a simple, parallel programming language with shared data. We also propose some variants and compare the main definitions. In particular, th is comparison allows us to conclude that all properties are uncomparable. A traditional way to enforce Non-Interference, is by the use of a security type system. However, this method is not precise. An alternative is to use a temp oral logic characterization that is amenable to model checking. We show how this can be achieved for the Non-Interference properties that do not involve pro babilities.