Information Flow Analysis

Buchkapitel

Autor(en):Christoph Scheben und Simon Greiner
In:Deductive Software Verification - The KeY Book: From Theory to Practice
Verleger:Springer
Reihe:Lecture Notes in Computer Science
Band:10001
Teil:III: From Verification to Analysis
Kapitel:13
Jahr:2016
Seiten:453-471
DOI:10.1007/978-3-319-49812-6_13

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.

BibTeX

@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.}
}