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