Adjoining Declassification and Attack Models by Abstract Interpretation

In this paper we prove that attack models and robust declassification in language-based security can be viewed as adjoint transformations of abstract interpretations. 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 program's semantics. This observation allows us to prove that the most abstract property on confidential data which can be declassified and the most concrete harmless attacker observing public data, both modeled as abstractions of program's semantics, are respectively the adjoint solutions of a completeness problem in standard abstract interpretation theory. In particular declassification corresponds to refine the given model of an attacker with the minimal amount of information to in order to achieve completeness, which is non-interference, while the harmless attacker corresponds to remove this information. This proves an adjunction relation between two basic approaches to language-based security: declassification and the construction of suitable attack models, and allows us to apply relevant techniques for abstract domain transformation in language-based security.