Information Flow in Object-Oriented Software

@InProceedings{BeckertBrunsKlebanovEA2013,
  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},
  volume        = {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.}
}