What you lose is what you leak: Information leakage in Declassification Policies

By: Anindya Banerjee, Roberto Giacobazzi and Isabella Mastroeni

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

Roberto Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
roberto.giacobazzi@univr.it

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

Abstract:

This paper suggests the following approach for checking whether a program satisfies an information flow policy that may declassify secret information: (a) Compute a finite abstract domain that overapproximates the information released by the policy and (b) Check whether program execution may release more information than what is permitted by the policy by completing the finite abstract domain wrt.\ weakest liberal preconditions. Moreover, techniques based on the Paige-Tarjan algorithm for partition refinement can be used to generate counterexamples to a declassification policy: the counterexamples demonstrate that more information is released by the program than what the policy permits. Subsequently the policy can be refined so that the least amount of confidential information necessary for making the program secure is declassified.
Related papers:
  • 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)

    • mastroeni@sci.univr.it