Information Flow, Modularity, and Declassification

October 26, 2006
Anindya Banerjee | Kansas State University

We give, via a relational Hoare-like logic, the specification of an interprocedural and flow sensitive (but termination insensitive) information flow analysis for heap-manipulating programs. Pointer aliasing is ubiquitous in such programs, and can potentially leak confidential information. Thus the logic employs agreement assertions to describe the noninterference property that formalizes confidentiality, and employs region assertions to describe possible aliasing. Programmer assertions, in the style of JML, are also allowed, thereby permitting a more fine-grained specification of information flow policy. The logic supports local reasoning about state in the style of separation logic.

In the second, more speculative part of the talk, we show how the logic can be used to formalize some recent proposals for declassification. We also show limitations of the logic and consider how abstract interpretation techniques may be used to calculate the amount of information released by a security policy.

Parts of this work are joint with Torben Amtoft, Sruthi Bandhakavi, Roberto Giacobazzi, Isabella Mastroeni and David Naumann.

Speaker Details

Anindya Banerjee is associate professor of computing and information sciences at Kansas State University. His research interests are in language-based computer security, all aspects of modularity – in particular, modular program analysis and verification, and concurrency. He is a recipient of the Career Award from the National Science Foundation.