Regression Verification for Java Using a Secure Information Flow Calculus (bibtex)
by Bernhard Beckert, Vladimir Klebanov and Mattias Ulbrich
Abstract:
Regression verification and checking for illicit information flow in programs are probably the two most prominent instances of so-called relational program reasoning. Regression verification is concerned with proving that two programs behave either equally or differently in a formally specified manner; information-flow checking aims to establish that an attacker cannot distinguish executions of a program that vary in a part of the initial state designated as secret. While the theoretical connections between the two problems are well understood, there are also subtle but significant pragmatic differences. This paper reports the results of an experiment to adapt a state-of-the-art deductive information-flow verification system for Java to the problem of regression verification.
Reference:
Regression Verification for Java Using a Secure Information Flow Calculus (Bernhard Beckert, Vladimir Klebanov and Mattias Ulbrich), In 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015), 2015.
Bibtex Entry:
@InProceedings{BeckertKlebanovUlbrich2015,
  author =       {Bernhard Beckert and Vladimir Klebanov and Mattias
                  Ulbrich},
  title =        {Regression Verification for Java Using a Secure
                  Information Flow Calculus},
  booktitle =    {17th Workshop on Formal Techniques for Java-like
                  Programs (FTfJP 2015)},
  month =        jul,
  year =         2015,
  abstract =     {Regression verification and checking for illicit
                  information flow in programs are probably the two
                  most prominent instances of so-called relational
                  program reasoning. Regression verification is
                  concerned with proving that two programs behave
                  either equally or differently in a formally
                  specified manner; information-flow checking aims to
                  establish that an attacker cannot distinguish
                  executions of a program that vary in a part of the
                  initial state designated as secret. While the
                  theoretical connections between the two problems are
                  well understood, there are also subtle but
                  significant pragmatic differences. This paper
                  reports the results of an experiment to adapt a
                  state-of-the-art deductive information-flow
                  verification system for Java to the problem of
                  regression verification.},
  http =
                  {https://formal.iti.kit.edu/biblio/?lang=en&key=BeckertKlebanovUlbrich2015},
  keywords =     {IMPROVE},
}
Powered by bibtexbrowser