Workshop on Program Equivalence
11-12 April 2016
London, United Kingdom
Carsten Fuhs: Proving Equivalence of Imperative Programs via Constrained Rewriting Induction
We apply constrained rewriting induction to prove equivalence of imperative programs that operate on integers and arrays. To this end, our approach first translates the input programs from (a subset of) C to a Logically Constrained Term Rewriting System (LCTRS). LCTRSs are a recent extension of classic term rewriting by predefined functions, targeted at functions for which automated reasoning techniques are readily available in current Satisfiability Modulo Theory (SMT) solvers. On the generated LCTRS, we then perform the actual equivalence proof using constrained rewriting induction. Apart from functional equivalence, our approach also allows us to verify other properties, such as memory safety.
Guilhem Jaber:
Can we automate proof of contextual equivalence using Logical Relations?
Kripke Logical Relations have matured enough to become now a formidable technique to
prove contextual equivalence of effectful higher-order programs.
However, it is not possible yet to automate such proofs.
After presenting the basics of KLRs, we will see what are the obstacles in the automation of this method.
Finally, we will see some leads to circumvent these obstacles, based on symbolic executions, and how we can try to characterize what can be automatically proven by such techniques.
Vasileios Koutavas:
From Applicative to Environmental Bisimulation
We illuminate important aspects of the semantics of higher-order functions that are common in the presence of local state, exceptions, names and type abstraction via a series of examples that add to those given by Stark. Most importantly we show that any of these language features gives rise to the phenomenon that certain behaviour of higher-order functions can only be observed by providing them with arguments which internally call the functions again. Other examples show the need for the observer to accumulate values received from the program and generate new names. This provides evidence for the necessity of complex conditions for functions in the definition of environmental bisimulation, which deviates in each of these ways from that of applicative bisimulation.
Shuvendu Lahiri/ Ofer Strichman:
SymDiff: A differential program verifier
SymDiff is a tool for performing differential program verification. Differential program verification concerns with specifying and proving interesting properties over program differences, as opposed to the program itself. Such properties include program equivalence, but can also capture more general differential/relational properties. SymDiff provides a specification language to state such differential (two-program) properties using the concept of mutual summaries that can relate procedures from two versions. It also provides proof system for checking such differential specifications along with the capability of generating simple differential invariants. This is performed by a novel product construction that allows for Interprocedural inference of mutual summaries. This talk discusses the SymDiff architecture, the product construction and its properties and some current and ongoing applications including equivalence checking, proving relative correctness of bug fixes, safety of approximate transformations and semantic change impact analysis. More details are present here.
Nuno Lopes:
Automatic Equivalence Checking of Programs with Uninterpreted Functions and Integer Arithmetic
I'll present an algorithm for the automatic verification of partial equivalence of two programs over the combined theory of uninterpreted function symbols and integer arithmetic (UF+IA). The proposed algorithm supports, in particular, programs with nested loops.
The crux of the technique is a transformation of uninterpreted functions (UFs) applications into integer polynomials, which enables the precise summarization of loops with UF applications using recurrences. The equivalence checking algorithm then proceeds on loop-free, integer only programs.
We applied the proposed technique for the verification of compiler optimizations, and we show that it can prove more optimizations correct than state-of-the-art techniques.
Nimrod Partush:
Statistical Similarity of Binaries
We present a new statistical approach for measuring the similarity between two procedures in binaries, which allows finding similar code even when it has been compiled using different compilers, or has been modified.
We introduce similarity by composition -- a three phase approach where we (i) decompose the code into smaller comparable fragments (ii) define semantic similarity between fragments, and (iii) use statistical reasoning to lift fragment similarity to similarity between procedures.
We will also present an evaluation of the approach, that we implemented in a tool called Esh, and applied it to find various prominent vulnerabilities across compilers and versions, in real-world binaries, including Heartbleed, Shellshock and Venom.
We will discuss the results and show that Esh produces high accuracy results, with few to no false positives (a crucial factor in the scenario of vulnerability search in stripped binaries).
Steven Ramsay:
Deciding contextual equivalence for IMJ*
I will describe joint work with Andrzej Murawski and Nikos Tzevelekos in
which we consider the problem of deciding observational equivalence for IMJ*.
IMJ* is a kind of maximal fragment of the language Interface Middleweight Java
(IMJ) for which the problem is decidable. Given two, possibly open (containing
free identiers), terms of IMJ*, the contextual equivalence problem asks if the
terms can be distinguished by any possible IMJ context. Our decision procedure
reduces this problem to the emptiness problem for fresh-register pushdown
automata. I will demonstrate our implementation of the procedure in the tool
Coneqct.
Ofer Strichman:
Regression verification: proving the equivalence of similar programs
Regression verification is the problem of proving the equivalence of successive, closely related versions of a program. It has the potential of being easier in practice than functional verification, although both problems are undecidable. In this tutorial I will survey different definitions of equivalence, and then the inference rules that are used in RVT and SymDiff for proving the equivalence of functions with loops and equivalence of recursive functions. I will also briefly discuss the problem of proving mutual termination, and regression verification for multithreaded programs.
Nikos Tzevelekos:
Game Semantics for Interface Middleweight Java
In this talk we present a denotational/operational model that captures the
behaviour of programs written in an object calculus called IMJ and in which
open terms interact with the environment through interfaces. The calculus is
intended to represent the essence of contextual interactions of Middleweight
Java code. The model is based on game semantics, a technique which models
interactions between a program and its environment as formal games. Working
with games, we build fully abstract models for the induced notions of contextual
approximation and equivalence.
This is joint work with A. Murawski.
Mattias Ulbrich:
Automating Regression Verification by Predicate Abstraction:
Pointer Programs and PLC Software
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. We present a novel automatic approach for
regression verification that reduces the equivalence of two related
imperative programs with pointers to constrained Horn clauses over
uninterpreted predicates. Subsequently, state-of-the-art SMT solvers
are used to solve the clauses.
We have implemented the approach as an extension to the LLVM compiler
framework, and our experiments (e.g., on the C standard library) show
that non-trivial programs with integer and pointer arithmetic can now
be proved equivalent without further user input.
We have also applied our approach to programs running on programmable
logic controllers (PLC) driving automated production systems and
succeeded to verify non-trivial evolution steps of PLC software for a
lab-scale automated production system.
Maor Veitsman:
Regression Verification for unbalanced recursive functions
I will begin by showing examples of pairs of recursive functions that are semantically the same, but not in lock-step. The equivalence of such functions cannot be proven by RVT's Hoare-style proof rules, and by any other equivalence or software verification tool that we are aware of. I will present our solution to this problem, which improves the overall completeness of RVT.
Tim Wood:
Modular equivalence verification of procedures that dynamically allocate heap memory
Automatically verifying the equivalence of procedures is useful in
many situations: for example, when trying to establish the correctness
of refactorings, compilation, or optimisation. Automatically verifying
the equivalence of heap manipulating procedures, where the order and
amount of dynamic memory allocation differ, is challenging for
state-of-the-art equivalence verifiers such as Microsoft Symdiff.
We propose a notion of procedure equivalence which is useful for such
heap manipulating procedures. Based on isomorphism between parts of
stores, our definition of procedure equivalence is flexible enough to
allow procedures with different orders and amounts of memory
allocation to be considered equivalent. Pairs of procedures that make
different rearrangements of existing objects can be equivalent.
Knowledge about procedure equivalence can be used modularly in
non-equivalent calling contexts. We are interested in programs that
include non-deterministic allocation, unbounded recursion, and
unbounded heap updates.
We are building a modular equivalence verification tool which uses the
Microsoft Boogie intermediate verification language. A naive encoding
of procedure equivalence would require the verification tool to
produce a witness to the store isomorphism after procedure calls,
which is challenging. We have developed several sound approximations
that help avoid the need to determine the isomorphism. We have proved
that it is sound to assume that when equivalent procedures are called
in an isomorphic manner, that the effects of the calls are equal.