Combining Static and Dynamic Program Analysis Techniques for Checking Relational Properties

Die vorliegende Dissertation ist im Bereich der formalen Verifikation von Software angesiedelt.
Sie behandelt die Überprüfung relationaler Eigenschaften von Computerprogrammen, d.h. solche Eigenschaften, die zwei oder mehr Programmausführungen betrachten.
Die Dissertation konzentriert sich auf zwei spezifische relationale Eigenschaften: (1) Nichtinterferenz und (2) ob ein Programm ein Slice eines anderen Programms ist.
Die Nichtinterferenz-Eigenschaft besagt, dass die Ausführung eines Programms mit den gleichen öffentlichen Eingaben die gleichen öffentlichen Ausgaben produziert und dies unabhängig von den geheimen Eingaben (z.B. ... mehreines Passworts) ist.
Das bedeutet, dass die geheimen Eingaben die öffentlichen Ausgaben nicht beeinflussen.
Programm-Slicing ist eine Technik zur Reduzierung eines Programms durch das Entfernen von Programmbefehlen, sodass ein spezifizierter Teil des Programmverhaltens erhalten bleibt, z.B. der Wert einer Variablen in einer Instruktion in dem Programm.

Die Dissertation stellt Frameworks zur Verfügung, die es dem Nutzer ermöglichen, die obigen zwei Eigenschaften für ein gegebenes Programm zu analysieren. Die Dissertation erweitert den Stand der Technik in dem Bereich der Verifikation relationaler Eigenschaften, indem sie einerseits neue Ansätze zur Verfügung stellt und andererseits bereits existierende Ansätze miteinander kombiniert. Die Dissertation enthält jeweils einen Teil für die behandelten zwei relationalen Eigenschaften.

$\textbf{Nichtinterferenz.}$
Das Framework zur Überprüfung der Nichtinterferenz stellt neue Ansätze für die automatische Testgenerierung und für das Debuggen des Programms zur Verfügung und kombiniert diese mit Ansätzen, die auf deduktiver Verifikation und Programmabhängigkeitsgraphen basieren.
Der erste neue Ansatz ermöglicht die automatische Generierung von Nichtinterferenz-Tests. Er ermöglicht dem Nutzer, nach Verletzungen der Nichtinterferenz-Eigenschaft im Programm zu suchen und stellt zudem ein für relationale Eigenschaften passendes Abdeckungskriterium für die generierten Test-Suites zur Verfügung.
Der zweite neue Ansatz ist ein relationaler Debugger zur Analyse von Nichtinterferenz-Gegenbeispielen. Er verwendet bekannte Konzepte des Programm-Debuggens und erweitert diese für die Analyse relationaler Eigenschaften.
Um den Nutzer beim Beweisen der Nichtinterferenz-Eigenschaft zu unterstützen, kombiniert das Framework einen auf Programmabhängigkeitsgraphen basierenden Ansatz mit einem auf Logik basierenden Ansatz, der einen Theorembeweiser verwendet.
Auf Programmabhängigkeitsgraphen basierende Ansätze berechnen die Abhängigkeiten zwischen den unterschiedlichen Programmteilen und überprüfen, ob die öffentliche Ausgabe von der geheimen Eingabe abhängt.
Im Vergleich zu logik-basierten Ansätzen skalieren programmabhängigkeitsgraphen-basierte Ansätze besser.
Allerdings, können sie Fehlalarme melden, da sie die Programmabhängigkeiten überapproximieren.
Somit bestehen zwei weitere Beiträge des Frameworks in Kombinationen von programmabhängigkeitsgraphen- und logik basierten Ansätzen:
(1) der programmabhängigkeitsgraphen basierte Ansatz vereinfacht das Programm, das danach vom logik basierten Ansatz überprüft wird und
(2) der logik basierte Ansatz beweist, dass einige vom Programmabhängigkeitsgraphen-basierten Ansatz berechnete Abhängigkeiten Überapproximationen sind und aus der Analyse entfernt werden können.


$\textbf{Programm-Slicing.}$
Der zweite Teil der Dissertation behandelt ein Framework für das automatische Programm-Slicing.
Während die meisten zum Stand der Technik gehörenden Slicing-Ansätze nur eine syntaktische Programmanalyse durchführen, betrachtet dieses Framework auch die Programmsemantik und kann dadurch mehr Programmbefehle entfernen.
Der erste Beitrag des Frameworks besteht aus einem Ansatz zur relationalen Verifikation, der erweitert wurde, um die Korrektheit eines Programm-Slice nachzuweisen, d.h. dass es das spezifizierte Verhalten des Originalprogramms bewahrt.
Der Vorteil der Benutzung relationaler Verifikation ist, dass sie auf zwei ähnlichen Programmen automatisch läuft -- was bei einem Slice-Kandidaten und Originalprogramm der Fall ist.
Somit, anders als bei den wenigen zum Stand der Technik gehörenden Ansätzen, die die Programmsemantik betrachten, ist dieser Ansatz automatisch.
Der zweite Beitrag des Frameworks besteht aus einer neuen Strategie zur Generierung von Slice-Kandidaten durch durch die Verfeinerung von dynamischen Slices (für eine Eingabe gültigen Slices) mithilfe von der relationalen Verifikation gelieferte Gegenbeispiele.

The topic of this thesis belongs to the research area of formal software verification. It deals with checking relational properties of computer programs (i.e., properties that consider two or more program executions). The thesis focuses on two specific relational properties: (1) noninterference and (2) whether a program is a correct slice of another. The noninterference property states that running a program with the same public input values will always produce the same public outputs, regardless of the secret inputs (e.g., a password). This means that the secret inputs do not influence public outputs. ... mehrProgram slicing is a technique to reduce a program by removing statements from it while preserving a specified part of its behavior, such as the value of a variable at a program location.

The thesis provides frameworks that allow the user to analyze the two properties for a given program. The thesis advances the state of the art in the area of formal verification of relational properties by providing novel approaches for the analysis on the one hand and by combining existing approaches on the other hand. The thesis contains two parts, each handling one of the two relational properties.

$\textbf{Noninterference.}$
The framework for checking noninterference provides new approaches both for automatic test generation and program debugging, and it combines these new approaches with approaches based on deductive verification and dependency graphs. The first new approach provided by this framework allows for the automatic generation of noninterference tests. It allows the user to search for violations of the noninterference property, and it also provides a coverage criterion for the generated test suites that is appropriate for relational properties. The second new approach provided by the framework is a relational debugger for analyzing noninterference counterexamples. It employs well-known concepts from program debugging, and it extends them for relational program analysis. To support the user in proving a noninterference property, the framework combines an approach based on dependency graphs with a logic-based approach that uses a theorem prover. Dependency-graph-based approaches compute the dependencies between various program parts and check whether the public output depends on the secure input. Compared with logic-based approaches, dependency-graph-based approaches scale better. However, because they over-approximate the dependencies in a program, they may report false alarms. Two further contributions of the framework are thus represented by two combinations of the logic-based and dependency-graph-based approaches: (1) the dependency-graph-based approach simplifies the program that is checked by logic-based approach, and (2) the logic-based approach proves that certain dependencies computed by the dependency-graph-based approach are over-approximations and can be discarded from the analysis.

$\textbf{Program slicing.}$
The second part of the thesis discusses a framework for automatic program slicing. Whereas most state-of-the-art slicing approaches only perform a syntactical analysis of the program, this framework also considers the semantics of the program and can remove more statements from a program. The first contribution of the slicing framework consists of a relational verification approach that was adapted to check whether a slice is valid, (i.e., whether it preserves the specified behavior of the original program). The advantage of using relational verification is that it works automatically for two similar programs---which is the case when considering a slice candidate and an original program. Thus, unlike the few state-of-the-art slicing approaches that consider the semantics of the program, our approach is automatic. The second contribution of this framework is a new strategy for generating slice candidates by refining dynamic slices (i.e., slices which are valid for a single input) by using the counterexamples provided by the relational verifier.