Item Type: |
Ph.D. Thesis |
Type of entry: |
Primary publication |
Title: |
Static Analysis of x86 Executables |
Language: |
English |
Referees: |
Veith, Prof. Dr. Helmut ; Mezini, Prof. Dr.- Mira |
Date: |
23 November 2010 |
Place of Publication: |
Darmstadt |
Date of oral examination: |
17 November 2010 |
Abstract: |
This dissertation is concerned with static analysis of binary executables in a theoretically well-founded, sound, yet practical way. The major challenge is the reconstruction of a correct control flow graph in presence of indirect jumps, pointer arithmetic, and untyped variables. While static program analysis for proving safety properties or finding bugs usually targets source code, in many potential analysis scenarios only a binary is available. For instance, intellectual property issues can prevent source code from being accessible to verification specialists, and some analyses, such as malware detection, are by definition required to work with executables. Moreover, binary analysis can be useful even in situations where the source code is available, e.g., when the compiler is not part of the trusted computing base. In most of the existing work, a heuristic disassembler makes a best effort attempt to generate a plain text listing of the assembly instructions in the executable and feeds it to a separate static analysis component. The heuristics render this technique inherently unsound, and the control flow graphs retrieved from such listings are usually fragmented and incomplete. Several approaches have pointed out the possibility of using results of data flow analysis to augment disassembly and control flow reconstruction, but described this connection as suffering from a "chicken and egg" problem, since data flow analysis requires a control flow graph to work on. This dissertation argues for the integration of disassembly, control flow reconstruction, and static analysis in a unified process. It introduces a framework for simultaneous control and data flow analysis on low level binary code, which overcomes the "chicken and egg" problem and is proven to yield the most precise control flow graph with respect to the precision of the data flow domain. A very precise domain that lends itself well to control flow reconstruction is introduced in Bounded Address Tracking, a combined pointer and value analysis that supports pointer arithmetic. It tracks variable valuations up to a tunable bound on the number of values per variable per program location. Its path sensitivity generally allows strong updates to memory, i.e., heap regions are uniquely identified, and equips it with context sensitivity without assuming a correct layout of procedures. These building blocks are combined into an extensible program analysis architecture, which is implemented in a novel binary analysis tool. The tool, named Jakstab, works directly on binaries and disassembles instructions on demand while exploring the program's state space, allowing it to handle low level features such as overlapping instructions, which cause difficulties for regular disassemblers. The architecture is highly configurable to allow a wide range of analyses, from sound abstract interpretation to heuristics-supported disassembly. Its practical feasibility and improvements over existing approaches are shown through case studies on device driver binaries and system executables found on a regular desktop PC. |
Alternative Abstract: |
Alternative Abstract | Language |
---|
Die vorliegende Arbeit befasst sich mit dem Problem der theoretisch fundierten, korrekten, aber dennoch praktisch nutzbaren statischen Analyse von ausführbaren Programmen im Binärformat. Die größte Herausforderung ist dabei die Rekonstruktion eines Kontrollflussgraphen angesichts von indirekten Sprüngen, Zeigerarithmetik und untypisierten Variablen. Statische Programmanalyse zum Beweis von Sicherheitseigenschaften oder zum Entdecken von Fehlern zielt normalerweise auf Quelltext ab, in vielen potentiellen Analyseszenarien ist jedoch nur eine Binärdatei verfügbar. So kann zum Beispiel die Sorge um geistiges Eigentum verhindern, dass ein Programm Spezialisten zur Verifikation vorgelegt wird, und bei Analysen wie der Erkennung von Schadprogrammen ist grundsätzlich nur eine Binärdatei verfügbar. Darüber hinaus kann eine Analyse von Binärprogrammen aber auch dann Vorteile bringen, wenn Quelltext vorliegt, zum Beispiel dadurch, dass die Korrektheit des übersetzers nicht länger angenommen werden muss. In bisherigen Arbeiten zur statischen Analyse von Binärprogrammen wird üblicherweise auf einen eigenständigen heuristischen "Disassembler" zurückgegriffen. Dieser versucht, möglichst alle Assembler-Instruktionen in der ausführbaren Binärdatei im Klartext aufzulisten und gibt diesen Programmtext dann an eine separate Komponente zur statischen Analyse weiter. Die Verwendung von Heuristiken verhindert die Korrektheit dieser Technik, und Kontrollflussgraphen, die aus solchen Programmtexten erzeugt werden, sind meist fragmentiert und unvollständig. In der Literatur wurde bereits von mehreren Autoren darauf hingewiesen, dass die Ergebnisse einer Datenflussanalyse bei der Erzeugung des Kontrollflussgraphen helfen können. Allerdings beschrieben sie diese Verbindung als ein "Henne-Ei-Problem", da eine klassische Datenflussanalyse bereits einen Kontrollflussgraphen als Eingabe benötigt. In der vorliegenden Dissertation wird argumentiert, dass Disassemblierung, Rekonstruktion des Kontrollflussgraphen und statische Analyse in einem einheitlichen Prozess durchgeführt werden sollten. Es wird ein Rahmen für gleichzeitige Kontroll- und Datenflussanalyse auf Maschinensprache vorgestellt, der das "Henne-Ei-Problem" auflöst und bewiesenermaßen den bezüglich der Genauigkeit der Datenflussanalyse bestmöglichen Kontrollflussgraphen rekonstruiert. Mit "Bounded Address Tracking" wird eine hochpräzise Analyse eingeführt, die sich besonders gut für diese Aufgabe eignet. Diese Analyse verfolgt sowohl Zeiger als auch Zahlenwerte und unterstützt dabei Zeigerarithmetik. Sie erfasst den Zustand von Variablen bis zu einer konfigurierbaren Schranke für die maximale Anzahl an Werten pro Variable und Programmpunkt. Pfadsensitivität verleiht der Analyse Kontextsensitivität auch ohne eine korrekte prozedurale Struktur annehmen zu müssen, und erlaubt ihr, das Ziel jedes Speicherzugriffs eindeutig zu identifizieren. Diese Komponenten werden zu einer erweiterbaren Architektur zusammengesetzt, die in dem neu entwickelten Analysewerkzeug Jakstab implementiert ist. Jakstab arbeitet direkt auf Binärdateien; während es den Zustandsraum des Zielprogramms durchsucht, disassembliert es bei Bedarf immer nur jeweils eine einzelne Instruktion. Dies erlaubt Jakstab, auch Konstrukte wie sich überlappende Instruktionen zu unterstützen, die herkömmlichen Disassemblern Probleme bereiten. Die Architektur ist sehr fein konfigurierbar, um ein weites Spektrum an Analysen zu ermöglichen, von Abstrakter Interpretation bis hin zu heuristischem Disassemblieren. Der praktische Nutzen und die Verbesserungen gegenüber früheren Ansätzen werden in Fallstudien über Gerätetreiber und Programmdateien eines gewöhnlichen Arbeitsplatzrechners gezeigt. | German |
|
Uncontrolled Keywords: |
static analysis, binaries, binary, executables, disassembly, x86, control flow |
Alternative keywords: |
Alternative keywords | Language |
---|
static analysis, binaries, binary, executables, disassembly, x86, control flow | English |
|
URN: |
urn:nbn:de:tuda-tuprints-23388 |
Classification DDC: |
000 Generalities, computers, information > 004 Computer science |
Divisions: |
20 Department of Computer Science 20 Department of Computer Science > Formal Methods in System Engineering |
Date Deposited: |
26 Nov 2010 11:11 |
Last Modified: |
08 Jul 2020 23:48 |
URI: |
https://tuprints.ulb.tu-darmstadt.de/id/eprint/2338 |
PPN: |
229081622 |
Export: |
|