2016/05/30 by Sanu Subramanian, Murphy Berzish, Subramanian, Sanu +7
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Security and Verification in Computing #Software Testing and Debugging Techniques #Web Application Security Vulnerabilities
paper · pdf · doi:10.48550/arxiv.1605.09446
openalex publication_date 2016/05/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a solver for a many-sorted first-order quantifier-free theory Tw,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 Tw,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 Tw,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.