SBA: statischer Binäranalyse -Framework
Was sollte für ein statisches Binäranalyse -Framework tun?
- Reduzieren Sie die Implementierungsaufwand für die individuelle Analyse
- Nur 250 Locs in C ++, um eine Analyse zur Validierung von Funktioneigenschaften zu implementieren.
- Hochkonfigurierbar
- Ein abstraktes interpretationsbasiertes Framework, mit dem Benutzer abstrakte Domänen definieren und die Bewertung der Anweisungen konfigurieren können.
- Klang und präzise Argumentation über Stack Memory
- Ein Stapelspeichermodell auf Byte-Ebene-Granularität sowie solide und effiziente Näherungen für ungenaue Updates auf Stack.
- Architektur-neutral
- Dekouple -Analyse aus Architekturspezifikationen wie Montagesprachen und ABI -Spezifikationen.
Erste Schritte
Abhängigkeiten
sudo apt-get install g++ ocaml camlp4-extra camlp4 tar cmake make
Bauen sba
mkdir build && cd build
cmake .. && make -j4
Anwendungen
Sprungtischanalyse
Verwenden Sie den folgenden Befehl, um ein binäres Objekt ~/obj zu analysieren:
./jump_table x86_64.auto ~/obj
Standardmäßig erstellt SBA temporäre Dateien und Ausgänge in /tmp/sba/ . Diese Pfade können mit -d und -o wie folgt spezifiziert werden:
./jump_table -d /tmp/sba/ -o /tmp/sba/result x86_64.auto ~/obj
Veröffentlichungen
SBA hat erheblich zur Umsetzung der folgenden Werke beigetragen:
- Skalierbare, Klang und genaue Sprungtischanalyse. IsSta 2024.
- Genaue Demontage komplexer Binärdateien ohne Verwendung von Compiler -Metadaten. ASPLOS 2023.
- Sicherer: Effizienter und fehlertolerante binäre Instrumentierung. Usenix 2023.
- Praktische feinkörnige Binärcode-Randomisierung. ACSAC 2020.
