Model counting of string constraints for probabilistic symbolic execution

Abstract

Probabilistic symbolic execution is a static analysis technique aiming at quantifying the probability of a target event occurring during a program execution; it exploits symbolic execution to identify the conditions on the program inputs leading to the occurrence of the target event and then model counting to quantify their probability. While efficient methods exist for model counting of numeric constraints, only limited results have been obtained for counting string constraints. The constraints are indeed first encoded in a corresponding accepting automaton; then the number of accepting paths of the automaton is quantified via a convenient generating function. The encoding in the form of automata limits the expressiveness of the formalism used for constraint specification to constructs mappable into automata, for an exact model count. Furthermore, the encoding of disjunctions requires the parallel composition of the automata representing the disjuncts, leading to an exponential growth in the size of the resulting automata. This thesis introduces the usage of SMT solvers to count the models of a string constraint by leveraging a standard smtlib interface. Several algorithms for both exact and approximate model counting of string constraints are defined and compared. The different solutions are implemented on top of the SMT solver CVC4 and evaluated on a set of established benchmarks, demonstrating the increased expressiveness with respect to previous approaches and improved performance on several classes of problems.

Probabilistic Symbolic Execution ist eine statische Analysetechnik, um die Eintrittswahrscheinlichkeit eines Ereignisses in der Programmausführung zu bestimmen. Es verwendet dazu eine Kombination der herkömmlichen Symbolic Execution und dem Zählen von Modellen. Symbolic Execution extrahiert die Pfadbedingungen, die notwendig sind, um zu dem Ereignis zu gelangen. Indem man die Anzahl Möglichkeiten berechnet, diese Bedingungen zu erfüllen, kann die Eintrittswahrscheinlichkeit des Ereignisses bestimmt werden. Während für das Zählen von Modellen für numerische Bedingungen schon effiziente Methoden publiziert wurden, existieren für das Zählen von Bedingungen mit Zeichenketten zurzeit nur eingeschränkte Möglichkeiten. Die existierenden Techniken basieren auf der Konstruktion von endlichen Zustandsautomaten, deren Sprache die erfüllenden Zeichenketten akzeptieren. Die Anzahl Modelle ergibt sich durch die Bestimmung der Anzahl akzeptierender Pfade in diesen Automaten. Diese Reduktion des Problems schränkt die Teilmenge an formulierbaren Bedingungen ein, für welche die exakte Anzahl Modelle bestimmt werden kann. Des Weiteren führen komplexe Bedingungen mit Verkettung von Disjunktionen zu einer Zustandsexplosion im konstruierten Automaten. Diese Thesis stellt ein Verfahren vor, das mit Hilfe von sogenannten SMT Solvern, die Anzahl Modelle von Bedingungen mit Zeichenketten bestimmen kann. Es wurden mehrere Algorithmen entwickelt, die unter Verwendung einer standardisierten SMT Solver Schnittstelle die exakten also auch approximativen Mengen an Modellen berechnen können. Als Implementierungsgrundlage wurde der SMT Solver CVC4 verwendet. Die Evaluation des entwickelten Forschungsprototyps mit etablierten Benchmarktests zeigt die erweiterte Ausdrucksfähigkeit der SMT-basierenden Verfahren gegenüber den existierenden Ansätzen. Außerdem können bestimmte Problemklassen nun effizienter gelöst werden.