Software
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 residual min-entropy measurement in QIF, this entails an error on the conservative side.
ApproxMC-p
A sound, approximative, projection-capable #SAT solver based on universal hashing. For details, see the QAPL 2016 paper.
Supplementary Materials
- Benchmarks: A few #SAT-p benchmarks, derived from the scaled up versions of Meng/Smith QIF benchmarks.
- Patches for CLASP and the Brauer/King #SAT-p solvers so they can read the benchmarks above.
- A patched version of cryptominisat4 as a #SAT-p solver with the same interface (recommended for ApproxMC-p).
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
