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

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


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
Related papers:
  • What you lose is what you leak: Information Leakage in Declassification Policies (MFPS 2007)
  • Adjoining Declassification and Attack Models by Abstract Interpretation (ESOP'05,2005)
  • Abstract Non-Interference - Parameterizing non-interference by Abstract Interpretation (POPL'04,2004)
  • Making Abstract Interpretation Complete (JACM,2000)
  • Proving Abstract Non-Interference (CSL, 2004)
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2), 1996)
  • Refining and compressing abstract domains (ICALP'97, LNCS 1256: 771-781, 1997)