Modeling Declassification Policies using Abstract Domain Completeness

This paper explores a three dimensional characterisation of a declassification-basednon-interference policy and its consequences. Two of the dimensions consist of specifying:(a) the power of the attacker, that is, what public information a program has that anattacker can observe; and(b) what secret information a program has that needs to be protected.Both these dimensions are regulated by the third dimension:(c) the choice of program semantics, for example, trace semantics or denotationalsemantics, or any semantics in Cousot’s semantics hierarchy.To check whether a program satisfies a non-interference policy, one can compute an abstractdomain that over-approximates the information released by the policy and then checkwhether program execution can release more information than permitted by the policy.Counterexamples to a policy can be generated by using a variant of the Paige–Tarjanalgorithm for partition refinement. Given the counterexamples, the policy can be refined sothat the least amount of confidential information required for making the program secure isdeclassified.