Modelling Declassification Policies using Abstract Domain Completeness

By: Isabella Mastroeni and Anindya Banerjee

Anindya Banerjee
Dept. of Computing and Information Sciences
Kansas State University
Manhattan, Kansas, USA
abanerje@ksu.edu

Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
isabella.mastroeni@univr.it

Abstract:

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.

Available: Pdf