Analyzing web applications requires reasoning about strings and non-strings cohesively. Existing string solvers either ignore non-string program behavior or support limited set of string operations. In this paper, we develop a general purpose string solver, called Z3-str, as an extension of the Z3 SMT solver through its plug-in interface. Z3-str treats strings as a primitive type, thus avoiding the inherent limitations observed in many existing solvers that encode strings in terms of other primitives. The logic of the plug-in has three sorts, namely, bool, int and string. The string-sorted terms include string constants and variables of arbitrary length, with functions such as concatenation, sub-string, and replace. The int-sorted terms are standard, with the exception of the length function over string terms. The atomic formulas are equations over string terms, and (in)-equalities over integer terms. Not only does our solver have features that enable whole program symbolic, static and dynamic analysis, but also it performs better than other solvers in our experiments. The application in remote code execution detection shows that its support of a wide spectrum of string operations is key to reducing false positives.

Yunhui Zheng, Xiangyu Zhang and Vijay Ganesh
Z3-str: A Z3-Based String Solver for Web Application Analysis
ESEC/FSE 2013

Download Z3-str (Last update: 2013-06-02)


Z3-str is a string theory plug-in built on the powerful Z3 SMT solver.

Z3-str is implemented using a Linux build of Z3 4.1, which is a version before Z3 became open-source. However, the download link for the Linux build of Z3 4.1 on Z3's old website seems gone.

Instead, our implementation can be built with Z3 4.1.1. The source code of version 4.1.1 is available at Z3's new official web site.

Note: We are still trying to optimize z3-str. If z3-str does not behave as expected, we appreciate very much if you could send the constraint input(s) to us.


What are in the tarball:

How To Use: