CertiStr: A Certified String Solver
Distinguished Paper AwardRemote
Theories over strings are one of 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 available operations. This has led to a plethora of bugs in implementation, which in the past 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 theory 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. Among these 80.4% tests, CertiStr can solve 83.5% of them (i.e. CertiStr returns sat or unsat) within 60s.
Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00
Proof Infrastructure, Rewriting and Automated ReasoningCPP at Salon III
Chair(s): Steve Zdancewic University of Pennsylvania
|CertiStr: A Certified String SolverDistinguished Paper AwardRemote|
Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Micha Schrader Technische Universität KaiserslauternDOI Pre-print Media Attached
|Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo RewritingRemote|
Michael Färber Universität Innsbruck, AustriaDOI Pre-print Media Attached File Attached
|An Extension of the Framework Types-To-Sets for Isabelle/HOLRemote|
CPPPre-print Media Attached
|A Drag-and-Drop Proof TacticRemote|
Benjamin Werner Ecole polytechnique, Pablo Donato Ecole polytechnique, Pierre-Yves Strub Ecole PolytechniqueDOI Pre-print Media Attached