Regression Verification for Java Using a Secure Information Flow Calculus

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.

BibTeX

@InProceedings{BeckertKlebanovUlbrich2015,
  author       = {Bernhard Beckert and Vladimir Klebanov and Mattias Ulbrich},
  title        = {Regression Verification for {J}ava Using a Secure Information Flow Calculus},
  booktitle    = {17th Workshop on Formal Techniques for
                  Java-like Programs (FTfJP 2015)},
  month        = jul,
  year         = {2015},
  pages        = {6:1--6:6},
  url          = {https://doi.acm.org/10.1145/2786536.2786544},
  doi          = {10.1145/2786536.2786544},
  publisher    = {ACM}
}