Automatic abstraction for bit vectors using decision procedures

Brauer, Jörg; Kowalewski, Stefan

doi:32806

Automatic abstraction for bit vectors using decision procedures = Automatische Abstraktion von Bitvektoren mittels Entscheidungsprozeduren

Brauer, Jörg (Author)

2013

VerantwortlichkeitsangabeJörg Brauer

ImpressumAachen : Fachgruppe Informatik, RWTH Aachen University 2013

UmfangIV, 207 S. : graph. Darst.

ReiheAachener Informatik-Berichte Technical report / Department of Computer Science, RWTH Aachen ; 2013,14

Zugl.: Aachen, Techn. Hochsch., Diss., 2013

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Kowalewski, Stefan (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2013-09-25

Online
URN: urn:nbn:de:hbz:82-opus-48361
URL: https://publications.rwth-aachen.de/record/229199/files/4836.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Abstrakte Interpretation (Genormte SW) ; Entscheidungsverfahren (Genormte SW) ; Bitvektor (Genormte SW) ; Informatik (frei) ; automatische Abstraktion (frei) ; automatic abstraction (frei) ; abstract interpretation (frei) ; decision procedures (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: F.3.2

Kurzfassung
Diese Dissertation ist im Fachgebiet der abstrakten Interpretation angesiedelt und beschäftigt sich mit der Analyse von Programmen, deren Semantik über endlichen Registern definiert ist. Insbesondere beinhaltet diese Klasse von Programmen ausführbaren Maschinencode, dessen Analyse sich wegen der Komplexität und Anzahl der Operationen anspruchsvoll gestaltet. Eine Herausforderung für korrekte und zugleich präzise abstrakte Interpretation von Maschinencode stellen Transferfunktionen dar, welche die Ausführung aller konkreten Operationen eines Programmes in einer abstrakten Domäne simulieren. Insbesondere müssen Über- und Unterläufe von Registern modelliert werden, um die Korrektheit der Analyse zu gewährleisten. Die in dieser Dissertation vertretene Kernthese ist, dass Transferfunktionen für Sequenzen von Operationen über endlichen Registern präzise und effizient generiert werden können. Diese These steht im Gegensatz zu klassischen Verfahren, welche den Entwurf von Transferfunktionen vornehmlich als manuellen Prozess vorsehen. Um diese These zu untermauern, präsentieren wir einen Ansatz in dem der zeitaufwendige Entwurf von Transferfunktionen entfällt. Im Mittelpunkt unseres Lösungsansatzes steht eine Spezifikation der Semantik einer Sequenz von Operationen in Form von Boolescher Logik. Mit Hilfe von Werkzeugen, welche die Erfüllbarkeit aussagenlogischer Formeln überprüfen, synthetisieren wir aus einer Spezifikation in einem automatischen Prozess Abstraktionen mit maximaler Aussagekraft. Die Praktikabilität dieses Ansatzes zeigen wir für eine Vielzahl numerischer Domänen, welche häufig in der abstrakten Interpretation eingesetzt werden, insbesondere Intervalle, Wertemengen, Oktagone, konvexe Polyeder, arithmetische Kongruenzen, affine Gleichungen und Polynome beschränkten Grades. Hierbei wird die Endlichkeit der Register, welche sich in Über- und Unterläufen manifestiert, automatisch modelliert. Ist die Analyse eines Programms abgeschlossen, so wird von einem Analysewerkzeug unter Umständen eine Warnung ausgegeben, welche einen potentiellen Fehler im analysierten Programm anzeigt. Da abstrakte Interpretation auf Basis von Überapproximation eine Obermenge der erreichbaren Zustände eines Programms berechnet, kann solch eine Warnung unberechtigt sein. Für dieses Szenario präsentieren wir Varianten der vorgestellten Algorithmen, welche vollständige Abstraktionen generieren, so dass sich Garantien über tatsächlich erreichbare Zustände ableiten lassen. Auf dieser Basis können sowohl unberechtigte Warnungen identifiziert als auch Gegenbeispiele generiert werden, welche einen fehlerhaften Pfad anzeigen und somit die zugrundeliegende Warnung validieren.

This dissertation is concerned with abstract interpretation of programs whose semantics is defined over finite machine words. Most notably, the considered class of programs contains executable binary code, the analysis of which turns out demanding due to the complexity and the sheer number of involved operations. Challenging for correct yet precise abstract interpretation of binary code are transfer functions, which simulate the execution of any concrete operation in a program in an abstract domain. Crucially for correctness, over- and underflows need to be supported faithfully. This dissertation argues that transfer functions and abstractions for sequences of operations over finite machine words can precisely and efficiently be generated, which contrasts with classical methods that depend on handcrafted transfer functions. To support this statement, we present an approach that eliminates the time-consuming process of manually deriving transfer functions altogether. The core of our methods are specifications of the concrete semantics of sequences of operations, which are given in propositional Boolean logic. By utilizing SAT and SMT solvers, which can determine satisfiability of Boolean formulae, we show how to automatically synthesize optimal abstractions from such semantic specifications. The practicality of our method is highlighted using abstractions generated for a variety of numerical domains that are frequently used in abstract interpretation. The abstract domains considered in this dissertation are, most notably, intervals, value sets, octagons, convex polyhedra, arithmetical congruences, affine equalities, and polynomials of bounded degree. Importantly, all presented techniques automatically handle finiteness of machine words, which manifests itself in over- and underflows. Once the analysis of a program has terminated, an abstract interpreter often emits a warning that highlights a potential error in the analyzed program. Since abstract interpretation computes an over-approximation of the states reachable in a concrete execution, such a warning may be spurious. For this setting, we present variations of our methods, which compute complete abstractions. Then, it is possible to provide guarantees about actually reachable states, which allows us to do both, identify a warning as spurious or generate a legitimate counterexample trace.

Fulltext:
PDF