A weakest precondition approach to active attacks analysis

Information flow controls can be used to protect both dataconfidentiality and data integrity. The certification of the securitydegree of a program that runs in untrusted environmentsstill 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 (holes),is not able to disclose more private information than a passiveattacker, who merely observes public data. In this paper,we extend a method recently proposed for checking declassifiednon-interference in presence of passive attackers only,in order to check robustness by means of the weakest preconditionsemantics. In particular, this semantics simulates thekind of analysis that can be performed by an attacker, i.e.,from the public output towards the private input. The choiceof the semantics lets us distinguish between different attacksmodels. In this paper, we also introduce relative robustnessthat is a relaxed notion of robustness for restricted classes ofattacks.