# Deductive Program Verification

## KeY

KeY is a deductive system for functional verification of Java / Java Card programs. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface.

## KeY Concurrent (MODL)

KeY/MODL is a prototype for functional verification of (a class of) multi-threaded Java programs. KeY/MODL is experimental software and available upon request.

The following publication describes the theory behind KeY/MODL:

Bernhard Beckert, Vladimir Klebanov:

*A Dynamic Logic for Deductive Verification of Multi-threaded Programs*

Formal Aspects of Computing, special issue of revised papers
originally published in the International Conference on Software
Engineering and Formal Methods (SEFM)

PDF
- BibTeX
- Abstract
- SpringerLink

## VerifyThus

VerifyThus is a formal methods dissemination effort. It is a linux distribution with a number of deductive verification tools pre-installed and ready to run. The VerifyThus image can be booted from a USB stick or run in a virtual machine.

# #SAT Solving under Projection

#SAT is the problem of counting the models of a propositional formula. The following tools combine #SAT solving with projection. Projecting a propositional formula F on the scope (i.e., set of variables) d produces a formula F' that says the same things about d as F but nothing else.

#SAT solving under projection can be used, e.g., in security analysis of software (see below).

## Dsharp-p

This is an extension of the #SAT solver (and d-DNNF compiler) Dsharp with projection capabilities.

bitbucket.org/vladimirkl/dsharp

## sharp-p-SAT

This is an extension of the #SAT solver sharpSAT with projection capabilities. At the moment, the projection computed by sharp-p-SAT is not exact but may describe too many models. For applications like QIF (see below), this entails an error on the conservative side.

## Supplementary Materials

- Benchmarks
- Patches for other projection/model enumeration tools (so they can read the benchmarks above)

# Quantitative Information Flow Analysis

Quantitative information flow analysis (QIF) is a collection of techniques for security assessment of software. The research in QIF is motivated by the observation that it is not feasible to completely prevent information leaks (i.e., the flow of confidential information to public ports) in realistic systems. Instead, practical security analysis demands a measure of leaked information in order to decide if a leak is tolerable.

Please note: The tools listed below are toolchains, i.e., there is no single executable. Instead, a description is provided on how to use several tools in combination to achieve the desired result.

## QIF/Poly: A polyhedra-based analysis (for imperative Java programs)

This is a QIF analysis for a subset of Java programs, based on polyhedral techniques (Barvinok's algorithm). The main limitation is that the indistinguishability relation of the program is affine (roughly: can be described with linear arithmetic). The analysis combines the KeY tool (see above) and the isl/barvinok framework by Sven Verdoolaege.

A description of the approach is available in:

Vladimir Klebanov:

*Precise Quantitative Information Flow Analysis - A Symbolic Approach*

Theoretical Computer Science (TCS), 2014

BibTeX
- Abstract
- ScienceDirect

and (outdated)

Vladimir Klebanov:

*Precise Quantitative Information Flow Analysis Using Symbolic Model Counting*

International Workshop on Quantitative Aspects in Security Assurance
(QASA), 2012

PDF
- BibTeX

## QIF/SAT: A SAT-based analysis (for ANSI C programs)

This is a SAT-based QIF analysis for ANSI C programs, i.e., the program behavior is reduced to a (large) propositional formula. There are no restrictions w.r.t. the shape of the indistinguishability relation, but only small sets of possible low inputs can be modeled with acceptable efficiency. The analysis combines the CBMC model checker with #SAT tools we extended with projection: Dsharp-p, sharp-p-SAT (see above), and/or sharpCDCL by Norbert Manthey.

A description of the approach is available in:

Vladimir Klebanov, Norbert Manthey, and Christian Muise:

*SAT-based Analysis and Quantification of Information Flow in Programs*

International Conference on Quantitative Evaluation of Systems (QEST 2013)

PDF
- BibTeX
- Abstract
- LNCS
8054

# Regression Verification

Regression verification is an approach complementing
regression testing with formal verification. The goal is to **formally
prove** that two versions of a program **behave** either
**equally** or differently in a precisely specified way.

## Rêve - An Automated Tool for Regression Verification / Equivalence Checking

Rêve is a tool that automatically checks whether two C-like programs behave equally. You can try rêve online.

A description of the approach is available in:

Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer,
and Mattias Ulbrich:

*Automating Regression Verification*

Intl. Conference on Automated Software Engineering (ASE 2014)

PDF
- BibTeX
- ACM DL