SMT solving for strings: an overview
Speaker:
Philipp Ruemmer
Date and Time
Friday, Oct 12th, 2018 at 14:15.
Location
Polacksbacken, ITC, room 1213.
Abstract
The recent years have seen a wealth of research on string solvers,
i.e., SMT solvers that can efficiently check satisfiability of
quantifier-free formulas over a background theory of strings and
regular expressions. String solvers can be applied in a variety of
verification approaches, for instance in software model checking to
take care of implication and path feasibility checks; the most
widespread adoption has occurred in the area of security analysis for
languages like JavaScript and PHP, for instance to discover
information leaks or vulnerability to injection attacks. To process
constraints from those domains, it is necessary for string solvers to
handle a delicate combination of (theoretically and practically)
highly challenging operations: concatenation in word equations, to
model assignments in programs; regular expressions or context-free
grammars, to model properties or attack patterns; string length, to
express string manipulation in programs; transduction, to express
sanitisation, escape operations, and replacement operations in
strings; and others. The lecture will explain properties of the
theory, existing and/or successful solver architectures, and also
outline the application of string solvers for security properties.
The talk summarises lectures given at the SAT/SMT/AR Summer School 2018 and the EPIT 2018 summer school.