Z3 parte 2 - Simples desafio de engenharia reversa
Este é o terceiro artigo da série de artigos Z3 Para o segundo artigo, Para o primeiro artigo
No artigo anterior, eu lhe dei um desafio de engenharia reversa: Para baixar o desafio
No desafio você tem um arquivo simples que pede um nome de usuário e senha, você precisa encontrar o nome de usuário e senha, assim:
Antes de ver minha solução para o desafio, eu recomendo fortemente que você tente resolvê-lo sozinho.
No próximo vídeo eu mostrei como resolver o desafio usando IDA + OllyDbg e finalmente como resolver o desafio também usando Z3 que é o assunto do artigo.
Para o video:
No vídeo eu usei o OllyDbg eu configurei e adicionei todos os plugins mais úteis a ele, se você estiver interessado no OllyDbg que configurei você pode baixá-lo diretamente do meu Github:
https://github.com/romanzaikin/OllyDbg-v1.10-With-Best-Plugins-And-Immunity-Debugger-theme-
Neste artigo, não vou me referir à engenharia reversa do desafio, mas sim à solução do desafio usando Z3, sobre como resolver com engenharia reversa que você pode ver no vídeo.
Começaremos abrindo o desafio no IDA, que será assim:
Para encontrar o código principal do software basta usar shift + f12 e pesquisar o texto impresso na tela “nome de usuário” sendo que:
Clique no texto duas vezes e vá para a área de memória onde está definido dentro do-data section:
A propósito, nesta área você também pode encontrar o nome de usuário do software que é "root", clique na linha do nome de usuário e depois clique em "x", para abrirmos a janela-xref:
Clique em ok e você alcançará o código do software:
Agora pressione F5 que executará hexrays no código:
Você pode ver que o número de caracteres que precisamos inserir deve ser menor ou igual a 0xb e então precisamos inserir caracteres para a senha que serão iguais a-[dword_41A900[i Que contém a seguinte lista:
Vamos copiar a lista:
data = [0x2121, 0x3568, 0x33F6, 0x2c6c, 0x2857,0x24f0,0x30a0,0x12cd,0x14c1,0x18f0,0x1AD8]
E vamos resolver o exercício usando z3.
Devemos primeiro definir nossas variáveis, cada uma das quais será, na verdade, um caractere da senha, para fazer isso, podemos definir dinamicamente as variáveis diretamente usando global assim:
`from z3 import *
username = bytearray("root")
data = [0x2121, 0x3568, 0x33F6, 0x2c6c, 0x2857, 0x24f0, 0x30a0, 0x12cd, 0x14c1, 0x18f0, 0x1AD8]
solver = Solver()
for i in xrange(11):
globals()["b{}".format(i)] = BitVec("b{}".format(i),32)`
Em seguida, precisamos definir o valor decimal dos caracteres que permitimos que o z3 insira para obter a senha:
solver.add(And(globals()["b{}".format(i)] > 48, globals()["b{}".format(i)] < 122))
E, finalmente, definiremos uma lei simples com base nas condições que extraimos-IDA:
solver.add((username[i % 4] ^ 0x14) * globals()["b{}".format(i)] + ( globals()["b{}".format(i)] ^ 0x4d) - 15 == data[i])
O código completo ficará assim:
Assim que executarmos o código, obteremos a resposta ao desafio:
No vídeo eu mostrei a vocês que existe outra maneira de resolver o desafio e que é realmente aproveitar o bug existente no desafio:
Se olharmos para o loop, parece que ela existe (strlen(a2 Vezes, que é basicamente a quantidade de caracteres na senha.
Mas e se a senha não tiver nenhum caractere?
Então o strlen retornará 0 e o loop não será executado, que retornará o valor 1 e receberá o texto "Acesso concedido" sem a necessidade de senha.
