z3_and_angr_binary_analysis_workshop
1.0.0
Originalmente entregado por Sam Brown en Steelcon y Hack.Lu 2018, este fue un taller de tres horas que presenta a los asistentes a usar Z3 y Angr para el análisis binario. El taller proporcionó una introducción a los solucionadores SMT, el solucionador SMT Z3 y su biblioteca de Python y el marco de análisis binario ANGR.
A lo largo de los ejercicios del taller, se proporcionaron que tenían como objetivo demostrar aplicaciones potenciales de la tecnología para ayudar a los investigadores de seguridad a llevar a cabo la investigación inversa de ingeniería y vulnerabilidad.
Las diapositivas proporcionan una guía aproximada para el contenido y en qué orden probar los ejercicios.
| Nombre | Tipo | Descripción |
|---|---|---|
| N reinas | Ejemplo | "¿Cómo se pueden colocar n reinas en un tablero de ajedrez NXN para que no dos se ataquen entre sí?" Utiliza Z3 para generar soluciones para un tablero de ajedrez N * n |
| Hackvent 15 | Ejemplo | Solución y caminar para resolver un desafío Hackvent 15 CTF con Z3 |
| Sudoku | Ejercicio | Intenta resolver sudoku usando z3 |
| Rng | Ejercicio | Ejercicios opcionales: usar Z3 para encontrar el valor de semilla de los generadores de números aleatorios no crayrográficamente seguros |
| x86 | 50/50 | Medio ejemplos, medio bricolaje: implementa versiones simiplificadas de instrucciones x86 utilizando Z3 |
| Predicados opacos | Ejercicio | Use las instrucciones implementadas previamente para identificar predicados opacos en pequeñas secuencias de instrucciones de ensamblaje |
| Comprobación de equivalencia | Ejemplo | Use las instrucciones implementadas previamente para identificar secuencias equivalentes de instrucciones |
| Nombre | Tipo | Descripción |
|---|---|---|
| opaco_predicates | Ejemplo | Uso de Angr para identificar predicados opacos con mucho menos trabajo :) |
| Ioctls | Ejemplo | Identificar códigos IOCTL de controlador de Windows usando ANGR |
| Hola Mundo | 50/50 | Ejercicio y tutorial sobre el uso de ANGR para generar argumentos válidos para un simple 'validador de clave de licencia' |
| Laboratorio de bombas | Ejercicio | Ejercicio de bricolaje usando Angr para resolver un 'laboratorio de bombas' |
Todo el código está en Python3 y solo debe instalar el marco de análisis binario ANGR.
mkvirtualenv --python=$(which python3) angr && python -m pip install angr
workon angr
