Algorithmic Verification of String-Manipulating Programs
Abstract:
Strings are among the most fundamental and commonly used data types in modern programming languages. Heavy string manipulations in programs often lead to mistakes, some of which could have serious security consequences (e.g. cross-site scripting). This gives rise to the currently active research area of algorithmic verification of string-manipulating programs. As is standard in software model checking, one crucial problem is to come up with an appropriate string theory and a decision procedure for it. This is because in theory a software model checker could then use standard methods (e.g. symbolic execution) to lift the decision procedure from formulas to programs. In this talk, I will describe the challenges of the design of a good string theory and decision procedure for the theory, as well as some existing attempts towards them, including our framework of “straight-line logic” and OSTRICH string solver. In particular, this is a tricky problem because there are many string operations that one would like to include as a primitive operation (especially from the point of view of techniques like symbolic execution), but at the same time they easily lead to undecidability.
The results presented came from a series of recent papers (POPL’16, POPL’18, and POPL’19) with Pablo Barcelo, Taolue Chen, Yan Chen, Matthew Hague, Lukas Holik, Petr Janku, Rupak Majumdar, Philipp Ruemmer, and Tomas Vojnar.
Bio:
Anthony Lin is a Professor of Automated Reasoning at Technical University of Kaiserslautern, a Max-Planck Fellow, and a current holder of an ERC Starting Grant. He is interested in developing methods using logic and automata for automatically reasoning about programs. His current interests lie in constraint solving over strings.