Relational Symbolic Execution

TL;DR

This paper introduces RelSym, a relational symbolic execution engine that extends classical symbolic execution to verify relational properties involving two program runs, aiding security, privacy, and optimization analyses.

Contribution

It generalizes symbolic execution to support relational specifications, enabling analysis of properties about multiple program executions on related inputs.

Findings

Supports verification of relational properties in programs with arrays and loops

Enables interactive refutation and proof of relational properties

Applicable to security, privacy, and optimization scenarios

Abstract

Symbolic execution is a classical program analysis technique used to show that programs satisfy or violate given specifications. In this work we generalize symbolic execution to support program analysis for relational specifications in the form of relational properties - these are properties about two runs of two programs on related inputs, or about two executions of a single program on related inputs. Relational properties are useful to formalize notions in security and privacy, and to reason about program optimizations. We design a relational symbolic execution engine, named RelSym which supports interactive refutation, as well as proving of relational properties for programs written in a language with arrays and for-like loops.