Abstract non-interference has been introduced as a method for weakening standard non-interference by modeling attackers as abstract interpretations (i.e., static analyzers) of programming language semantics. In this paper we generalize the notion of abstract non-interference to deal with tree-like models of computation. This allows us to widen the scope of abstract non-interference for modeling security properties in automata, timed automata as models of real-time systems, and concurrent systems. We show that well known techniques for proving non-interference in these models of computation can be viewed as instances of our generalization. This proves that abstract non-interference can reasonably be considered as a general framework for studying and comparing security properties at different levels of abstraction in both programming languages and systems, making available to security all the methods known in abstract interpretation for reasoning about approximate semantics. In particular the most precise harmless attacker of a system can be systematically derived by transforming abstractions in the lattice of abstract interpretations, giving a ranking of degrees of security for automata and concurrent systems.

Generalized Abstract Non-Interference - Abstract Secure Information-flow Analysis for Automata

GIACOBAZZI, Roberto;MASTROENI, Isabella
2005-01-01

Abstract

Abstract non-interference has been introduced as a method for weakening standard non-interference by modeling attackers as abstract interpretations (i.e., static analyzers) of programming language semantics. In this paper we generalize the notion of abstract non-interference to deal with tree-like models of computation. This allows us to widen the scope of abstract non-interference for modeling security properties in automata, timed automata as models of real-time systems, and concurrent systems. We show that well known techniques for proving non-interference in these models of computation can be viewed as instances of our generalization. This proves that abstract non-interference can reasonably be considered as a general framework for studying and comparing security properties at different levels of abstraction in both programming languages and systems, making available to security all the methods known in abstract interpretation for reasoning about approximate semantics. In particular the most precise harmless attacker of a system can be systematically derived by transforming abstractions in the lattice of abstract interpretations, giving a ranking of degrees of security for automata and concurrent systems.
2005
9783540291138
language-based security; Abstract interpretation; Concurrent system
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/23532
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 2
social impact