A Separation Logic for Enforcing Declarative Information Flow Control Policies

Last modified: Wed Aug 13 01:08:28 2014 GMT.

Authors

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

In Proc. 3rd Conference on Principles of Security and Trust (POST), Grenoble, France, April 2014. Lecture Notes in Computer Science, Vol. 8414, pages 179-198. [pdf]

Coq proofs (Coq version 8.4pl2) : [Coq file] [html] [html, proof scripts omitted] [pdf] [pdf, proof scripts omitted]

colophon