Pular para o conteúdo principal

Z3 & Symbolic Execution (angr)

Z3 - Solucionador de condições​

Z3 é o Solver SMT (Satisfiability Modulo Theories) desenvolvido para Microsoft. É um solver de restrições que pode resolver equações e lógica simbólica. É usado para encontrar valores que satisfaçam condições específicas.

Para instalar: pip install z3-solver

Por exemplo, se temos as restrições:

x + y = 10
x > 0
y > x

damos elas ao Z3 e ele retorna x = 4, y = 6. (uma das possíveis soluções)

Em pwning, o Z3 pode ser usado para resolver condições complexas de um programa, como:

  • Encontrar a entrada que atinge um certo endereço
  • Resolver equações de overflow
  • Quebrar proteções como stack canaries se puderem ser deduzidos

Porém nós precisamos analisar as condições no código para dar ao z3. Uma vez analisadas as condições, ele faz o resto.

Exemplo​

Suponha que o programa exija um input com as seguintes condições:

  • x + y == 0xdeadbeef
  • x > 0x1000
  • y & 0xff == 0x42 (& é uma operação bit a bit AND)

Vamos usar o Z3 solver para achar x e y:

from z3 import *

x = BitVec('x', 32)  # variável de 32 bits
y = BitVec('y', 32)

s = Solver()
s.add(x + y == 0xdeadbeef)
s.add(x > 0x1000)
s.add(y & 0xff == 0x42)

if s.check() == sat:
    m = s.model()
    print(hex(m[x].as_long()), hex(m[y].as_long()))
elif s.check() == unsat:
    print("Não é possível resolver")

Isto nos retorna 0x1c8f3fad 0xc21e7f42. Se verificarmos em uma calculadora, 0x1c8f3fad + 0xc21e7f42 = 0xdeadbeef.

Z3 CheatSheet​

Variáveis simples (inteiros, booleanos, reais)​

from z3 import *

# Inteiros
x = Int('x')
y = Int('y')

# Booleanas
p = Bool('p')
q = Bool('q')

# Reais
a = Real('a')
b = Real('b')

# Exemplo: resolver x + y = 10, x > y
s = Solver()
s.add(x + y == 10)
s.add(x > y)

if s.check() == sat:
    m = s.model()
    print(f"x = {m[x]}, y = {m[y]}")

Strings​

from z3 import *

# Criar variáveis string
s1 = String('s1')
s2 = String('s2')

# Criar solver com teoria de strings
s = Solver()

# Operações com strings
s.add(Length(s1) == 5)                    # Comprimento
s.add(Concat(s1, s2) == "HelloWorld")     # Concatenação
s.add(Contains(s1, "ell"))                # Contém substring
s.add(PrefixOf("He", s1))                 # É prefixo
s.add(SuffixOf("lo", s1))                 # É sufixo
s.add(s1 == "Hello")                      # Igualdade

# Extrair substring
s.add(SubString(s1, 1, 3) == "el")

# Índice de caracter
s.add(IndexOf(s1, "l", 0) == 2)           # Primeira ocorrência de 'l'

if s.check() == sat:
    print(s.model())

Arrays​

from z3 import *

# Declaração de array: ArraySort(domínio (índice), contradomínio (conteúdo))
A = Array('A', IntSort(), IntSort()) # A = [0,1,2,3] (exemplo)
B = Array('B', IntSort(), BoolSort()) # A[0] = False, A[1] = True (exemplo)

s = Solver()

# Operações básicas
# 1. Store: modificar um elemento
A1 = Store(A, 0, 10)  # A[0] = 10

# 2. Select: acessar um elemento
s.add(Select(A, 0) == 10)
s.add(Select(A, 1) == 20)

# 3. Exemplo mais complexo
x = Int('x')
s.add(x >= 0, x < 5)
s.add(Select(A, x) == 100)

# Array constante
# Criar array onde todos os elementos são 0
const_array = K(IntSort(), 0)
s.add(Select(const_array, 5) == 0)

if s.check() == sat:
    m = s.model()
    print(f"Modelo: {m}")

Arrays de strings​

from z3 import *

# Array de índices inteiros para strings
string_array = Array('string_array', IntSort(), StringSort())

s = Solver()

# Definir valores
s.add(Select(string_array, 0) == "hello")
s.add(Select(string_array, 1) == "world")

# Cria cópia do array com modificação: string_array[2] = "z3"
new_array = Store(string_array, 2, "z3")

if s.check() == sat:
    m = s.model()
    print(f"array[0] = {m.evaluate(Select(string_array, 0))}")

Symbolic Execution​

Symbolic Execution é uma técnica de análise onde as variáveis possuem valores simbólicos (não valores concretos como int, float, str, etc). Em vez de testar com entradas específicas, as entradas são tratadas como variáveis simbólicas e são rastreadas restrições (constraints) sobre esses símbolos à medida que o programa é executado.

Imagine que você pode testar TODAS as entradas possíveis de um programa de uma só vez, sem precisar executá-lo fisicamente milhões de vezes. Isso é análise simbólica. A cada IF/WHILE/FOR, um novo estado é gerado e a saída gerada é analisada.

Por exemplo, temos um programa que diz se um número é positivo:

if x > 0:
    print("Positivo")
else:
    print("Não positivo")
  • Execução normal: Testamos com x = 5 -> Resultado: Positivo
  • Execução simbólica: Usamos x = α (símbolo). Quando chegamos no if, criamos dois caminhos para a condição if($\alpha > 0$):
    1. Estado true: $\alpha > 0\rightarrow$ print: "Positivo"
    2. Estado false: $\alpha \leq 0\rightarrow$ print: "Não positivo"

Como funciona?​

  1. Variáveis simbólicas - As entradas do programa são representadas por símbolos (X, Y).
  2. Valores de variáveis - Os valores das variáveis ficam em função desses símbolos, como uma equação (X + 2)
  3. Path Constraints - São definidas as condições sobre símbolos para alcançar uma parte do código (>, <, ==, etc)
  4. Exploração de caminhos - Em cada branch (if, loop, etc), divide a execução em múltiplos caminhos, adicionando a condição ao conjunto de constraints
  5. Solução com SAT/SMT solver - Depois que encontramos todas as relações e queremos chegar a um caminho específico, agora é só usar um solver para encontrar valores que satisfaçam as constraints.

Angr​

Angr é um framework de análise de binários que implementa Symbolic execution para explorar múltiplos caminhos. Usa SMT solvers (como z3) internamente.

Para instalar: pip install angr

O fluxo de uso básico do angr é:

  1. Carregar binário → angr.Project()
  2. Criar variável → claripy.BVS()
  3. Criar estado → factory.entry_state()
  4. Criar manager → factory.simulation_manager()
  5. Definir condição → função que verifica output
  6. Explorar → sm.explore(find=condicao)
  7. Extrair solução → state.solver.eval()

Como usar​

Carregando um binário​

import angr

# 1. Carregar um programa (binário compilado)
# auto_load_libs=False → Não carrega bibliotecas dinamicamente (mais rápido)
proj = angr.Project('./meu_programa', auto_load_libs=False)

# Informações básicas do projeto
print(f"Arquitetura: {proj.arch}")           # Ex: AMD64, x86
print(f"Entry point: {hex(proj.entry)}")    # Onde o programa começa
print(f"Arquivo: {proj.filename}")

Criando variáveis simbólicas​

Obs: Claripy é o que permite utilizar variáveis simbólicas. É a camada intermediária do angr par aexpressões simbólicas.

import claripy  # Parte do angr para criar variáveis simbólicas

# 2.1 Criando um NÚMERO simbólico (32 bits = int padrão)
numero = claripy.BVS('numero', 32)  # BVS = Bit Vector Symbolic
# 'numero' → nome da variável (para debug)
# 32 → tamanho em bits (32 bits = 4 bytes = int)

# 2.2 Criando uma STRING simbólica
senha = claripy.BVS('senha', 8 * 10)  # 10 caracteres * 8 bits cada
# Isso cria uma sequência de 10 bytes (80 bits)

# 2.3 Criando um ARRAY simbólico
# Array de 5 inteiros (5 * 32 bits)
array = claripy.BVS('array', 32 * 5)
# Ou como lista de variáveis individuais
array_list = [claripy.BVS(f'array_{i}', 32) for i in range(5)]

Criando um estado inicial​

# Um "estado" representa uma possível execução do programa
# Entry state = estado no início do programa

# 3.1 Estado básico
state = proj.factory.entry_state()

# 3.2 Estado com entrada simbólica via STDIN (teclado)
state_com_input = proj.factory.entry_state(
    stdin=senha  # Nossa variável simbólica 'senha'
)

# 3.3 Estado com argumentos de linha de comando
# Se o programa fosse chamado como: ./programa arg1 arg2
state_com_args = proj.factory.entry_state(
    args=['./meu_programa', claripy.BVS('arg1', 8*20)],  # argv[1]
    env={}  # Variáveis de ambiente (vazio por simplicidade)
)

Capturando coisas impressas​

# state.posix.dumps(N) → captura a saída de um "file descriptor"
# Em sistemas Unix/POSIX:
#   0 = stdin  (entrada/input)
#   1 = stdout (saída normal/output)
#   2 = stderr (saída de erro/error)

# Exemplo: capturar o que foi impresso na tela
output = state.posix.dumps(1)  # Pega tudo que foi para stdout
error = state.posix.dumps(2)   # Pega tudo que foi para stderr
input_data = state.posix.dumps(0)  # Pega tudo que foi lido de stdin

# Durante a execução SIMBÓLICA, não executamos realmente o programa
# Mas simulamos. O .dumps() captura dados que SERIAM impressos

Encontrando funções​

# Análise de CFG (Control Flow Graph)
cfg = proj.analyses.CFGFast()

# Listar todas as funções
for func_addr, func in cfg.kb.functions.items():
    if func.name:  # Só funções com nome
        print(f"{func.name}: {hex(func_addr)}")

# Pegar função específica
main_func = cfg.kb.functions.function(name='main')
print(f"\nMain function:")
print(f"  Endereço: {hex(main_func.addr)}")
print(f"  Tamanho: {main_func.size} bytes")
print(f"  Blocos básicos: {len(main_func.blocks)}")

OBS: CFG (Control Flow Graph) é um grafo usado internamente que possui todos os caminhos possíveis. A cada IF/WHILE/FOR, gera-se um novo estado possível cuja saída é capturada pelo angr.

        [main]
           |
           v
    [scanf input] 
           |
           v
    [if (check)]─────┐
           |         |
           v         v
   [print Win]  [print Lose]
           |         |
           v         v
          [exit]   [exit]

Constraints (Importante)​

Podemos adicionar regras (constraints) às variáveis simbólicas. Quanto mais constraints usarmos, menos valores são possíveis, e mais rápida fica a busca. Saber direcionar a busca é extremamente importante, pois para programas mais complexos, o tempo de espera pode ser inviável.

# Sem constraints: x pode ser QUALQUER valor
x = claripy.BVS('x', 32)

# Com constraints: x só pode ser certos valores
state.solver.add(x > 10)    # Constraint 1
state.solver.add(x < 100)   # Constraint 2
state.solver.add(x % 2 == 0) # Constraint 3

# Agora x só pode ser: 12, 14, 16, ..., 98

# Podemos usar múltiplas constraints de uma vez
state.solver.add(x > 10, x < 50)  # 10 < x < 50

OBS: comparações diretas como x > 10 podem falhar. Em geral falham apenas para strings e arrays, mas se falhar, use a conversão abaixo.

c = claripy.BVV(10, 8) # Converter inteiro 10 para bitVec de 8 bits
state.solver.add(x > c)

Enquanto BVS = Bit Vector Symbolic (variável desconhecida), BVV = Bit Vector Value (valor conhecido).

As constraints servem para evitar o problema de path explosion. Imagine o seguinte código:

int main() {
    int x;
    scanf("%d", &x);
    
    if (x > 10) {       // Branch 1
        if (x < 20) {   // Branch 2  
            if (x != 15) {  // Branch 3
                if (x % 2 == 0) {  // Branch 4
                    // ... e assim vai
                }
            }
        }
    }
    return 0;
}

Se analisarmos ele sem constraints, cada "if" DOBRA o número de estados!

  • 2 ifs → 4 estados
  • 3 ifs → 8 estados
  • 10 ifs → 1,024 estados
  • 20 ifs → 1,048,576 estados ← MAIS LENTO

Mas se usarmos constraints:

# Nós SABEMOS que queremos x que chegue no final
x = claripy.BVS('x', 32)
state.solver.add(x > 10)    # Já elimina 50% dos estados!
state.solver.add(x < 20)    # Elimina mais 50%!
state.solver.add(x != 15)   # Elimina 1 estado específico
state.solver.add(x % 2 == 0) # Só pares

# Agora angr só explora caminhos que SATISFAZEM estas condições!

Não precisamos entender todas as constraints do programa, mais quanto mais conseguirmos extrair do código, melhor para o angr.

Constraints para strings​

Podemos adicionar constraints para strings com variavel.get_byte(index):

# Flag tem formato: CTF{XXXXXXXXXXXXXX}
flag = claripy.BVS('flag', 8 * 30)  # 30 bytes

# Constraints por índice específico:
state.solver.add(flag.get_byte(0) == ord('C'))   # Índice 0 = 'C'
state.solver.add(flag.get_byte(1) == ord('T'))   # Índice 1 = 'T'
state.solver.add(flag.get_byte(2) == ord('F'))   # Índice 2 = 'F'
state.solver.add(flag.get_byte(3) == ord('{'))   # Índice 3 = '{'
state.solver.add(flag.get_byte(29) == ord('}'))  # Índice 29 = '}'
state.solver.add(flag.get_byte(30) == 0)         # Índice 30 = null

# Limitando para somente caracteres de a-z, A-Z, 0-9
for i in [4,5,6,7,9,10,11,12,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28]:
    byte = flag.get_byte(i)
    is_alpha_num = claripy.Or(
        claripy.And(byte >= ord('A'), byte <= ord('Z')),
        claripy.And(byte >= ord('a'), byte <= ord('z')),
        claripy.And(byte >= ord('0'), byte <= ord('9'))
    )
    state.solver.add(is_alpha_num)

OBS: ord é uma função do python que retorna o código (valor inteiro) de um caractere ASCII.

Constraints para arrays​

Para arrays simples como lista:

# Array de 10 inteiros (32 bits cada)
array_ints = [claripy.BVS(f'arr_{i}', 32) for i in range(10)]

# Constraints em índices específicos:
state.solver.add(array_ints[0] == 100)       # arr[0] = 100
state.solver.add(array_ints[1] > array_ints[0])  # arr[1] > arr[0]

Para arrays nativos:

# Array de 10 bytes (80 bits) como UMA variável
array = claripy.BVS('array', 8 * 10)  # 10 bytes × 8 bits

# Converter inteiro 10 para BitVec de 8 bits
const = claripy.BVV(10, 8) 

# Constraint no byte específico (índice 3)
state.solver.add(array.get_byte(3) > const)

Para arrays multidimensionais:

# Matriz 3x3
matriz = [[claripy.BVS(f'matriz_{i}_{j}', 32) for j in range(3)] for i in range(3)]

# Constraint específica:
state.solver.add(matriz[0][0] == 1)      # canto superior esquerdo

Hook de funções​

Existem funções muito problemáticas, como rand(), time(), etc. Elas soltam valores diferentes a todo momento, então é conveniente adotar um retorno padrão para elas, permitindo a análise.

import angr

# Hook para função rand() sempre retornar 42
class RandHook(angr.SimProcedure):
    def run(self):
        return 42  # Sempre retorna 42

proj = angr.Project('./programa', auto_load_libs=False)
proj.hook_symbol('rand', RandHook())  # Substitui rand()

Exploração dirigida por endereço de memória​

Podemos fazer uma exploração buscando chegar em um endereço de memória específico.

# Começar do estado inicial
state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)

# 3. Definir endereço alvo (onde queremos chegar)
# Suponha que 0x401234 seja o endereço de "printf("Win!")"
target_addr = 0x401234  # Endereço da string "print Win!"

# Explorar até encontrar um estado nesse endereço
simgr.explore(find=target_addr)

# 5. Verificar resultados
if len(simgr.found) > 0:
    print(f"✅ Encontrado {len(simgr.found)} caminho(s) para 0x{target_addr:x}")
    
    # Para cada estado encontrado
    for i, found_state in enumerate(simgr.found):
        print(f"\n--- Caminho {i+1} ---")
        
        # Podemos obter a entrada que levou até lá
        # Supondo que a entrada estava em stdin
        input_data = found_state.posix.dumps(0)  # stdin
        print(f"Entrada: {input_data}")
        
        # Mostrar onde veio
        print(f"Endereço atual: 0x{found_state.addr:x}")
        
else:
    print("❌ Nenhum caminho encontrado para o endereço alvo")
    print(f"Estados ativos: {simgr.active}")

Erros e problemas comuns​

  • Esquecer auto_load_libs=False
proj = angr.Project('./programa')  # Pode travar
proj = angr.Project('./programa', auto_load_libs=False)  # Correto
  • Variável muito grande
entrada = claripy.BVS('entrada', 1000*8)  # MUITO LENTO
entrada = claripy.BVS('entrada', 50*8)    # Suficiente para maioria
  • Não limitar exploração
simgr.explore(find=alvo)  # Pode rodar indefinidamente
simgr.explore(find=alvo, limit=1000)  # Limita estados
  • Path explosion
# Programa com MUITOS ifs aninhados
if (x > 10) {
    if (y < 20) {
        if (z == 30) {
            // ... e assim por diante
        }
    }
}

# angr vai criar 2^n estados!
# Soluções:
# 1. Usar .explore(limit=N)
# 2. Usar constraints
# 3. Definir find/avoid específicos

Exemplo - Encontrando senha​

Temos o seguinte programa, e queremos, dado um input, obter o output: ACESSO PERMITIDO!\n. O exemplo abaixo é simples, mas a lógica de verificação de senha poderia ser bem mais complexa.

// alvo.c
#include <stdio.h>
#include <string.h>

int main() {
    char senha[20];
    
    printf("Digite a senha: ");
    scanf("%19s", senha);
    
    if (strcmp(senha, "SECRET") == 0) {
        printf("ACESSO PERMITIDO!\n");
        return 0;
    } else {
        printf("ACESSO NEGADO!\n");
        return 1;
    }
}

Usando o angr com claripy:

import angr
import claripy

# PASSO 1: Carregar o programa
proj = angr.Project('./alvo', auto_load_libs=False)

# PASSO 2: Criar variável simbólica para a senha
# "SECRET" tem 6 letras + 1 null byte = 7 bytes
senha_simbolica = claripy.BVS('senha', 7 * 8)  # 7 bytes

# PASSO 3: Criar estado inicial com essa entrada
state = proj.factory.entry_state(stdin=senha_simbolica)

# PASSO 4: Opcional - adicionar restrições (constraints)
# Por exemplo: a senha deve terminar com null byte (\0)
# state.solver.add(senha_simbolica.get_byte(7) == 0)

# PASSO 5: Criar gerenciador de simulação
# Ele controla múltiplos "estados" de execução
simgr = proj.factory.simulation_manager(state)

# PASSO 6: Definir condições de SUCESSO e FRACASSO
def sucesso(state):
    """Identifica estados de sucesso"""
    # Pega o que foi impresso na tela (stdout)
    output = state.posix.dumps(1)  # fd 1 = stdout
    
    # Se contém "ACESSO PERMITIDO", é sucesso!
    return b"ACESSO PERMITIDO" in output

def fracasso(state):
    """Identifica estados de fracasso"""
    output = state.posix.dumps(1)
    return b"ACESSO NEGADO" in output

# PASSO 7: Explorar caminhos até encontrar sucesso
simgr.explore(
    find=sucesso,    # Condição para parar (SUCESSO)
    avoid=fracasso   # Caminhos a evitar (FRACASSO)
)

# PASSO 8: Analisar resultados
if len(simgr.found) > 0:
    print("🎉 SUCESSO! Caminho encontrado")
    
    # Pegar o primeiro estado que levou ao sucesso
    estado_sucesso = simgr.found[0]
    
    # "Resolver" a variável simbólica (Qual valor concreto satisfaz todas as constraints?)
    senha_concreta = estado_sucesso.solver.eval(
        senha_simbolica,      # Variável a resolver
        cast_to=bytes         # Converter para bytes (em vez de número)
    )
    
    # Converter bytes para string (remover null bytes no final)
    senha_string = senha_concreta.decode().split('\x00')[0]
    
    print(f"🔑 Senha encontrada: '{senha_string}'")
    
    # Mostrar mais informações
    print(f"\n📊 Detalhes:")
    print(f"   Endereço final: {hex(estado_sucesso.addr)}")
    print(f"   Bytes brutos: {senha_concreta}")
    
else:
    print("😞 Nenhuma solução encontrada")
    print(f"Estados ativos: {len(simgr.active)}")
    print(f"Estados evitados: {len(simgr.avoided)}")

Exemplo - Minimalista​

import angr
import claripy

# 1. Carrega programa
p = angr.Project('./teste', auto_load_libs=False)

# 2. Cria entrada simbólica (8 bytes)
entrada = claripy.BVS('entrada', 64)  # 64 bits = 8 bytes

# 3. Estado inicial com entrada
s = p.factory.entry_state(stdin=entrada)

# 4. Gerenciador de simulação
sm = p.factory.simulation_manager(s)

# 5. Explorar até encontrar string "WIN"
def win_condition(state):
    return b"WIN" in state.posix.dumps(1)

sm.explore(find=win_condition)

# 6. Resultado
if sm.found:
    solucao = sm.found[0].solver.eval(entrada, cast_to=bytes)
    print(f"Input vencedor: {solucao}")

Quando usar Z3 ou angr?

Quando:

  • A lógica é complexa mas determinística
  • Existem muitas restrições a serem satisfeitas
  • A análise manual seria muito demorada
  • Você precisa gerar inputs específicos automaticamente