Information Flow Analysis

@incollection{SchebenGreiner2016,
  author    = {Christoph Scheben and
               Simon Greiner},
  title     = {Information Flow Analysis},
  booktitle = {Deductive Software Verification - The {\KeY} Book: From Theory to Practice},
  series    = {Lecture Notes in Computer Science},
  volume    = {10001},
  pages     = {453--471},
  chapter   = {13},
  part      = {III: From Verification to Analysis},
  publisher = {Springer},
  year      = {2016},
  doi       = {10.1007/978-3-319-49812-6_13},
  month     = dec,
  abstract  = {Information flow analysis detects and controls how sensitive information is
               propagated through an application. We give a formal model of what it means
               for sensitive information to be revealed, as well as an extension of JML that
               allows for the specification of information flow concerns. We present an
               approach by which we can verify these JML contracts using {\KeY}. It is based on
               two symbolic executions of the program.}
}