Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Soteria: Efficient Symbolic Execution as a Functional Library

Sacha-Élie Ayoun, Opale Sjöstedt, Azalea Raad

TL;DR

Soteria tackles the trade-offs of IL-based symbolic execution by arguing for language-specific SE engines built directly over source semantics. The paper introduces Soteria, an OCaml library with a monadic SE interface that enables constructing engines like Soteriarust for Rust (including Tree Borrows) and Soteriac for C (WPST and bi-abduction) while maintaining soundness proofs and practical performance. Through formalisation, it shows that symbolic interpreters built on Soteria can achieve competitive or superior results to state-of-the-art IL-based tools, with demonstrations across real benchmarks and real-world code. The results suggest that direct-language SE, coupled with modular solvers and reusable data structures, can yield scalable, accurate, and configurable analyses with robust logging and verification guarantees, advancing the practicality of symbolic testing for systems languages. The work lays a foundation for broader language coverage (e.g., Python, concurrency) and solver automation, highlighting the potential of monadic, compositional SE frameworks over traditional IL approaches.

Abstract

Symbolic execution (SE) tools often rely on intermediate languages (ILs) to support multiple programming languages, promising reusability and efficiency. In practice, this approach introduces trade-offs between performance, accuracy, and language feature support. We argue that building SE engines \emph{directly} for each source language is both simpler and more effective. We present Soteria, a lightweight OCaml library for writing SE engines in a functional style, without compromising on performance, accuracy or feature support. Soteria enables developers to construct SE engines that operate directly over source-language semantics, offering \emph{configurability}, compositional reasoning, and ease of implementation. Using Soteria, we develop Soteria$^{\text{Rust}}$, the \emph{first} Rust SE engine supporting Tree Borrows (the intricate aliasing model of Rust), and Soteria$^{\text{C}}$, a compositional SE engine for C. Both tools are competitive with or outperform state-of-the-art tools such as Kani, Pulse, CBMC and Gillian-C in performance and the number of bugs detected. We formalise the theoretical foundations of Soteria and prove its soundness, demonstrating that sound, efficient, accurate, and expressive SE can be achieved without the compromises of ILs.

Soteria: Efficient Symbolic Execution as a Functional Library

TL;DR

Soteria tackles the trade-offs of IL-based symbolic execution by arguing for language-specific SE engines built directly over source semantics. The paper introduces Soteria, an OCaml library with a monadic SE interface that enables constructing engines like Soteriarust for Rust (including Tree Borrows) and Soteriac for C (WPST and bi-abduction) while maintaining soundness proofs and practical performance. Through formalisation, it shows that symbolic interpreters built on Soteria can achieve competitive or superior results to state-of-the-art IL-based tools, with demonstrations across real benchmarks and real-world code. The results suggest that direct-language SE, coupled with modular solvers and reusable data structures, can yield scalable, accurate, and configurable analyses with robust logging and verification guarantees, advancing the practicality of symbolic testing for systems languages. The work lays a foundation for broader language coverage (e.g., Python, concurrency) and solver automation, highlighting the potential of monadic, compositional SE frameworks over traditional IL approaches.

Abstract

Symbolic execution (SE) tools often rely on intermediate languages (ILs) to support multiple programming languages, promising reusability and efficiency. In practice, this approach introduces trade-offs between performance, accuracy, and language feature support. We argue that building SE engines \emph{directly} for each source language is both simpler and more effective. We present Soteria, a lightweight OCaml library for writing SE engines in a functional style, without compromising on performance, accuracy or feature support. Soteria enables developers to construct SE engines that operate directly over source-language semantics, offering \emph{configurability}, compositional reasoning, and ease of implementation. Using Soteria, we develop Soteria, the \emph{first} Rust SE engine supporting Tree Borrows (the intricate aliasing model of Rust), and Soteria, a compositional SE engine for C. Both tools are competitive with or outperform state-of-the-art tools such as Kani, Pulse, CBMC and Gillian-C in performance and the number of bugs detected. We formalise the theoretical foundations of Soteria and prove its soundness, demonstrating that sound, efficient, accurate, and expressive SE can be achieved without the compromises of ILs.

Paper Structure

This paper contains 75 sections, 4 theorems, 15 equations, 15 figures.

Table of Contents

  1. Introduction
  2. Argument 1: Design once, use often!
  3. Argument 2: Prove once, use often!
  4. The Soteria Framework
  5. Contributions and Outline
  6. Overview: Build Your Own Symbolic Execution Engine for Lang over Soteria
  7. Preliminary: Concrete Monadic Interpreter
  8. Symbolic Interpreter with Soteria
  9. The Soteria Symex Module
  10. Symbolic Values and Solvers
  11. Guarantees
  12. Implementation
  13. Solver and Values
  14. The Value Interface
  15. The Solver Interface
  16. ...and 60 more sections

Key Result

theorem 1

For all $f, \widehat{f}, g, \widehat{g}, a, \widehat{a}, b, \widehat{b}$ and all modes $m \in \{ \mathsf{OX}\xspace, \mathsf{UX}\xspace \}$:

Figures (15)

  • Figure 1: Overview of the Soteria architecture
  • Figure 2: The Soteriarust architecture
  • Figure 3: The Kani and Miri test suite results (above); number of tests passed over time by each tool (below)
  • Figure 4: Example of a biased test in the Kani test suite, and a modification to make it verifiable by Soteriarust
  • Figure 5: The DS suite results with a timeout of 10s (above); tests passed over time by each tool (below).
  • ...and 10 more figures

Theorems & Definitions (9)

  • Remark 1
  • theorem 1: Soundness Preservation
  • definition 1: Symbolic Execution Monad
  • lemma 1: Symbolic execution monad: Monad Laws
  • definition 2: Symbolic branch
  • definition 3: $\mathsf{OX}\xspace$ soundness
  • definition 4: $\mathsf{UX}\xspace$ soundness
  • theorem 2: Soundness Preservation: Composition
  • theorem 3: Soundness Preservation: Branching