Automata-based Model Counting for String Constraints

Most common vulnerabilities in Web applications are due
to string manipulation errors in input validation and sanitization code.
String constraint solvers are essential components of program analysis
techniques for detecting and repairing vulnerabilities that are due to
string manipulation errors. For quantitative and probabilistic program
analyses, checking the satisfiability of a constraint is not sufficient, and it
is necessary to count the number of solutions. In this paper, we present a
constraint solver that, given a string constraint, 1) constructs an automa-
ton that accepts all solutions that satisfy the constraint, 2) generates a
function that, given a length bound, gives the total number of solutions
within that bound. Our approach relies on the observation that, using
an automata-based constraint representation, model counting reduces to
path counting, which can be solved precisely. We demonstrate the effec-
tiveness of our approach on a large set of string constraints extracted
from real-world web applications.