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.

What you lose is what you leak: Information leakage in declassification policies

GIACOBAZZI, Roberto;MASTROENI, Isabella
2007-01-01

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.
2007
Abstract interpretation; completeness; declassification; information flow
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/242968
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 15
  • ???jsp.display-item.citation.isi??? ND
social impact