z3_and_angr_binary_analysis_workshop

Introdução à análise binária com Z3 e Angr

Originalmente entregue por Sam Brown no Steelcon e Hack.LU 2018, este foi um workshop de três horas que apresentava os participantes a usar o Z3 e o Angr para análise binária. O workshop forneceu uma introdução aos solucionadores de SMT, o Z3 SMT Solver e sua biblioteca Python e a estrutura de análise binária Angr.

Durante todo o workshop, foram fornecidos exercícios com o objetivo de demonstrar possíveis aplicações da tecnologia para ajudar os pesquisadores de segurança a realizar pesquisas de engenharia e vulnerabilidade reversas.

Os slides fornecem um guia aproximado para o conteúdo e qual ordem para experimentar os exercícios.

Exemplos e exercícios

Z3

Nome	Tipo	Descrição
N Queens	Exemplo	- Como o N Queens pode ser colocado em um tabuleiro de xadrez NXN para que dois deles se ataquem? Usa o Z3 para gerar soluções para um tabuleiro de xadrez n * n
Hackvent 15	Exemplo	Solução e caminhe para resolver um desafio Hackvent 15 CTF com Z3
Sudoku	Exercício	Tente resolver sudoku usando Z3
Rng	Exercício	Exercícios opcionais - usando Z3 para encontrar geradores de números aleatórios não criptograficamente seguros
x86	50/50	Meio exemplos, Half DIY - Implemente versões simplificadas de instruções x86 usando Z3
Predicados opacos	Exercício	Use as instruções implementadas anteriormente para identificar predicados opacos em pequenas seqüências de instruções de montagem
Verificação de equivalência	Exemplo	Use as instruções implementadas anteriormente para identificar sequências equivalentes de instruções

Angr

Nome	Tipo	Descrição
opaque_predicates	Exemplo	Usando Angr para identificar predicados opacos com muito menos trabalho :)
Ioctls	Exemplo	Identifique os códigos IOCTL do driver do Windows usando Angr
Olá mundo	50/50	Exercite -se e passo a passo sobre o uso de Angr para gerar argumentos válidos para um simples 'Chave de licença validador'
Laboratório de bombas	Exercício	Exercício DIY usando Angr para resolver um 'laboratório de bomba'

Configurar

Todo o código está no Python3 e você deve apenas instalar a estrutura de análise binária.

 mkvirtualenv --python=$(which python3) angr && python -m pip install angr
workon angr