Symbolic execution (SE) is a program analysis technique that executes the program with symbolic inputs. In modern SE engines, when the analysis of a given program is exhaustive, the analyzed program is typically considered safe, i.e., free of bugs, but no formal guarantees are provided to support this. Rather than aiming for a formally verified SE engine that will provide such guarantees, which is challenging, we propose a systematic approach where each individual analysis additionally outputs a formal safety proof that validates the symbolic computations that were carried out.
Our approach consists of two main components: A formal framework connecting concrete and symbolic semantics, and an instrumentation of the SE engine that generates formal safety proofs based on this framework. We showcase our approach by implementing a KLEE-based prototype that operates on a subset of LLVM IR with integers and generates proofs in Coq.
Our preliminary experiments show that our approach generates proofs that have reasonable validation times, while the instrumentation incurs only a minor overhead on the SE engine.
In addition, during the implementation of our prototype, we found previously unknown semantic implementation issues in KLEE.