This thesis presents a fully automatic and sound interprocedural framework for executable analysis, which is employed for e.g. detecting low-level errors or malware. We present an analysis that intertwines disassembling and abstract interpretation-based analysis to provide a sound overapproximation of the control flow graph for an executable. In order to discharge certain assumptions made during control flow reconstruction we add a side-effect analysis that reasons about the modifying potential of procedures. A stack analysis is implemented to precisely deal with non-optimised code. Therefore we present the domain of fast linear two-variable equalities. To track relations between loop iteration variables and memory accesses, we propose the domain of simplices, a subclass of polyhedra. Our experimental evaluation of the implementation shows that our techniques scale well for industrial-sized executables and provide very good results.      «

This thesis presents a fully automatic and sound interprocedural framework for executable analysis, which is employed for e.g. detecting low-level errors or malware. We present an analysis that intertwines disassembling and abstract interpretation-based analysis to provide a sound overapproximation of the control flow graph for an executable. In order to discharge certain assumptions made during control flow reconstruction we add a side-effect analysis that reasons about the modifying potential...     »

Diese Arbeit beschreibt ein voll automatisches interprozedurales Framework zur Analyse von Binärprogrammen. Wir stellen eine Analyse vor, die Disassemblieren und statische Analyse, basierend auf dem Prinzip der abstrakten Interpretation, verbindet, um so eine sichere Überapproximation des Kontrollflussgraphen eines Binärprogramms zu erhalten. In dem Zusammenhang sind Analysen notwendig, die das Modifikationspotential von Funktionen bestimmen und den Stack präzise analysieren. Für letztere präsentieren wir die Domäne der Zwei-Variablen-Gleichheiten, um so auch nicht-optimierten Code präzise analysieren zu können. Um Beziehungen zwischen Schleifenvariablen und Speicherzugriffen zu inferieren, verwenden wir die Domäne der Simplizes, eine Subklasse von Polyedern. Unsere Implementierung dieser Analysen und eine erste experimentelle Auswertung zeigt sowohl die Skalierbarkeit unseres Ansatzes als auch sehr gute Analyseergebnisse.      «

Diese Arbeit beschreibt ein voll automatisches interprozedurales Framework zur Analyse von Binärprogrammen. Wir stellen eine Analyse vor, die Disassemblieren und statische Analyse, basierend auf dem Prinzip der abstrakten Interpretation, verbindet, um so eine sichere Überapproximation des Kontrollflussgraphen eines Binärprogramms zu erhalten. In dem Zusammenhang sind Analysen notwendig, die das Modifikationspotential von Funktionen bestimmen und den Stack präzise analysieren. Für letztere präs...     »