Transforming abstract interpretations by abstract interpretation

New challenges in language-based security

Invited Lecture (Slides)

By: R. Giacobazzi and I. Mastroeni

Roberto Giacobazzi
Dip. di Informatica
Univsit\agrave di Verona
Strada Le Grazie a Ca' Vignal 2, 37134 Verona (Italy)


In this paper we exploit abstract interpretation for transforming abstract domains and semantics. The driving force in both transformations is making domains and semantics, \ie abstract interpretations themselves, complete, namely precise, for some given observation. We prove that a common geometric pattern is shared by all these transformations, both at the domain and semantic level. This pattern is based on the notion residuated closures, which in our case can be viewed as an instance of abstract interpretation. We consider these operations in the context of language-based security, and show how domain and semantic transformations model security policies and attackers, opening new perspectives in the model of information flow in programming languages.

Available from PDF, BibTeX Entry.

Related papers:
  • 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)
  • Making abstract interpretations complete (ACM JACM 47(2):361-416, 2000)
  • Building Complete Abstract Interpretations in a Linear Logic-based Setting (SAS'98, LNCS, 1998)
  • Incompleteness, Counterexamples and Refinements in Abstract Model-Checking (SAS'01, LNCS 2126, 2001)
  • Domain Compression for Complete Abstractions (VMCAI'03, LNCS 2575, 2003)
  • Abstract Non-Interference (ACM POPL'04, 2004)
  • Making abstract domains condensing (ACM Transactions on Computational Logic (TOCL). 6(1):33--60, 2005)
  • Transforming Semantics by Abstract Interpretation (Theoretical Computer Science. 337(1-3):1-50, 2005)
  • Adjoining Declassification and Attack Models by Abstract Interpretation (ESOP05, LNCS 3444 2006)
  • Incompleteness of States w.r.t. Traces in Model Checking (Inf and Comp 204(3):376-407, 2006)
  • What you lose is what you leak: Information leakage in Declassification Policies (MFPS'07, ENCS 2007)