Flatten and conquer: a framework for efficient analysis of string constraints

• https://dl.acm.org/citation.cfm?doid=3062341.3062384

Automata Theory, Formal Verification, String Equation

We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.

It has recently transpired that for verification and, importantly, security analysis of software such as web applications, written in scripting languages such as PHP and JavaScript, but also for analysis for Java, C++, C#,... programs, reasoning about the string data type is crucial.
Our work belongs among a wide range of recent works on string analysis---design and effective/efficient analysis of languages of string constraints suitable for analysis of such programs. String program analysis presents a difficult challenge in that it strives to reach contending objectives, expressiveness on the borders of decidability and high effectiveness/efficiency. Heuristics play a crucial role in all current promising angles of attack. This paper present a fresh approach, also based on a heuristic, which is rather unique among the multitude of the other works and has a very competitive results. It is based on a novel idea of abstracting solutions of string constraints as so called flat languages. Flat languages are less expressive than regular languages, but can be represented and manipulated extremely efficiently, and allow for an easy combination of regular, rational, length and other constraints over strings needed in analysis of string programs. As we show experimentally, the flat abstraction in a combination with counterexample guided refinement is also almost always enough to (dis)prove string constraints that appear in practice. It hence represents a radically new and very promising angle of approaching this hard problem.


5 citations found by SCOPUS, 12 by Google Scholar (both without autocitations)