Adjoining classified and unclassified information by Abstract Interpretation

By: Roberto Giacobazzi and Isabella Mastroeni

Roberto Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy

Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy


In this paper we prove that attack models and information released in language-based security can be viewed as adjoint transformations in the abstract interpretation framework. This is achieved by interpreting the well known Joshi and Leino's semantic approach to non-interference as a problem of making an abstraction complete relatively to a program's semantics. This observation allows us to prove that the maximal confidential information that flows, and the most powerful harmless attacker observing output public data, both modeled as abstractions of the program's semantics, are respectively the adjoint solutions of a completeness problem in standard abstract interpretation theory. In particular the information released corresponds to refining the given declassification policy with the minimal amount of information that has to be observed in order to achieve completeness, and hence security, while the harmless attacker corresponds to remove this information from the attacker model. The completeness model of non-interference provides a deeper insight in the relation between these facets of non-interference, allowing to prove that we cannot minimally characterise which information we can keep secret.
Available: Pdf
Related papers:
  • Modelling Declassification Policies using Abstract Domain Completeness (Submitted for publication, 2008)
  • What you lose is what you leak: Information leakage in Declassification Policies (MFPS'07)
  • Adjoining Declassification and Attack Models by Abstract Interpretation (ESOP'05)
  • Modeling Information Flow Dependencies with Boolean Functions (WITS'04,2004)
  • 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)
  • Handling the puzzle of semantics (Submitted for publication, 2002 )