Automated Binary Analysis

Zur GPN17 des Entropia e.V. im ZKM - Zentrum für Kunst und Medien
und der Hochschule für Gestaltung (HfG) hat Florian Magin
(@0x464d) einen Vortrag zu Automated Binary Analysis gehalten und
war bereit uns auch im Podcast zu erzählen, wie er mit
mathematischen Verfahren Software auf Schwachstellen analysiert.


Florian studiert Informatik an der TU Darmstadt und engagiert
sich im CTF-Team Wizards of Dos seiner Universität. Sein
Interesse an der Computersicherheit hat ihn auch zur Firma ERNW
Research geführt, wo er als Werkstudent in der
IT-Sicherheitsforschung tätig ist.


Wie wichtig die Suche nach Schwachstellen und deren Absicherung
ist, wurde kürzlich bei der weltweiten Verbreitung der
WannaCry/WannaCrypt-Schadsoftware bewusst, die die Aufmerksamkeit
von einer anderen und lukrativeren Schadsoftware Adylkuzz
ablenkte.


Unter der Binary Analysis versteht man die quellenlose Analyse
eines Programms alleine auf den Daten im Maschinencode auf einem
Speichermedium. Ein erster Schritt der Analysis ist die Wandlung
der Maschinensprache in Mnemonic durch einen Disassembler. Dieser
Programmcode kann sich deutlich von einer ursprünglichen
Quelltext des Programms unterscheiden, da der Maschinencode
erzeugende Compiler eine Vielzahl von Optimierungsmöglichkeiten
umsetzt, die den Ablauf und das Abbild des Programms im
Maschinencode deutlich verändern können.


Eine Herausforderung stellt sich inzwischen in der Größe der
Programme: Während es inzwischen zahlreiche Wettbewerbe gibt,
Programme unter extremen Platzbeschränkungen umzusetzen, wächst
die Größe klassischer Programme stark an. Ein
Maschinensprache-Befehl kann in einem Byte kodiert sein, wie
früher etwa hexadezimal C9 auf dem Z80 eine Unterroutine beendet,
so können in 4 Bytes Operationen wie eine Addition samt Parameter
definiert sein.


Die automatisierte Binäranalyse hat besonders durch die Darpa
Cyber Grand Challenge im Jahr 2016 großes Interesse geweckt, wo
die Teams autonome Software entwickeln sollten, die für sich
alleine den CTF-Wettbewerb bestreitet.


Eine Anwendung solcher automatisierten Programme ist die schnelle
Überprüfung von neuer Software auf bekannte oder typische
Schwachstellen oder Implementierungsfehler. Eine sehr allgemeine
Methode zur Detektion von Sicherheitslücken ist das Fuzzing: Das
Open Source Tool AFL modifiziert beispielsweise korrekte
Eingabewerte und prüft bei welcher Modifikation das Programm vom
zuvor aufgezeichneten Programmablauf abweicht und damit einen
Hinweis auf eine mögliche Schwachstelle gibt. Es kann dabei
idealerweise auf dem Sourcecode operieren oder auch das Programm
in einem Emulator wie QEMU ausführen und analysieren.


Wie schwer aber selbst Source Code zu verstehen sein kann, zeigen
die Wettbewerbe International Obfuscated C Code Contest (IOCCC),
zu möglichst schwer verständlichen sinnvollen Code, und der
Underhanded C Contest, wo ein scheinbar sinnvoller Code für
Menschen möglichst unvorhersehbare Zusatzfunktionen aufweist.
Ebenso können sehr beliebte Programmiersprachen wie Python sehr
unvorhersehbar reagieren, wenn man versehentlich Tabulatoren und
Space vermischt, oder gleich die Programmiersprache Whitespace
benutzt. Ein weiteres Beispiel ist, dass das Breitenlose
Leerzeichen in neuen C++-Standards erlaubt ist, und für den
Menschen ununterscheidbaren Code ermöglicht, der unterschiedliche
Dinge tut. Aber auch Computer können getäuscht werden, wenn zum
Vergleich unsichere Hash-Funktionen genutzt werden, wie jüngst
die Shattered-Attacke auf die SHA-1 Hash zeigte.


Eine automatisierte Analysemöglichkeit ist die Control Flow Graph
Recovery, die beispielsweise mit IDA , radare2, binary ninja
durchgeführt werden kann, um aus einer eindimensionalen
Speicherdarstellung zu einem Programmnetz, wo zusammengehörige
Programmblöcke miteinander vernetzt werden. Hier kann auch schon
sichtbar werden, ob beschränkte Bereiche ohne Authentifikation
erreicht werden können. Ein weiteres automatisierbares Verfahren
ist die Datenflussanalyse, wo die Verarbeitung und Auswirkungen
von Variablen und Daten im Verlauf des Programms analysiert wird.
Hier kann der Verlauf von beispielsweise vertraulichen Daten
kontrolliert werden.


Bei einer Symbolischen Auswertung wird das Programm abstrakt mit
einem Interpreter auf beliebigen variablen Daten bzw.
symbolischen Ausdrücken auf allen Pfaden gleichzeitig ausgeführt.
Für die Pfaderkundung benötigt man hier eine Strategie zwischen
der Breitensuche und Tiefensuche, um die relevanten Teile des
Ausführungsgraphen möglichst schnell abzudecken. In der
automatisierten Analyse werden dabei offene Sprungmöglichkeiten
zu nahezu beliebigen Adressen sehr interessant, da dies einen
starken Indikator für einen Angriffsvektor liefern. Mit
Return-oriented Programming kann man so bestehenden Code gezielt
anspringen und für eigene Zwecke missbrauchen.


Das Open-Source Framework Angr wurde von Forschern des Computer
Security Lab at UC Santa Barbara entwickelt und belegte mit
Shellphish auf der Darpa-Challenge den dritten Platz. Ein
weiteres Open-Source Analyseframework ist Triton, welches man
leicht in eigene Projekte einbinden kann. Sehr verbreitet ist
auch das Framework S2E der École Polytechnique Fédérale de
Lausanne. Ein weiterer Finalist der Cyber Grand Challenge ist das
Team CodeJitsu von der University of California at Berkeley,
Cyberhaven, and Syracuse. Die Binary Analysis Platform wurde vom
Team um Professor David Brumley am Cylab der Carnegie Mellon
University entwickelt.


Funktionale Programmiersprachen wie OCAML oder Haskell haben für
den Anwendungsfall der symbolischen Auswertung ganz besondere
Vorteile. Ebenso werden Programmiersprachen auch auf ihre
inherente Unsicherheit im Sinne der Language based security
untersucht, sowie fertige Programme versucht auch auf ihre
Korrektheit zu verifizieren. Ein Tool, das dies vereinfachen soll
ist der Z3 Prover. Hier kommt die Suche nach Sicherheitslücke zur
Mathematik: In der formalen Darstellung einer Routine kann das
Verhalten als Abbildung aus symbolischen Variablen beschrieben
werden, und die Suche nach einer Lösung führt auf die
entsprechenden Logik oder Optimierungsverfahren.

Literatur und weiterführende Informationen

Florian Magin: Introduction to Automated Binary Analysis,
Vortrag auf der GPN17, 2017.

Program Analysis reading list

D. Brumley: Analysis and Defense of Vulnerabilities in Binary
Code, PhD thesis, School of Computer Science Carnegie Mellon
University, 2008.


Podcasts

M. Musch: Steganographie, Gespräch mit S. Ritterbusch im
Modellansatz Podcast, Folge 57, Fakultät für Mathematik,
Karlsruher Institut für Technologie (KIT), 2015.

J. Breitner: Incredible Proof Machine, Gespräch mit S.
Ritterbusch im Modellansatz Podcast, Folge 78, Fakultät für
Mathematik, Karlsruher Institut für Technologie (KIT), 2016.


GPN17 Special

Sibyllinische Neuigkeiten: GPN17, Folge 4 im Podcast des CCC
Essen, 2017.

M. Lösch: Smart Meter Gateway, Gespräch mit S. Ritterbusch im
Modellansatz Podcast, Folge 135, Fakultät für Mathematik,
Karlsruher Institut für Technologie (KIT), 2017.

F. Magin: Automated Binary Analysis, Gespräch mit S.
Ritterbusch im Modellansatz Podcast, Folge 137, Fakultät für
Mathematik, Karlsruher Institut für Technologie (KIT), 2017.