Triton Download - Triton Source Code Download

Triton

Andere Kategorien

Version 0.9

Herunterladen

Triton ist eine dynamische Binäranalyse -Bibliothek. Es bietet interne Komponenten, mit denen Sie Ihre Programmanalyse -Tools erstellen, Reverse Engineering automatisieren, die Softwareverifizierung durchführen oder nur Code emulieren können.

Dynamische symbolische Ausführung
Dynamische Makleranalyse
AST-Darstellung des X86 , X86-64 , ARM32 , AArch64 und RISC-V 32/64 ISA Semantic
Ausdrucksynthese
SMT -Vereinfachung geht
Heben auf LLVM sowie Z3 und Rücken
SMT Solver Schnittstelle zu Z3 und Bitwuzla
C ++ und Python -API

Da Triton eine Art Teilzeitprojekt ist, beschuldigen Sie uns bitte nicht , wenn es nicht vollständig zuverlässig ist. Offene Probleme oder Zuganfragen sind immer besser als Trolling =). Sie können jedoch die Entwicklung auf Twitter @QB_TRITON verfolgen.

Schneller Start

Installation
Python API
C ++ API
Python -Beispiele
Sie benutzten bereits Triton

Erste Schritte

 from triton import *

> >> # Create the Triton context with a defined architecture
>> > ctx = TritonContext ( ARCH . X86_64 )

> >> # Define concrete values (optional)
>> > ctx . setConcreteRegisterValue ( ctx . registers . rip , 0x40000 )

> >> # Symbolize data (optional)
>> > ctx . symbolizeRegister ( ctx . registers . rax , 'my_rax' )

> >> # Execute instructions
>> > ctx . processing ( Instruction ( b" x48 x35 x34 x12 x00 x00 " )) # xor rax, 0x1234
> >> ctx . processing ( Instruction ( b" x48 x89 xc1 " )) # mov rcx, rax

> >> # Get the symbolic expression
>> > rcx_expr = ctx . getSymbolicRegister ( ctx . registers . rcx )
> >> print ( rcx_expr )
( define - fun ref ! 8 () ( _ BitVec 64 ) ref ! 1 ) ; MOV operation - 0x40006 : mov rcx , rax

>> > # Solve constraint
>> > ctx . getModel ( rcx_expr . getAst () == 0xdead )
{ 0 : my_rax : 64 = 0xcc99 }

>> > # 0xcc99 XOR 0x1234 is indeed equal to 0xdead
>> > hex ( 0xcc99 ^ 0x1234 )
'0xdead'

Installieren

Triton stützt sich auf die folgenden Abhängigkeiten:

 * libcapstone                >= 5.0.x   https://github.com/capstone-engine/capstone
* libboost      (optional)   >= 1.68
* libpython     (optional)   >= 3.6
* libz3         (optional)   >= 4.6.0   https://github.com/Z3Prover/z3
* libbitwuzla   (optional)   >= 0.4.x   https://github.com/bitwuzla/bitwuzla
* llvm          (optional)   >= 12

Linux und MacOS

$ git clone https://github.com/JonathanSalwan/Triton
$ cd Triton
$ mkdir build ; cd build
$ cmake ..
$ make -j3
$ sudo make install

Standardmäßig werden LLVM und Bitwuzla nicht zusammengestellt. Wenn Sie die volle Kraft von Triton genießen möchten, lautet das CMake -Kompilieren:

$ cmake -DLLVM_INTERFACE=ON -DCMAKE_PREFIX_PATH= $( llvm-config --prefix ) -DBITWUZLA_INTERFACE=ON ..

MacOS M1 Hinweis:

Falls Sie Kompilierungsfehler wie folgt erhalten:

 Could NOT find PythonLibs (missing: PYTHON_LIBRARIES PYTHON_INCLUDE_DIRS)

Versuchen Sie, PYTHON_EXECUTABLE , PYTHON_LIBRARIES und PYTHON_INCLUDE_DIRS für Ihre spezifische Python -Version anzugeben:

 cmake -DCMAKE_INSTALL_PREFIX=/opt/homebrew/ 
      -DPYTHON_EXECUTABLE=/opt/homebrew/bin/python3 
      -DPYTHON_LIBRARIES=/opt/homebrew/Cellar/[email protected]/3.10.8/Frameworks/Python.framework/Versions/3.10/lib/libpython3.10.dylib 
      -DPYTHON_INCLUDE_DIRS=/opt/homebrew/opt/[email protected]/Frameworks/Python.framework/Versions/3.10/include/python3.10/ 
      ..

Diese Informationen können Sie von diesem Snippet herausholen:

 from sysconfig import get_paths
info = get_paths ()
print ( info )

Fenster

Sie können CMake verwenden, um die .ln -Datei von Libtriton zu generieren.

> git clone https://github.com/JonathanSalwan/Triton.git
> cd Triton
> mkdir build
> cd build
> cmake -G " Visual Studio 14 2015 Win64 " 
  -DBOOST_ROOT="C:/Users/jonathan/Works/Tools/boost_1_61_0" 
  -DPYTHON_INCLUDE_DIRS="C:/Python36/include" 
  -DPYTHON_LIBRARIES="C:/Python36/libs/python36.lib" 
  -DZ3_INCLUDE_DIRS="C:/Users/jonathan/Works/Tools/z3-4.6.0-x64-win/include" 
  -DZ3_LIBRARIES="C:/Users/jonathan/Works/Tools/z3-4.6.0-x64-win/bin/libz3.lib" 
  -DCAPSTONE_INCLUDE_DIRS="C:/Users/jonathan/Works/Tools/capstone-5.0.1-win64/include" 
  -DCAPSTONE_LIBRARIES="C:/Users/jonathan/Works/Tools/capstone-5.0.1-win64/capstone.lib" ..

Wenn Sie jedoch die vorkompilierte Bibliothek direkt herunterladen möchten, lesen Sie die Artefakte unseres Appveyors. Beachten Sie, dass Sie wahrscheinlich die visuellen C ++ - Neuverteilbaren Pakete für Visual Studio 2012 installieren müssen, wenn Sie die Artefakte von Appveyor verwenden.

Installation von VCPKG

Der Triton -Port in VCPKG wird von Microsoft -Teammitgliedern und Community -Mitwirkenden auf dem Laufenden gehalten. Die URL von VCPKG lautet: https://github.com/microsoft/vcpkg. Sie können Triton mit dem VCPKG -Abhängigkeitsmanager herunterladen und installieren:

$ git clone https://github.com/Microsoft/vcpkg.git
$ cd vcpkg
$ ./bootstrap-vcpkg.sh  # ./bootstrap-vcpkg.bat for Windows
$ ./vcpkg integrate install
$ ./vcpkg install triton

Wenn die Version veraltet ist, erstellen Sie bitte eine Ausgabe- oder Pull -Anfrage im VCPKG -Repository.

Mitwirkende

Alberto Garcia Illera - Kreuzfahrtautomatisierung
Alexey Vishnyakov - ISP Ras
Schwarzer binär - n/a
Christian Heitman - Quarkslab
Daniil Kuts - Isp Ras
Jessy Campos - n/a
Matteo F. - n/a
Pierrick Brunet - Quarkslab
Pixelrick - n/a
Romain Thomas - Quarkslab
Und noch viel mehr

Sie benutzten bereits Triton

Werkzeuge

Exrop: Automatische Seilbundgenerierung.
Zuhälter: Triton -basiertes R2 -Plugin für konkolische Ausführung und Gesamtsteuerung.
PONCE: IDA 2016 Plugin Contest -Gewinner! Symbolische Ausführung nur ein Klick weg!
Qsynthesis: Greybox -Synthesizer für die Deobfuskation von Montageanweisungen.
Tritondse: Triton-basierte DSE-Bibliothek mit Lade- und Erkundungsfunktionen.
Titan: Titan ist ein VMProtect Devirtualizer mit Triton.

Papiere und Konferenz

Sydr-Fuzz: Kontinuierliche hybride Fuzzing und dynamische Analyse für den Lebenszyklus für Sicherheitsentwicklung
Sprechen Sie bei : Ivannikov ISP Ras Open Conference, Moskau, Russland, 2022. [Papier] [Slide]
Autoren : Vishnyakov A., Kuts D., Logunova V., Parygina D., Kobrin E., Savidov G., Fedotov A.
Abstract : Heutzutage sind automatisierte dynamische Analyse -Frameworks für kontinuierliche Tests sehr gefragt, um die Sicherheit der Software zu gewährleisten und die SDL -Anforderungen (Sicherheitsentwicklung) zu erfüllen. Die Effizienz der Sicherheitsfehler-Jagd von hochmodernen Hybridfuzzing-Techniken übertrifft weit verbreitete Deckungsfuzzing. Wir schlagen eine verbesserte dynamische Analyse -Pipeline vor, um die Produktivität der automatisierten Fehlererkennung basierend auf Hybridfuzzing zu nutzen. Wir implementieren die vorgeschlagene Pipeline im Continuous Fuzzing Toolset Sydr-Fuzz, der vom Hybrid-Fuzzing-Orchestrator angetrieben wird und unser DSE-Tool Sydr in Libfuzzer und AFL ++ integriert. Sydr-Fuzz umfasst auch Sicherheitspräßschubs für Sicherheitsprädikate, Crash-Trianting-Tools und Versorgungsunternehmen für die Minimierung von Korpus und die Abdeckung. Das Benchmarking unseres hybriden Fuzzers gegen alternative hochmoderne Lösungen zeigt seine Überlegenheit gegenüber abdeckungsgesteuerten Fuzzern und bleibt mit fortschrittlichen Hybridfuzzern auf dem gleichen Niveau. Darüber hinaus genehmigen wir die Relevanz unseres Ansatzes, indem wir 85 neue Software-Fehler in der realen Welt im Oss-Sydr-Fuzz-Projekt entdecken. Schließlich öffnen wir CASR -Quellcode für die Community, um die Prüfung der vorhandenen Abstürze zu erleichtern.

Starke optimistische Lösung für dynamische symbolische Ausführung
Sprechen Sie bei : Ivannikov Memorial Workshop, Kazan, Russland, 2022. [Papier] [Slide]
Autoren : Parygina D., Vishnyakov A., Fedotov A.
Abstract : Dynamische symbolische Ausführung (DSE) ist eine effektive Methode für automatisierte Programmtests und Fehlererkennung. Es erhöht die Codeabdeckung durch die komplexen Zweige, die während des hybriden Fuzzings untersucht werden. DSE -Tools ziehen die Zweige entlang eines Ausführungspfads um und helfen Fuzzar, bisher nicht verfügbare Programmteile zu untersuchen. DSE hat oft Probleme mit über- und unterbezogenen Problemen. Der erste führt zu einer signifikanten Analyse -Komplikation, während der zweite eine ungenaue symbolische Ausführung verursacht. Wir schlagen eine starke optimistische Lösungsmethode vor, die irrelevante Prädikatbeschränkungen für die Inversion von Zielzweigen beseitigt. Wir beseitigen solche symbolischen Einschränkungen, von denen der Zielzweig nicht kontrolliert ist, abhängig. Darüber hinaus verarbeiten wir separat symbolische Zweige, die die Übertragungsanweisungen verschachtelt haben, die die Kontrolle über das übergeordnete Zweigbereich, z. B. Return, GOTO, BREAK usw. übergeben. Wir implementieren die vorgeschlagene Methode in unserem dynamischen symbolischen Ausführungstool Sydr. Wir bewerten die starke optimistische Strategie, die optimistische Strategie, die nur die letzte Einschränkung negiert, und ihre Kombination. Die Ergebnisse zeigen, dass die Kombination aus Strategien dazu beiträgt, entweder die Codeabdeckung oder die durchschnittliche Anzahl korrekt invertierter Zweige pro Minute zu erhöhen. Es ist optimal, beide Strategien im Gegensatz zu anderen Konfigurationen zusammen anzuwenden.

Greybox -Programmsynthese: Ein neuer Ansatz zum Angriff auf Datenflusszuwehung
Sprechen Sie bei : Blackhat USA, Las Vegas, Nevada, 2021. [Slide]
Autoren : Robin David
Zusammenfassung : Dieser Vortrag zeigt die neuesten Fortschritte in der Programmsynthese, die für die Deobfuskation angewendet werden. Es zielt darauf ab, diese Analysetechnik zu entmystifizieren, indem gezeigt wird, wie sie in Bezug auf die Verschleierung in die Tat umgesetzt werden kann. Insbesondere die für diesen Vortrag veröffentlichte Implementierung Qsynthese zeigt einen vollständigen End-to-End-Workflow für Deobfuscate-Montageanweisungen in optimierten (deobfuszierten) Anweisungen wieder in der Binärdatei wieder zusammen.

Vom Quellcode zu Crash-Testfall durch Software-Testautomatisierung
Sprechen Sie unter : C & esar, Rennes, Frankreich, 2021. [Papier] [Slide]
Autoren : Robin David, Jonathan Salwan, Justin Bourroux
Abstract : In diesem Artikel wird ein Ansatz vorgestellt, der den Software -Testprozess von einem Quellcode zum dynamischen Test des kompilierten Programms automatisiert. Insbesondere aus einem statischen Analysebericht, in dem Warnungen in Quellzeilen angezeigt werden, ermöglicht das Testen, diese Zeilen dynamisch und opportunistisch zu überprüfen, ob sie einen Absturz auslösen können oder nicht. Das Ergebnis ist ein Testkorpus, der es ermöglicht, Warnungen abzudecken und sie auszulösen, wenn es sich um wahre positive Positive handelt. In diesem Artikel wird die Methodik erörtert, die zur Verfolgung von Warnmeldungen im kompilierten Binary, des Auswahlprozesses für Testmotoren und den Ergebnissen einer TCP/IP -Stapel -Implementierung für eingebettete und IoT -Systeme verfolgt wird.

Symbolische Sicherheitsprädikate: Jagdprogrammschwächen
Sprechen Sie bei : Ivannikov ISP Ras Open Conference, Moskau, Russland, 2021. [Papier] [Slide]
Autoren : A.vishnyakov, V.Logunova, E.Kobrin, D.Kuts, D. Parygina, A.Fedotov
Abstract : Dynamische symbolische Ausführung (DSE) ist eine leistungsstarke Methode zur Pfaduntersuchung bei hybridem Fuzzing und automatischer Fehlererkennung. Wir schlagen Sicherheitsprädikate vor, um undefinierte Verhaltens- und Speicherzugriffsverletzungsfehler effektiv zu erkennen. Zunächst führen wir symbolisch Programm auf Pfaden aus, die keine Fehler auslösen (Hybridfuzzing kann diese Pfade untersuchen). Anschließend erstellen wir ein symbolisches Sicherheitsprädikat, um eine Fehlerbedingung zu überprüfen. Daher können wir den Programmdatenfluss ändern, um Nullzeiger-Derreferenz-, Teilung durch Null, Zugang zu Out-of-Bounds oder Ganzzahlüberlaufschwächen zu bilden. Im Gegensatz zur statischen Analyse meldet die dynamische symbolische Ausführung nicht nur Fehler, sondern generiert auch neue Eingabedaten, um sie zu reproduzieren. Darüber hinaus führen wir eine Funktionssemantikmodellierung für gemeinsame C/C ++ - Standardbibliotheksfunktionen ein. Wir wollen den Steuerfluss in einer Funktion mit einer einzelnen symbolischen Formel modellieren. Dies hilft die Erkennung des Fehlers, beschleunigt die Untersuchung der Pfad und überwindet Überstände im Pfadprädikat. Wir implementieren die vorgeschlagenen Techniken in unserem dynamischen symbolischen Ausführungstool Sydr. Daher verwenden wir leistungsstarke Methoden aus SYDR, wie z. B. Slicing von Pfadprädikat, die irrelevante Einschränkungen beseitigt. Wir präsentieren Julia Dynamic, um die Genauigkeit der dynamischen Fehlererkennung zu messen. Das Testsystem überprüft außerdem, dass die Erzeugung von Eingängen Desinfektionsmittel auslösen. Wir bewerten die Sydr -Genauigkeit für 11 CWEs aus der Julia Test Suite. SYDR zeigt 95,59% Gesamtgenauigkeit. Wir stellen SYDR -Bewertungsartefakte öffentlich zur Verfügung, um die Reproduzierbarkeit der Ergebnisse zu erleichtern.

Auf dem Weg zu symbolischen Zeigern, die in der dynamischen symbolischen Ausführung denken
Sprechen Sie bei : Ivannikov Memorial Workshop, Nizhny Novgorod, Russland, 2021. [Papier] [Slide]
Autoren : Daniil Kuts
Abstract : Dynamische symbolische Ausführung ist eine weit verbreitete Technik für automatisierte Softwaretests, die für die Erkennung von Ausführungspfaden und Programmfehlern entwickelt wurde. Ein hybrider Ansatz ist in letzter Zeit weit verbreitet, wenn das Hauptziel der symbolischen Ausführung darin besteht, Fuzzerr -Program -Berichterstattung zu erhöhen. Je mehr Zweige symbolische Executor invertieren können, desto nützlicher ist es für Fuzzer. Ein Programmsteuerungsfluss hängt häufig von Speicherwerten ab, die durch Berechnung von Adressindizes aus der Benutzereingabe erhalten werden. Die meisten DSE -Tools unterstützen solche Abhängigkeiten jedoch nicht, daher vermissen sie einige gewünschte Programmabzeigungen. Wir implementieren symbolische Ansprachen für die Begründung von Speicherlesungen in unserem dynamischen symbolischen Ausführungstool SYDR. Mögliche Speicherzugriffsregionen werden bestimmt, indem entweder symbolische Ausdrücke der Speicheradresse oder die binäre Suche mit SMT-SOLVER analysiert werden. Wir schlagen eine verbesserte Linearisationstechnik zum Modellieren von Speicherzugriffszubehör vor. Unterschiedliche Memory -Modellierungsmethoden werden mit den Programmen verglichen. Unsere Bewertung zeigt, dass symbolische Adressen die Handhabung ermöglichen, neue symbolische Zweige zu entdecken und die Programmabdeckung zu erhöhen.

Qsynth: Ein Programmsynthese -basierter Ansatz für Binärcode Deobfuscation
Sprechen Sie an : Bar, San Diego, Kalifornien, 2020. [Papier]
Autoren : Robin David, Luigi Coniglio, Mariano Ceccato
Abstract : Wir präsentieren einen generischen Ansatz, der sowohl die DSE- als auch die Programmsynthese nutzt, um Programme erfolgreich mit gemischten Boolen-arithmetischen, datenkodierenden oder virtualisierten Synthese zu synthetisieren. Der vorgeschlagene Synthesealgorithmus ist eine Offline-Aufzählungssynthese-Primitive, die von der Suche nach oben nach unten geführt wird. Wir zeigen seine Wirksamkeit gegen einen modernen Verschleierungspunkt und seine Skalierbarkeit, wenn sie andere ähnliche Ansätze ersetzt, die auf der Synthese basieren. Wir zeigen auch seine Wirksamkeit bei der Gegenwart einer zusammengesetzten Verschleierung (Kombination verschiedener Techniken). Diese fortlaufende Arbeit erleuchtet die Wirksamkeit der Synthese, um bestimmte Arten von Verschleierung abzuzielen, und eröffnet den Weg zu robusteren Algorithmen und Vereinfachungsstrategien.

SYDR: Spitzenreitige dynamische symbolische Ausführung
Sprechen Sie bei : Ivannikov ISP Ras Open Conference, Moskau, Russland, 2020. [Papier] [Slide] [Video]
Autor
Abstract : Dynamische symbolische Ausführung (DSE) weist eine enorme Menge an Anwendungen in der Computersicherheit (Fuzzing, Sicherheitsförderung, Reverse-Engineering usw.) auf. Wir schlagen mehrere Leistungs- und Genauigkeitsverbesserungen für die dynamische symbolische Ausführung vor. Wenn Sie nicht symbolische Anweisungen überspringen, können Sie ein Pfadprädikat 1,2-- 3,5-mal schneller erstellen. Die symbolische Engine vereinfacht die Formeln während der symbolischen Ausführung. Pfadprädikatschneide eliminiert irrelevante Konjunkten aus Löserabfragen. Wir verarbeiten jede Sprungtabelle (Switch-Anweisung) als mehrere Zweige und beschreiben die Methode zur symbolischen Ausführung von Multi-Thread-Programmen. Die vorgeschlagenen Lösungen wurden im SYDR -Tool implementiert. SYDR führt die Inversion von Zweigen im Pfadprädikat durch. SYDR kombiniert Dynamorio Dynamic Binary Instrumentation Tool mit Triton Symbolic Engine.

Symbolische Deobfuskation: Vom virtualisierten Code zurück zum Original
Sprechen Sie bei : Dimva, Paris-Saclay, Frankreich, 2018. [Papier] [Slide]
Autoren : Jonathan Salwan, Sébastien Bardin, Marie-Laure-Potet
Zusammenfassung : Der Softwareschutz hat im letzten Jahrzehnt einen wichtigen Platz eingenommen, um die legitime Software vor Reverse Engineering oder Manipulationen zu schützen. Die Virtualisierung gilt als eine der besten Abwehrkräfte gegen solche Angriffe. Wir präsentieren einen generischen Ansatz, der auf symbolischen Pfaduntersuchungen, -vermächtigten und -Compilation basiert, die es ermöglichen, von einem virtualisierten Code, einem devirtualisierten Code, semantisch mit dem ursprünglichen und der Größe identisch zu sein und die Größe zu nähern. Wir definieren Kriterien und Metriken, um die Relevanz der deobfuszierten Ergebnisse in Bezug auf Richtigkeit und Präzision zu bewerten. Schließlich schlagen wir ein Open-Source-Setup vor, der es ermöglicht, den vorgeschlagenen Ansatz an verschiedenen Formen der Virtualisierung zu bewerten.

Deobfuskation von VM -basierten Softwareschutz
Sprechen Sie bei : SSTIC, Rennes, Frankreich, 2017. [Französisches Papier] [Englische Folie] [Französisch Video]
Autoren : Jonathan Salwan, Sébastien Bardin, Marie-Laure-Potet
Abstract : In dieser Präsentation beschreiben wir einen Ansatz, der dazu besteht, den Softwareschutz für den virtuellen Maschinen automatisch zu analysieren und eine neue Version des Binärs ohne solche Schutzmaßnahmen neu zu kompilieren. Dieser automatisierte Ansatz beruht auf einem symbolischen Ausführungshandbuch durch eine Makelanalyse und einige Konkretisierungsrichtlinien, dann auf ein binäres Umschreiben mit LLVM -Übergang.

Wie Triton dazu beitragen kann, virtuelle Maschinenbasis -Softwareschutz umzukehren
Sprechen Sie bei : CSAW SOS, NYC, New York, 2016. [Slide]
Autoren : Jonathan Salwan, Romain Thomas
Zusammenfassung : Der erste Teil des Vortrags wird eine Einführung in den Triton -Framework sein, um seine Komponenten aufzudecken und zu erklären, wie sie zusammenarbeiten. Anschließend enthält der zweite Teil Demonstrationen darüber, wie es möglich ist, virtuelle maschinenbasierte Schutzmaßnahmen mithilfe von Makelanalysen, symbolische Ausführung, SMT-Vereinfachungen und LLVM-IR-Optimierungen umzukehren.

Dynamische binäre Analyse und verschleierte Codes
Reden Sie unter : St'Hack, Bordeaux, Frankreich, 2016. [Slide]
Autoren : Jonathan Salwan, Romain Thomas
Abstract : Bei dieser Präsentation werden wir darüber sprechen, wie ein DBA (Dynamic Binary Analysis) einem umgekehrten Ingenieur helfen kann, verschleiert den Code umzukehren. Wir werden zunächst einige grundlegende Verschleierungstechniken einführen und dann enthüllen, wie es möglich ist, einige Dinge zu brechen (mit unserem Open -Source -DBA -Framework - Triton) wie Erkennung von undurchsichtigen Vorhersagen, CFG rekonstruieren, den ursprünglichen Algorithmus finden, vernünftige Daten isolieren und vieles mehr.

Wie Triton dazu beitragen kann, verschleierte Binärdateien zu analysieren
Veröffentlichung bei : Miscial Magazine 82, 2015. [Französischer Artikel]
Autoren : Jonathan Salwan, Romain Thomas
Zusammenfassung : Binäre Verschleierung wird verwendet, um das geistige Eigentum von Software zu schützen. Es gibt verschiedene Arten von Obfokationsarten, aber es verwandelt ungefähr eine binäre Struktur in eine andere binäre Struktur, indem sie dasselbe Semantik erhalten. Ziel der Verschleierung ist es, sicherzustellen, dass die ursprünglichen Informationen in nutzlosen Informationen "ertrinken" werden, die umgekehrte Engineering erschweren. In diesem Artikel werden wir zeigen, wie wir ein vom Ofbussen analysierender Programm analysieren und einige Verschleierung mithilfe des Triton -Frameworks brechen können.

Triton: Ein konkolischer Ausführungsrahmen
Sprechen Sie bei : SSTIC, Rennes, Frankreich, 2015. [Französisches Papier] [Detaillierte englische Folie]
Autoren : Jonathan Salwan, Florent Saudel
Zusammenfassung : In diesem Vortrag geht es um die Veröffentlichung von Triton, einem konkolischen Ausführungsrahmen basierend auf PIN. Es bietet Komponenten wie eine gemütliche Engine, eine dynamische symbolische Ausführungsmotor, eine Snapshot -Engine, die Übersetzung der X64 -Anweisung in SMT2, eine Z3 -Schnittstelle zur Lösung von Einschränkungen und Pythonbindungen. Basierend auf diesen Komponenten bietet Triton die Möglichkeit, Tools für Schwachstellenforschung oder umgekehrte Unterstützung zu erstellen.

Dynamische Verhaltensanalyse unter Verwendung binärer Instrumentierung
Sprechen Sie unter : St'Hack, Bordeaux, Frankreich, 2015. [Slide]
Autoren : Jonathan Salwan
Zusammenfassung : Dieser Vortrag kann wie der Teil 2 unseres Vortrags am Sicherheitstag betrachtet werden. Im vorherigen Teil haben wir darüber gesprochen, wie es möglich war, eine gezielte Funktion im Speicher mithilfe des DSE -Ansatzes (Dynamic Symbolic Execution) abzudecken. Decken Sie eine Funktion (oder ihre Zustände) nicht ab. Finden Sie nicht alle Schwachstellen. Eine gewisse Sicherheitsanfälligkeit stürzt das Programm nicht ab. Aus diesem Grund müssen wir eine spezielle Analyse implementieren, um bestimmte Fehler zu finden. Diese Analyse basiert auf der binären Instrumentierung und der Laufzeitverhaltensanalyse des Programms. In diesem Vortrag werden wir sehen, wie es möglich ist, diese folgenden Fehler zu finden: Off-by-One, Stack / Heap-Überlauf, Nutzungsfrei, Formatstring und {schreiben, lesen} -What-wo.

Abdeckung einer Funktion unter Verwendung eines dynamischen symbolischen Ausführungsansatzes
Sprechen Sie bei : Sicherheitstag, Lille, Frankreich, 2015. [Slide]
Autoren : Jonathan Salwan
Zusammenfassung : In diesem Vortrag geht es um binäre Analyse und Instrumentierung. Wir werden sehen, wie es möglich ist, eine bestimmte Funktion abzielen, den Kontextspeicher/die Register vor der Funktion zu schnappen, die Instrumentierung in eine Zwischendarstellung umzusetzen, eine auf diesem IR anhand dieses IRs basierende Analyse anwenden, Formeln bauen/halten, formeln für eine dynamische symbolische Ausführung (DSE).

Triton zitieren

@inproceedings{SSTIC2015-Saudel-Salwan,
  author    = {Saudel, Florent and Salwan, Jonathan},
  title     = {Triton: A Dynamic Symbolic Execution Framework},
  booktitle = {Symposium sur la s{ ' {e}}curit{ ' {e}} des technologies de l'information
               et des communications},
  series    = {SSTIC},
  pages     = {31--54},
  address   = {Rennes, France},
  month     = jun,
  year      = {2015},
}

Expandieren

Zusätzliche Informationen