A Solver for a Theory of Strings and Bit-vectors

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...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2016-05
Main Authors: Subramanian, Sanu, Murphy Berzish, Zheng, Yunhui, Tripp, Omer, Ganesh, Vijay
Format: Article
Language:English
Subjects:
C++ (programming language)
Decision theory
Mathematical models
Modelling
Number theory
Security
Solvers
Strings
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422