Abstract Non-Interference: Parameterizing Non-Interference by Abstract Interpretation

Roberto Giacobazzi and Isabella Mastroeni

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


Abstract

In this paper we introduce the notion of parametric non-interference relatively to an observation. This means that no unauthorized flow of information is possible in programs from confidential to public data, relatively to what the attacker can observe on input/output. The idea is to consider attackers as dataflow analyzers, whose task is to reveal properties of confidential resources by analyzing public ones. We prove that this notion can be fully specified in standard abstract interpretation framework, making the degree of security of a program a property of its semantics. We introduce systematic methods for extracting attackers from programs, providing a domain-theoretic characterization of the most precise attacker which cannot violate the security of a given program. These methods allow us both to compare attackers and program secrecy by comparing the corresponding abstractions in the lattice of abstract interpretations, and to design automatic program certification tools for security by abstract interpretation.


Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems