Information Flow, Modularity, and Declassification

Опубликовано 7 сентября 2016, 16:34

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.