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

In this paper we generalize the notion of non-interference making it parametric relatively to what an attacker can analyze about the input/output information flow. The idea is to consider attackers as data-flow analyzers, whose task is to reveal properties of confidential resources by analyzing public ones. This means that no unauthorized flow of information is possible from confidential to public data, relatively to the degree of precision of an attacker. 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. This provides a comprehensive account of non-interference features for language-based security. We introduce systematic methods for extracting attackers from programs, providing domain-theoretic characterizations of the most precise attackers 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 language-based security by abstract interpretation.