PODLIST

Automated Binary Analysis

Download

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


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