SBA: Marco de análisis binario estático
¿Qué debería hacer un marco de análisis binario estático?
- Reducir el esfuerzo de implementación para el análisis individual
- Solo 250 locs en C ++ para implementar un análisis para validar las propiedades de la función.
- Altamente configurable
- Un marco basado en la interpretación abstracta que permite al usuario definir dominios abstractos y configurar la evaluación de instrucciones.
- Razonamiento sólido y preciso sobre la memoria de la pila
- Un modelo de memoria de pila en granularidad a nivel de bytes y aproximaciones sonoras y eficientes para actualizaciones imprecisas sobre la pila.
- Arquitectura-neutral
- Análisis de decouple a partir de detalles de arquitectura, como lenguas de ensamblaje y especificaciones de ABI.
Empezando
Dependencias
sudo apt-get install g++ ocaml camlp4-extra camlp4 tar cmake make
Construir SBA
mkdir build && cd build
cmake .. && make -j4
Aplicaciones
Análisis de mesa de salto
Para analizar un objeto binario ~/obj , use el siguiente comando:
./jump_table x86_64.auto ~/obj
De forma predeterminada, SBA crea archivos y salidas temporales que dan como resultado /tmp/sba/ . Estas rutas se pueden especificar usando -d y -o de la siguiente manera:
./jump_table -d /tmp/sba/ -o /tmp/sba/result x86_64.auto ~/obj
Publicaciones
SBA ha contribuido significativamente a la implementación de los siguientes trabajos:
- Análisis de mesa de salto escalable, de sonido y preciso. ISSTA 2024.
- Desmontaje preciso de binarios complejos sin el uso de metadatos del compilador. Asplos 2023.
- Más seguro: instrumentación binaria eficiente y tolerante a errores. Usenix 2023.
- Aleatorización práctica del código binario de grano fino. ACSAC 2020.
