Publication
Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
Sören Tempel; Tobias Brandt; Christoph Lüth; Christian Dietrich; Rolf Drechsler
In: Design, Automation and Test in Europe Conference (DATE). Design, Automation & Test in Europe (DATE-2025), March 31 - April 2, Lyon, France, 2025.
Abstract
Symbolic execution is an SMT-based software verification and testing technique. Symbolic execution requires
tracking performed computations during software simulation
to reason about branches in the software under test. The
prevailing approach on symbolic execution of binary code tracks
computations by transforming the code to be tested to an
architecture-independent intermediate representation (IR) and
then symbolically executes this IR. However, the resulting IR
must be semantically equivalent to the binary code, making this
process complex and error-prone. The semantics of the binary
code are specified by the targeted instruction set architecture
(ISA), commonly given in natural language and requiring a
manual implementation of the transformation to an IR. In recent
years, the use of formal languages to describe ISA semantics in
a machine-readable way has gained increased popularity. We
investigate the utilization of such formal semantics for symbolic
execution of binary code, achieving an accurate representation
of instruction semantics. We present a prototype for the RISC-V
ISA and conduct a case study to demonstrate that it can be easily
extended to additional instructions. Furthermore, we perform
an experimental comparison with prior work which resulted
in the discovery of five previously unknown bugs in the ISA
implementation of the popular IR-based symbolic executor angr