Information Flow in Object-Oriented Software

Abstract This paper contributes to the investigation of object-sensitive information flow properties for sequential Java, i. e. , properties that take into account information leakage through objects, as opposed to primitive values. We present two improvements to a popular object-sensitive non-interference property. Both reduce the burden on analysis and monitoring tools. We present a formalization of this property in a program logic – JavaDL in our case – which allows using an existing tool without requiring program modification. The third contribution is a novel fine-grained specification methodology. In our approach, arbitrary JavaDL terms (read ‘side-effect-free Java expressions’) may be assigned a security level – in contrast to security labels being attached to fields and variables only.

Authors

• Bernhard Beckert
• Daniel Bruns
• Vladimir Klebanov
• Christoph Scheben
• Peter H. Schmitt
• Mattias Ulbrich

Keywords

No keywords are indexed for this paper.