A weakest precondition approach to active attacks analysis
2009 (English)In: PLAS'09: Proceedings of the ACM SIGPLAN 4th Workshop on Programming Languages and Analysis for Security, 2009, 59-71 p.Conference paper (Refereed)
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 (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.
Place, publisher, year, edition, pages
2009. 59-71 p.
Active attackers, Declassification, Non-interference, Program semantics, Robustness
IdentifiersURN: urn:nbn:se:kth:diva-81034DOI: 10.1145/1554339.1554348ScopusID: 2-s2.0-70450253335ISBN: 9781605586458OAI: oai:DiVA.org:kth-81034DiVA: diva2:497039
ACM SIGPLAN 4th Workshop on Programming Languages and Analysis for Security, PLAS 2009; Dublin; 15 June 2009 through 15 June 2009
QC 201202162012-02-102012-02-102012-02-16Bibliographically approved