Soteria: Efficient Symbolic Execution as a Functional Library

TL;DR

Soteria introduces a functional library for building source-language specific symbolic execution engines directly, improving performance, accuracy, and feature support over traditional intermediate language-based approaches.

Contribution

It presents Soteria, a lightweight OCaml library enabling direct, source-language semantics-based symbolic execution engines, demonstrated with Rust and C, outperforming existing tools.

Findings

Soteria-based Rust engine supports Tree Borrows, a complex aliasing model.

Soteria C engine is compositional and competitive with state-of-the-art tools.

Theoretical foundations of Soteria are formalized and proven sound.

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.