z3_and_angr_binary_analysis_workshop
1.0.0
Ursprünglich von Sam Brown bei Steelcon und Hack.LU 2018 geliefert, war dies ein dreistündiger Workshop, in dem die Teilnehmer Z3 und ANGR für die binäre Analyse einführten. Der Workshop lieferte eine Einführung in SMT Solvers, den Z3 SMT Solver und seine Python Library und den ANGR -Binäranalyse -Framework.
Im Rahmen der Workshop -Übungen wurden geplant, die darauf abzielten, potenzielle Anwendungen der Technologie zu demonstrieren, um Sicherheitsforscher bei der Durchführung von Reverse -Engineering- und Schwachstellenforschung zu unterstützen.
Die Folien bieten einen groben Leitfaden für den Inhalt und welche Reihenfolge die Übungen in den Übungen ausprobieren.
| Name | Typ | Beschreibung |
|---|---|---|
| N Queens | Beispiel | "Wie können N Queens auf ein NXN -Schachbrett platziert werden, damit sich keine zwei von ihnen angreifen?" Verwendet Z3, um Lösungen für ein N * N -Schachbrett zu generieren |
| Hackvent 15 | Beispiel | Lösung und gehen Sie durch, um eine Hackvent 15 CTF Challenge mit Z3 zu lösen |
| Sudoku | Übung | Versuchen Sie, Sudoku mit Z3 zu lösen |
| Rng | Übung | Optionale Übungen - Verwenden Sie Z3, um nicht kryptografisch sicheren Zufallszahlengeneratoren Saatgutwert zu finden |
| x86 | 50/50 | Halbe Beispiele, halb DIY - Implementieren Sie simiplifizierte Versionen von X86 -Anweisungen mit Z3 |
| Undurchsichtige Prädikate | Übung | Verwenden Sie die zuvor implementierten Anweisungen, um undurchsichtige Prädikate in kleinen Sequenzen von Montageanweisungen zu identifizieren |
| Äquivalenzprüfung | Beispiel | Verwenden Sie die zuvor implementierten Anweisungen, um äquivalente Sequenzen von Anweisungen zu identifizieren |
| Name | Typ | Beschreibung |
|---|---|---|
| undurchsichtig | Beispiel | Verwenden Sie ANGR, um undurchsichtige Prädikate mit viel weniger Arbeit zu identifizieren :) |
| Ioctls | Beispiel | Identifizieren Sie Windows -Treiber -IOCTL -Codes mit ANGR |
| Hallo Welt | 50/50 | Übung und Walkthrough zur Verwendung von ANGR, um gültige Argumente für einen einfachen "Lizenzschlüssel -Validator" zu generieren |
| Bombenlabor | Übung | DIY -Übung mit ANGR, um ein "Bombenlabor" zu lösen |
Der gesamte Code befindet sich in Python3 und Sie sollten nur das ANGR -Binäranalyse -Framework installieren.
mkvirtualenv --python=$(which python3) angr && python -m pip install angr
workon angr
