Adjoining classified and unclassified information by Abstract Interpretation

Completeness in abstract interpretation models the ideal situation where no loss of precision is introduced in computations by approximating concrete data by their abstractions. If we interpret the abstraction as the ability of an attacker to distinguish, i.e., observe, properties of public computations, and the computation as the concrete denotational semantics of the program, then the lack of precision, encoded in abstract interpretation as a lack of completeness, corresponds precisely to the leakage of information corresponding to a violated security policy. This correspondence allows us to inherit, in the field of language-based security, the whole theory and methodology for making abstract domains complete. In particular, we prove that an adjoint relation exists between the power of the attacker and the amount of the information released – the more the attacker can observe, the less information can be kept private. This characterisation is achieved by interpreting, in the security context, the standard adjoint transformations making an abstract domain complete by refining and simplifying abstractions.