A Model Counter For Constraints Over Unbounded Strings

Model counting is the problem of determining the number of so-lutions that satisfy a given set of constraints. Model counting has numerous applications in the quantitative analyses of program exe-cution time, information flow, combinatorial circuit designs as well as probabilistic reasoning. We present a new approach to model counting for structured data types, specifically strings in this work. The key ingredient is a new technique that leverages generating functions as a basic primitive for combinatorial counting. Our tool SMC which embodies this approach can model count for con-straints specified in an expressive string language efficiently and precisely, thereby outperforming previous finite-size analysis tools. SMC is expressive enough to model constraints arising in real-world JavaScript applications and UNIX C utilities. We demon-strate the practical feasibility of performing quantitative analyses arising in security applications, such as determining the compar-ative strengths of password strength meters and determining the information leakage via side channels. 1