Regression Verification for Java Using a Secure Information Flow Calculus

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Bernhard Beckert, Vladimir Klebanov und Mattias Ulbrich
In:17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)
Verleger:ACM
Jahr:2015
Seiten:6:1–6:6
DOI:10.1145/2786536.2786544
Links:

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{Beckert2015,
  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)},
  pages = {6:1--6:6},
  doi = {10.1145/2786536.2786544},
  publisher = {ACM},
  month = jul,
  year = {2015}
}