Modelling Declassification Policies using Abstract Domain Completeness

This paper explores a three dimensional characterization of a declassification-based noninterference policy and its consequences. Two of the dimensions consist in specifying (a) the power of the attacker, that is, what public information an attacker can observe of a program, and (b) what secret information of a program needs to be protected. Both these dimensions are regulated by the third dimension, (c) the choice of program semantics, for example, trace semantics or denotational semantics, or indeed any semantics in Cousot's semantics hierarchy. To check whether a program satisfies a noninterference policy one can compute an abstract domain that over-approximates the information released by the policy and can subsequently check whether program execution may release more information than what is permitted by the policy. Counterexamples to a policy can be generated by using a variant of the Paige-Tarjan algorithm for partition refinement. Given the counterexamples the policy can be refined so that the least amount of confidential information necessary for making the program secure is declassified.