Regression Verification for {J}ava Using a Secure Information Flow Calculus
Bernhard Beckert, Vladimir Klebanov and Mattias Ulbrich
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.