Authors
David Costanzo
Zhong Shao
Abstract
In this paper, we present a program logic for proving that a program does not
release information about sensitive data in an unintended way. The most important
feature of the logic is that it provides a formal security guarantee while supporting
"declassification policies" that describe precise conditions under which a piece
of sensitive data can be released. We leverage the power of Hoare Logic to express
the policies and security guarantee in terms of state predicates. This allows our
system to be far more specific regarding declassification conditions than most other
information flow systems.
The logic is designed for reasoning about a C-like, imperative language with
pointer manipulation and aliasing. We therefore make use of ideas from Separation
Logic to reason about data in the heap.
Published