A logic for information flow in object-oriented programs
Sigplan Notices, Volume 41, Issue 1, 2006, Pages 91-102.
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 noninte...More
PPT (Upload PPT)