SBA: cadre d'analyse binaire statique
Qu'est-ce qu'un cadre d'analyse binaire statique devrait faire?
- Réduire l'effort de mise en œuvre pour l'analyse individuelle
- Seulement 250 locs en C ++ pour implémenter une analyse pour valider les propriétés de la fonction.
- Hautement configurable
- Un cadre basé sur l'interprétation abstrait qui permet à l'utilisateur de définir des domaines abstraits et de configurer l'évaluation des instructions.
- Raisonnement sonore et précis sur la mémoire de la pile
- Un modèle de mémoire de pile à une granularité au niveau des octets et des approximations sonores et efficaces pour les mises à jour imprécises sur la pile.
- Architecture neutre
- Analyse de découple à partir de détails d'architecture tels que les langages d'assemblage et les spécifications ABI.
Commencer
Dépendances
sudo apt-get install g++ ocaml camlp4-extra camlp4 tar cmake make
Construire SBA
mkdir build && cd build
cmake .. && make -j4
Applications
Analyse de la table à sauter
Pour analyser un objet binaire ~/obj , utilisez la commande suivante:
./jump_table x86_64.auto ~/obj
Par défaut, SBA crée des fichiers temporaires et des sorties entraînent /tmp/sba/ . Ces chemins peuvent être spécifiés en utilisant -d et -o comme suit:
./jump_table -d /tmp/sba/ -o /tmp/sba/result x86_64.auto ~/obj
Publications
SBA a contribué de manière significative à la mise en œuvre des travaux suivants:
- Analyse de la table de saut évolutive, sonore et précise. ISSTA 2024.
- Démontage précis des binaires complexes sans utiliser de métadonnées du compilateur. ASPLOS 2023.
- Plus sûr: instrumentation binaire efficace et tolérante aux erreurs. Usenix 2023.
- Randomisation de code binaire à grain fin pratique. ACSAC 2020.
