Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis
summary
First formalization of symbolic finite transducers and core algorithms in Isabelle/HOL, using an abstract Boolean-algebra label layer plus refinement to concrete structures (red‑black trees, hashmaps) and refinement to intervals for execution. Applies to web sanitizer verification (model sanitizers as SFTs, intersect with unsafe regexes) and to SMT-style string solving with replace‑all; emptiness checks run at verification <0.02s, and the implementation outperforms Ostrich/CVC5 on many replace‑all benchmarks.
AI-written summary · about
chapters (15)
- 0:00String sanitization motivation
- 3:14Formal verification of sanitizers
- 4:59Symbolic finite transducers
- 8:30Definition of symbolic transducers
- 10:20Product operation for verification
- 12:49Refinement proof in Isabelle/HOL
- 15:14Sanitizer verification with transducers
- 16:39Composition of sanitizers
- 17:44Real-world HTML sanitizer model
- 18:50Evaluation on sanitizers
- 19:12Extending string servers
- 20:42Performance comparison
- 21:27Expressiveness comparison
- 22:30Summary and future work
- 22:54Q&A: SMT solvers comparison
related talks
19mCertiStr: A Certified String Solver
32mSymbolic analysis by using folding narrowing with irreducibility and SMT constra...
31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...
58mAutomating Relational Verification of Infinite-State Programs
28mForward Symbolic Execution for Trustworthy Automation of Binary Code Verification
28mProving Memory Access Violations in Isabelle/HOL
15mProving LTL Properties of Bitvector Programs and Decompiled Binaries
19mVerifying non-terminating programs with IO in F*