CertiStr: A Certified String Solver (technical report)

TL;DR

CertiStr is a formally verified string constraint solver that guarantees correctness and efficiently solves a significant portion of string constraints, addressing security-critical issues in string manipulation verification.

Contribution

It introduces a certified, automated string solver implemented in Isabelle/HOL, with a forward-propagation algorithm based on symbolic automata, and demonstrates its effectiveness on standard benchmarks.

Findings

Solves 83.5% of relevant tests within 60 seconds

Achieves 80.4% coverage of the string constraint fragment in benchmarks

Provides a formally verified implementation to reduce bugs in string solvers

Abstract

Theories over strings are among the most heavily researched logical theories in the SMT community in the past decade, owing to the error-prone nature of string manipulations, which often leads to security vulnerabilities (e.g. cross-site scripting and code injection). The majority of the existing decision procedures and solvers for these theories are themselves intricate; they are complicated algorithmically, and also have to deal with a very rich vocabulary of operations. This has led to a plethora of bugs in implementation, which have for instance been discovered through fuzzing. In this paper, we present CertiStr, a certified implementation of a string constraint solver for the theory of strings with concatenation and regular constraints. CertiStr aims to solve string constraints using a forward-propagation algorithm based on symbolic representations of regular constraints as symbolic automata, which returns three results: sat, unsat, and unknown, and is guaranteed to terminate for the string constraints whose concatenation dependencies are acyclic. The implementation has been developed and proven correct in Isabelle/HOL, through which an effective solver in OCaml was generated. We demonstrate the effectiveness and efficiency of CertiStr against the standard Kaluza benchmark, in which 80.4% tests are in the string constraint fragment of CertiStr. Of these 80.4% tests, CertiStr can solve 83.5% (i.e. CertiStr returns sat or unsat) within 60s.