A weakest precondition approach to active attacks analysis
By: Musard Balliu and Isabella Mastroeni
Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
isabella.mastroeni@univr.it
Abstract:
Information flow controls can be used to protect both data
confidentiality and data integrity. The certification of the security
degree of a program that runs in untrusted environments still remains
an open problem in language-based security. The notion of robustness
asserts that an active attacker, who can modify program code in some
fixed points ({\em holes}), is not able to disclose more private
information than a passive attacker, who merely observes public
data. In this paper, we extend a method recently proposed for checking
declassified non-interference in presence of passive attackers only,
in order to check robustness by means of the weakest precondition
semantics. In particular, this semantics simulates the kind of
analysis that can be performed by an attacker, i.e., from the public
output towards the private input. The choice of the semantics lets us
distinguish between different attacks models. In this paper, we also
introduce relative robustness that is a relaxed notion of robustness
for restricted classes of attacks.
Related papers: