Information Technology Reference
In-Depth Information
Generalized Abstract Non-interference:
Abstract Secure Information-Flow
Analysis for Automata
Roberto Giacobazzi and Isabella Mastroeni
Dipartimento di Informatica - Universita di Verona, Italy
roberto.giacobazzi@univr.it
mastroeni@sci.univr.it
Abstract.
Abstract non-interference has been introduced as a weaken-
ing non-interference which models 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 au-
tomata as models of real-time systems, and concurrent systems. We show
that well known definitions of non-interference in these models of com-
putation 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. More-
over, the most precise harmless attacker of a system is systematically
derived by transforming abstract domains, characterizing the security
degree of automata and concurrent systems.
1
Introduction
Non-interference [15] is a key notion in language based security. The idea is
that no information about confidential data can be obtained by observing public
information. The standard methods used for preventing interference are based
on access control, i.e. higher privileges are required in order to access files con-
taining confidential data. The problem with these methods is that, after access,
there is no further control on how confidential information flows during execu-
tion. Hence, many techniques for checking
secure information flows
in software
and systems, ranging from standard data-flow/control-flow analysis techniques
to type inference, are studied, based on non-interference (see [22] and [11] for
excellent surveys). All these approaches are devoted to prove that a system as
a whole, or parts of it, does not allow confidential data to flow towards public
variables. Type-based approaches are designed in such a way that well-typed
programs do not leak secrets. In a security-typed language, a type is induc-
tively associated at compile-time with program statements in such a way that
any statement showing a potential flow disclosing secrets is rejected [25,27,28].
