Information Flow in Object-Oriented Software

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich
In:23rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2013), Revised Selected Papers
Publisher:Springer
Series:Lecture Notes in Computer Science
Year:2013
Number:8901
Pages:19-37
DOI:10.1007/978-3-319-14125-1_2

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. The second contribution is 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.

BibTeX

@InProceedings{BeckertBrunsKlebanovEtAl2013,
  author        = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov
                   and Christoph Scheben and Peter H. Schmitt and Mattias
                   Ulbrich},
  title         = {Information Flow in Object-Oriented Software},
  booktitle     = {23rd International Symposium on Logic-Based Program
                   Synthesis and Transformation ({LOPSTR} 2013), Revised
                   Selected Papers},
  editor        = {Gopal Gupta and Ricardo Pe{\~n}a},
  language      = {english},
  year          = 2013,
  month         = sep,
  publisher     = {Springer},
  series        = {Lecture Notes in Computer Science},
  number        = 8901,
  pages         = {19--37},
  doi           = {10.1007/978-3-319-14125-1_2},
  isbn          = {978-3-319-14125-1},
  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. The second contribution is 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.}
}