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

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.