Deriving and Proving Abstract non-Interference

Supervisor
Isabella Mastroeni - Universita' di Verona
Date and time
Tuesday, March 9, 2004 at 5:30 PM
Place
Ca' Vignal - Piramide, Floor 0, Hall Verde
Programme Director
Nicola Fausto Spoto
External reference
Publication date
February 19, 2004
Department
 

Summary

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. In this way we make the security degree a program a property of its semantics. 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. Moreover we introduce a compositional proof-system for certifying abstract non-interference in programming languages. Assertions specify the secrecy of a program relatively to the given attacker and the proof-system specifies how these assertions can be composed in a syntax-directed a la Hoare deduction of secrecy. We prove that the proof-system is sound relatively to the standard semantics of an imperative programming language with non-deterministic choice.





© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234