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...
»