z3_and_angr_binary_analysis_workshop
1.0.0
Initialement livré par Sam Brown chez Steelcon et Hack.LU 2018, il s'agissait d'un atelier de trois heures présentant les participants à utiliser Z3 et ANGR pour une analyse binaire. L'atelier a fourni une introduction aux solveurs SMT, au solveur SMT Z3 et à sa bibliothèque Python et au cadre d'analyse binaire ANGR.
Au cours des exercices d'atelier, des exercices ont été fournis, ce qui visait à démontrer des applications potentielles de la technologie pour aider les chercheurs en sécurité à effectuer une recherche sur l'ingénierie inverse et la recherche sur la vulnérabilité.
Les diapositives fournissent un guide approximatif pour le contenu et quel ordre d'essayer les exercices.
| Nom | Taper | Description |
|---|---|---|
| N queens | Exemple | «Comment les N Queens peuvent-ils être placés sur un échec NXN pour que ces deux ne s'attaquent pas? Utilise Z3 pour générer des solutions pour un échec n * n |
| Hackvent 15 | Exemple | Solution et promenade pour résoudre un défi de Hackvent 15 CTF avec Z3 |
| Sudoku | Exercice | Essayez de résoudre Sudoku en utilisant Z3 |
| RNG | Exercice | Exercices facultatifs - Utilisation de Z3 pour trouver la valeur de semence des générateurs de nombres aléatoires non critiqués |
| x86 | 50/50 | Demi-exemples, demi-bricol |
| Prédicats opaques | Exercice | Utilisez les instructions implémentées précédemment pour identifier les prédicats opaques dans de petites séquences d'instructions d'assemblage |
| Vérification de l'équivalence | Exemple | Utilisez les instructions implémentées précédemment pour identifier des séquences d'instructions équivalentes |
| Nom | Taper | Description |
|---|---|---|
| opaque_predicats | Exemple | Utiliser ANGR pour identifier les prédicats opaques avec beaucoup moins de travail :) |
| Ioctls | Exemple | Identifier les codes IOCTL du pilote Windows à l'aide d'ANGR |
| Bonjour le monde | 50/50 | Exercice et procédure pas à pas sur l'utilisation d'ANGR pour générer des arguments valides pour un simple «validateur de clé de licence» |
| Laboratoire de bombe | Exercice | Exercice de bricolage utilisant ANGR pour résoudre un «laboratoire de bombes» |
Tout le code est dans Python3 et vous ne devriez avoir besoin que d'installer le cadre d'analyse binaire ANGR.
mkvirtualenv --python=$(which python3) angr && python -m pip install angr
workon angr
