Beschreibung:
<jats:p>This paper explores a three dimensional characterisation of a declassification-based non-interference policy and its consequences. Two of the dimensions consist of specifying:<jats:list list-type="number"><jats:list-item><jats:label>(a)</jats:label><jats:p>the power of the attacker, that is, what public information a program has that an attacker can observe; and</jats:p></jats:list-item><jats:list-item><jats:label>(b)</jats:label><jats:p>what secret information a program has that needs to be protected.</jats:p></jats:list-item></jats:list>Both these dimensions are regulated by the third dimension:<jats:list list-type="number"><jats:list-item><jats:label>(c)</jats:label><jats:p>the choice of program semantics, for example, trace semantics or denotational semantics, or any semantics in Cousot's semantics hierarchy.</jats:p></jats:list-item></jats:list>To check whether a program satisfies a non-interference policy, one can compute an abstract domain that over-approximates the information released by the policy and then check whether 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–Tarjan algorithm for partition refinement. Given the counterexamples, the policy can be refined so that the least amount of confidential information required for making the program secure is declassified.</jats:p>