guest ::
Symbolic execution and program synthesis : a general methodology for software verification = Symbolische Auswertung und Programmsynthese : Ein allgemeiner Ansatz zur Software-Verifikation
2019
Dissertation, RWTH Aachen University, 2019
Veröffentlicht auf dem Publikationsserver der RWTH Aachen University
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
;
Tag der mündlichen Prüfung/Habilitation
2019-01-28
Online
DOI: 10.18154/RWTH-2019-01779
URL: http://publications.rwth-aachen.de/record/755346/files/755346.pdf
Einrichtungen
- Lehr- und Forschungsgebiet Informatik 2 (Programmiersprachen und Verifikation) (121420)
- Fachgruppe Informatik (120000)
Inhaltliche Beschreibung (Schlagwörter)
complexity analysis (frei) ; program synthesis (frei) ; software verification (frei) ; symbolic execution (frei) ; termination analysis (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Unser Anliegen ist die Korrektheit von Software und wir präsentieren einen allgemeinen Ansatz zur Verifikation von Programmeigenschaften in nahezu beliebigen Programmiersprachen. Dieser Ansatz besteht aus zwei Schritten: Zuerst führen wir das zu analysierende Programm symbolisch aus, um eine endliche Überapproximation aller möglichen Programmläufe für alle möglichen Eingaben zu erhalten. Wir nennen diese Überapproximation einen symbolischen Auswertungsgraphen (symbolic execution graph). Im Unterschied zu den meisten existierenden Ansätzen, welche abstrakte Interpretationen nutzen, wird die Konstruktion eines solchen Graphen stark durch das zu analysierende Programm gesteuert, anstatt programmunabhängige Widening-Operatoren zu nutzen. Anschließend synthetisieren wir aus dem Graphen Programme in einfachen Programmiersprachen, welche die wesentlichen Programmeigenschaften ausdrücken, die wir analysieren wollen. Auf diese Weise wird die nachfolgende Analyse dieser Programmeigenschaften auf Grundlage der synthetisierten Programme substanziell vereinfacht. Wir nutzen also Synergien zwischen Techniken zur Programmanalyse und zur Programmsynthese, um mächtige Verifikationsverfahren zu entwickeln. Obwohl die durch den symbolischen Auswertungsgraphen und die nachfolgende Programmsynthese erzeugte Überapproximation zu einem Verlust an Präzision führen kann, zeigen unsere empirischen Untersuchungen, dass die in dieser Arbeit eingeführten Abstraktionen in der Praxis präzisere Ergebnisse als andere existierende Ansätze liefern und dabei immer noch effiziente Analysen erlauben (insbesondere durch die Vereinfachung während der Programmsynthese und durch die Nutzung mächtiger existierender Analysetechniken für die einfachen Zielsprachen). Daher erwies sich unser Ansatz als äußerst erfolgreich in den führenden internationalen Wettbewerben im Bereich unserer Analysen. Wir wenden unseren Ansatz an, um Eindeutigkeit (determinacy), Terminierung und Laufzeitkomplexitätsschranken von Prolog Programmen, Speicherintegrität (memory safety) und Terminierung von LLVM Programmen (kompiliert aus C Programmen) sowie Freiheit von Deadlocks und Livelocks in nebenläufigen imperativen Programmen mit gemeinsamem Speicher zu beweisen. Außerdem finden wir mit unserem Ansatz eine Lösung des Behavior Composition Problems. Hierbei handelt es sich um das Programmsyntheseproblem, ein deterministisches Zielverhalten mit einer Menge nicht-deterministischer Agenten (welche sich in einer nicht-deterministischen Umwelt bewegen) verlässlich zu realisieren. Unser Ansatz ist besonders für die Analyse "universeller" Eigenschaften geeignet, welche für alle Programmauswertungen gelten müssen (z.B. Terminierung, Speicherintegrität oder obere Laufzeitschranken). In solchen Fällen zeigen unsere empirischen Untersuchungen, dass unser Ansatz alle früheren existierenden Ansätze übertrifft. Obwohl unser Ansatz zu einem gewissen Grad auch dazu eingesetzt werden kann, "existenzielle" Eigenschaften zu analysieren, welche nur für manche Programmauswertungen gelten müssen (z.B. die Existenz von Fehlern wie Nicht-Terminierung oder Verletzungen der Speicherintegrität), ist durch die inhärente Überapproximation zusätzlicher Aufwand nötig, um unseren Ansatz für solche Analysen korrekt anzuwenden. Im Prinzip können wir mit unserem Ansatz Kandidaten finden, welche die gesuchten existenziellen Eigenschaften erfüllen, müssen aber deren Erreichbarkeit separat beweisen. Viele unserer Beiträge wurden im Verifikationstool AProVE implementiert und durch umfangreiche Experimente empirisch evaluiert. Unsere Beiträge verbessern den Stand der Technik bei der automatischer Programmverifikation und zeigen eine Richtung für die Entwicklung zukünftiger Verifikationstechniken an.We are concerned with the correctness of software and present a general methodology for verifying properties of programs in virtually any programming language. This methodology consists of two stages: First, we symbolically execute the program in question to obtain a finite over-approximation of all possible program executions for all possible inputs. We call this over-approximation a symbolic execution graph. The difference of this graph compared to most existing approaches using abstract domains is that its construction is strongly guided by the analyzed program rather than using program-independent widening operators. Afterwards, we synthesize programs in simple programming languages from the symbolic execution graph capturing the essence of the program properties that we want to analyze. Thus, the subsequent analysis of these properties on the synthesized programs is substantially simplified. So we exploit synergies between program analysis and synthesis techniques to obtain powerful verification approaches. Although the over-approximation induced by the symbolic execution graph and subsequent program synthesis might lose precision, our empirical evaluations demonstrate that the abstract domains introduced in this thesis are more precise than other existing domains while still allowing efficient analyses in practice (in particular due to the simplification obtained by program synthesis and the exploitation of powerful existing analysis techniques for the simple target languages). Hence, our methodology proved to be very successful in the leading international competitions in the fields of our analyses. We apply our methodology to prove determinacy, termination, and upper runtime complexity bounds of Prolog programs, memory safety and termination of LLVM programs (compiled from C programs), deadlock and livelock freedom of concurrent imperative programs with shared memory, and to provide a solution to the Behavior Composition Problem, a program synthesis problem trying to reliably achieve a deterministic target behavior with a set of non-deterministic agents acting in a non-deterministic environment. Our methodology is particularly useful for analyzing ``universal'' properties that hold for all program executions (e.g., termination, memory safety, or upper bounds on runtime complexity). Here, our empirical results show that our approach clearly outperforms any previous existing approach. While our methodology can to some extent also be applied to analyze "existential" properties that only need to hold for some program executions (e.g., proving the presence of defects like non-termination or violations of memory safety), additional effort is necessary to make our approach sound for such analyses due to the over-approximation inherently involved. In principle, we can detect candidates satisfying such existential properties in our symbolic execution graph but must prove their feasibility separately. Many of our contributions have been implemented in the verification tool AProVE and empirically evaluated by extensive experiments. Our contributions advance the state of the art in automated program verification and offer a guideline for creating future verification techniques following our methodology.
OpenAccess: 
PDF
(additional files)
Dokumenttyp
Dissertation / PhD Thesis
Format
online
Sprache
English
Externe Identnummern
HBZ: HT020003000
Interne Identnummern
RWTH-2019-01779
Datensatz-ID: 755346
Beteiligte Länder
Germany
