A Logic for Information Flow Analysis of Pointer Programs

This paper specifies a nontermination-insensitive, interprocedural, information flow analysis for objectoriented programs via a Hoare-like logic. Pointer aliasing is ubiquitous in such programs, and can potentially leak confidential information. Therefore, assertions in the logic not only describe the noninterference property that formalizes confidentiality, but also describe aliasing properties. The representation of noninterference in assertions makes explicit the independences between variables and addresses. The logic is flow-sensitive and can deem secure more programs than extant type-based information flow analyses. Modular (or local) reasoning is a critical component of the logic. Apart from supporting interprocedural reasoning in a modular way, the logic also supports local reasoning about state in the style of Separation Logic. "Small" specifications are used; they mention only the variables and addresses relevant to a command. Specifications are combined using a frame rule that is sound in the logic. An algorithm for the computation of postconditions is described: under certain assumptions, there exists a strongest postcondition which the algorithm computes. The core language permits programmer assertions, in the style of ESC/Java, thereby providing a more fine-grained information flow analysis. The logic can thus be viewed as a modular, interprocedural static checker for confidentiality.