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


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:
  • What you lose is what you leak: Information Leakage in Declassification Policies (MFPS 2007)
  • Adjoining Declassification and Attack Models by Abstract Interpretation (ESOP'05,2005)
  • Abstract Non-Interference - Parameterizing non-interference by Abstract Interpretation (POPL'04,2004)
  • Making Abstract Interpretation Complete (JACM,2000)
  • Proving Abstract Non-Interference (CSL, 2004)
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2), 1996)
  • Refining and compressing abstract domains (ICALP'97, LNCS 1256: 771-781, 1997)

  • isabella.mastroeni@univr.it