Sciweavers

POPL
2006
ACM

A logic for information flow in object-oriented programs

14 years 3 months ago
A logic for information flow in object-oriented programs
This paper specifies, via a Hoare-like logic, an interprocedural and flow sensitive (but termination insensitive) information flow analysis for object-oriented programs. Pointer aliasing is ubiquitous in such programs, and can potentially leak confidential information. Thus the logic employs independence 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. Small specifications are used; they mention only the variables and addresses relevant to a command. Specifications are combined using a frame rule. An algorithm for the computation of postconditions is described: under certain assumptions, there exists a strongest postcondition which the algorithm computes.
Torben Amtoft, Sruthi Bandhakavi, Anindya Banerjee
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where POPL
Authors Torben Amtoft, Sruthi Bandhakavi, Anindya Banerjee
Comments (0)