Report 2006-4.
What you lose is what you leak: Information leakage in declassification policies completeness properties of static analyses and their logics
by
Anindya Banerjee and Roberto Giacobazzi and Isabella Mastroeni
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
over-approximates 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.
Report 2006-3.
Comparing
completeness properties of static analyses and their logics
by David A. Schmidt
Report 2006-2.
Underapproximating predicate transformers
by David A. Schmidt
Report 2006-1.
Automata-based non-interference monitoring
by Gurvan le Guernic, Anindya Banerjee, and David Schmidt
Abstract:
This report presents a non-interference monitoring mechanism for
sequential programs. Non-interference is a property of the information
flows of a program. It implies the respect of the confidentiality of the
secret information manipulated. The approach taken uses an automaton based
monitor. During the execution, abstractions of the events occurring are
sent to the automaton. The automaton uses those inputs to track the
information flows and to control the execution by forbidding or editing
dangerous actions. The mechanism proposed is proved to be sound and more
efficient than a type system similar to the historical one developed by
Volpano, Smith and Irvine.