A Solver for a Theory of Strings and Bit-vectors

TL;DR

This paper introduces Z3strBV, a native string and bit-vector solver that improves efficiency over existing methods, enabling effective analysis of C/C++ code for security vulnerabilities and overflows.

Contribution

The paper presents Z3strBV, a decision procedure for a combined string and bit-vector theory, with optimizations and experimental validation demonstrating superior performance.

Findings

Z3strBV outperforms reduction-based solvers in efficiency.

Decidability of the combined string and bit-vector theory is proven.

Successfully detects real-world security vulnerabilities.

Abstract

We present a solver for a many-sorted first-order quantifier-free theory $T_{w,bv}$ of string equations, string length represented as bit-vectors, and bit-vector arithmetic aimed at formal verification, automated testing, and security analysis of C/C++ applications. Our key motivation for building such a solver is the observation that existing string solvers are not efficient at modeling the string/bit-vector combination. Current approaches either reduce strings to bit-vectors and use a bit-vector solver as a backend, or model bit-vectors as natural numbers and use a solver for the combined theory of strings and natural numbers. Both these approaches are inefficient for different reasons. Modeling strings as bit-vectors destroys structure inherent in string equations thus missing opportunities for efficiently deciding such formulas, and modeling bit-vectors as natural numbers is known to be inefficient. Hence, there is a clear need for a solver that models strings and bit-vectors natively. Our solver Z3strBV is a decision procedure for the theory $T_{w,bv}$ combining solvers for bit-vector and string equations. We demonstrate experimentally that Z3strBV is significantly more efficient than reduction of string/bit-vector constraints to strings/natural numbers. Additionally, we prove decidability for the theory $T_{w,bv}$. We also propose two optimizations which can be adapted to other contexts. The first accelerates convergence on a consistent assignment of string lengths, and the second, dubbed library-aware SMT solving, fixes summaries for built-in string functions (e.g., {\tt strlen} in C/C++), which Z3strBV uses directly instead of analyzing the functions from scratch each time. Finally, we demonstrate experimentally that Z3strBV is able to detect nontrivial overflows in real-world system-level code, as confirmed against 7 security vulnerabilities from CVE and Mozilla database.