Adjoining classified and unclassified information by Abstract Interpretation

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.