Execução simbólica¶
A execução simbólica é uma técnica muito útil para se ter em sua caixa de ferramentas, especialmente ao lidar com problemas em que você precisa encontrar uma entrada correta para alcançar um determinado bloco de código. Nesta seção, resolveremos um simples crackme para Android usando a estrutura de análise binária Angr como nosso mecanismo de execução simbólica.
Para demonstrar esta técnica, usaremos um crackme chamado Validador de Licença Android. O crackme consiste em um único arquivo executável ELF, que pode ser executado em qualquer dispositivo Android seguindo as instruções abaixo:
$ adb push validate /data/local/tmp
[100%] /data/local/tmp/validate
$ adb shell chmod 755 /data/local/tmp/validate
$ adb shell /data/local/tmp/validate
Uso: ./validate <serial>
$ adb shell /data/local/tmp/validate 12345
Serial incorreto (formato errado).
Até aqui tudo bem, mas não sabemos nada sobre como é uma chave de licença válida. Para começar, abra o executável ELF em um desmontador como iaito. A função principal está localizada no deslocamento 0x00001874 na desmontagem. É importante notar que este binário está habilitado para PIE, e o iaito escolhe carregar o binário em 0x0 como endereço base da imagem.
Os nomes das funções foram removidos do binário, mas felizmente há strings de depuração suficientes para nos fornecer contexto sobre o código. Avançando, começaremos a analisar o binário a partir da função de entrada no deslocamento 0x00001874, e manteremos uma nota de todas as informações facilmente disponíveis para nós. Durante esta análise, também tentaremos identificar as regiões de código que são adequadas para execução simbólica.
strlen é chamado no deslocamento 0x000018a8, e o valor retornado é comparado a 0x10 no deslocamento 0x000018b0. Imediatamente após isso, a string de entrada é passada para uma função de decodificação Base32 no deslocamento 0x00001340. Isso nos fornece informações valiosas de que a chave de licença de entrada é uma string de 16 caracteres codificada em Base32 (que totaliza 10 bytes em bruto). A entrada decodificada é então passada para a função no deslocamento 0x00001760, que valida a chave de licença. A desmontagem desta função é mostrada abaixo.
Agora podemos usar esta informação sobre a entrada esperada para analisar mais a fundo a função de validação em 0x00001760.
╭ (fcn) fcn.00001760 268
│ fcn.00001760 (int32_t arg1);
│ ; var int32_t var_20h @ fp-0x20
│ ; var int32_t var_14h @ fp-0x14
│ ; var int32_t var_10h @ fp-0x10
│ ; arg int32_t arg1 @ r0
│ ; CALL XREF from fcn.00001760 (+0x1c4)
│ 0x00001760 push {r4, fp, lr}
│ 0x00001764 add fp, sp, 8
│ 0x00001768 sub sp, sp, 0x1c
│ 0x0000176c str r0, [var_20h] ; 0x20 ; "$!" ; arg1
│ 0x00001770 ldr r3, [var_20h] ; 0x20 ; "$!" ; entry.preinit0
│ 0x00001774 str r3, [var_10h] ; str.
│ ; 0x10
│ 0x00001778 mov r3, 0
│ 0x0000177c str r3, [var_14h] ; 0x14
│ ╭─< 0x00001780 b 0x17d0
│ │ ; CODE XREF from fcn.00001760 (0x17d8)
│ ╭──> 0x00001784 ldr r3, [var_10h] ; str.
│ │ ; 0x10 ; entry.preinit0
│ ╎│ 0x00001788 ldrb r2, [r3]
│ ╎│ 0x0000178c ldr r3, [var_10h] ; str.
│ ╎│ ; 0x10 ; entry.preinit0
│ ╎│ 0x00001790 add r3, r3, 1
│ ╎│ 0x00001794 ldrb r3, [r3]
│ ╎│ 0x00001798 eor r3, r2, r3
│ ╎│ 0x0000179c and r2, r3, 0xff
│ ╎│ 0x000017a0 mvn r3, 0xf
│ ╎│ 0x000017a4 ldr r1, [var_14h] ; 0x14 ; entry.preinit0
│ ╎│ 0x000017a8 sub r0, fp, 0xc
│ ╎│ 0x000017ac add r1, r0, r1
│ ╎│ 0x000017b0 add r3, r1, r3
│ ╎│ 0x000017b4 strb r2, [r3]
│ ╎│ 0x000017b8 ldr r3, [var_10h] ; str.
│ ╎│ ; 0x10 ; entry.preinit0
│ ╎│ 0x000017bc add r3, r3, 2 ; "ELF\x01\x01\x01" ; aav.0x00000001
│ ╎│ 0x000017c0 str r3, [var_10h] ; str.
│ ╎│ ; 0x10
│ ╎│ 0x000017c4 ldr r3, [var_14h] ; 0x14 ; entry.preinit0
│ ╎│ 0x000017c8 add r3, r3, 1
│ ╎│ 0x000017cc str r3, [var_14h] ; 0x14
│ ╎│ ; CODE XREF from fcn.00001760 (0x1780)
│ ╎╰─> 0x000017d0 ldr r3, [var_14h] ; 0x14 ; entry.preinit0
│ ╎ 0x000017d4 cmp r3, 4 ; aav.0x00000004 ; aav.0x00000001 ; aav.0x00000001
│ ╰──< 0x000017d8 ble 0x1784 ; provável
│ 0x000017dc ldrb r4, [fp, -0x1c] ; "4"
│ 0x000017e0 bl fcn.000016f0
│ 0x000017e4 mov r3, r0
│ 0x000017e8 cmp r4, r3
│ ╭─< 0x000017ec bne 0x1854 ; provável
│ │ 0x000017f0 ldrb r4, [fp, -0x1b]
│ │ 0x000017f4 bl fcn.0000170c
│ │ 0x000017f8 mov r3, r0
│ │ 0x000017fc cmp r4, r3
│ ╭──< 0x00001800 bne 0x1854 ; provável
│ ││ 0x00001804 ldrb r4, [fp, -0x1a]
│ ││ 0x00001808 bl fcn.000016f0
│ ││ 0x0000180c mov r3, r0
│ ││ 0x00001810 cmp r4, r3
│ ╭───< 0x00001814 bne 0x1854 ; provável
│ │││ 0x00001818 ldrb r4, [fp, -0x19]
│ │││ 0x0000181c bl fcn.00001728
│ │││ 0x00001820 mov r3, r0
│ │││ 0x00001824 cmp r4, r3
│ ╭────< 0x00001828 bne 0x1854 ; provável
│ ││││ 0x0000182c ldrb r4, [fp, -0x18]
│ ││││ 0x00001830 bl fcn.00001744
│ ││││ 0x00001834 mov r3, r0
│ ││││ 0x00001838 cmp r4, r3
│ ╭─────< 0x0000183c bne 0x1854 ; provável
│ │││││ 0x00001840 ldr r3, [0x0000186c] ; [0x186c:4]=0x270 section..hash ; section..hash
│ │││││ 0x00001844 add r3, pc, r3 ; 0x1abc ; "Product activation passed. Congratulations!"
│ │││││ 0x00001848 mov r0, r3 ; 0x1abc ; "Product activation passed. Congratulations!" ;
│ │││││ 0x0000184c bl sym.imp.puts ; int puts(const char *s)
│ │││││ ; int puts("Product activation passed. Congratulations!")
│ ╭──────< 0x00001850 b 0x1864
│ ││││││ ; CODE XREFS from fcn.00001760 (0x17ec, 0x1800, 0x1814, 0x1828, 0x183c)
│ │╰╰╰╰╰─> 0x00001854 ldr r3, aav.0x00000288 ; [0x1870:4]=0x288 aav.0x00000288
│ │ 0x00001858 add r3, pc, r3 ; 0x1ae8 ; "Incorrect serial." ;
│ │ 0x0000185c mov r0, r3 ; 0x1ae8 ; "Incorrect serial." ;
│ │ 0x00001860 bl sym.imp.puts ; int puts(const char *s)
│ │ ; int puts("Incorrect serial.")
│ │ ; CODE XREF from fcn.00001760 (0x1850)
│ ╰──────> 0x00001864 sub sp, fp, 8
╰ 0x00001868 pop {r4, fp, pc} ; entry.preinit0 ; entry.preinit0 ;
Discutir todas as instruções na função está além do escopo deste capítulo, em vez disso, discutiremos apenas os pontos importantes necessários para a análise. Na função de validação, há um loop presente em 0x00001784 que realiza uma operação XOR no deslocamento 0x00001798. O loop é mais claramente visível na visualização de grafo abaixo.
XOR é uma técnica muito comumente usada para criptografar informações onde ofuscação é o objetivo em vez de segurança. XOR não deve ser usado para qualquer criptografia séria, pois pode ser quebrado usando análise de frequência. Portanto, a mera presença de criptografia XOR em tal lógica de validação sempre requer atenção e análise especiais.
Prosseguindo, no deslocamento 0x000017dc, o valor decodificado por XOR obtido acima está sendo comparado com o valor de retorno de uma sub-chamada de função em 0x000017e8.
Claramente, esta função não é complexa e pode ser analisada manualmente, mas ainda assim permanece uma tarefa árdua. Especialmente ao trabalhar em uma grande base de código, o tempo pode ser uma restrição importante, e é desejável automatizar tal análise. A execução simbólica dinâmica é útil exatamente nessas situações. No crackme acima, o mecanismo de execução simbólica pode determinar as restrições em cada byte da string de entrada mapeando um caminho entre a primeira instrução da verificação de licença (em 0x00001760) e o código que imprime a mensagem "Product activation passed" (em 0x00001840).
As restrições obtidas das etapas acima são passadas para um mecanismo solver, que encontra uma entrada que as satisfaça - uma chave de licença válida.
Você precisa realizar várias etapas para inicializar o mecanismo de execução simbólica do Angr:
-
Carregar o binário em um
Project, que é o ponto de partida para qualquer tipo de análise no Angr. -
Passar o endereço a partir do qual a análise deve começar. Neste caso, inicializaremos o estado com a primeira instrução da função de validação de serial. Isso torna o problema significativamente mais fácil de resolver porque você evita executar simbolicamente a implementação Base32.
-
Passar o endereço do bloco de código que a análise deve alcançar. Neste caso, é o deslocamento
0x00001840, onde está localizado o código responsável por imprimir a mensagem "Product activation passed". -
Além disso, especificar os endereços que a análise não deve alcançar. Neste caso, o bloco de código que imprime a mensagem "Incorrect serial" em
0x00001854não é interessante.
Observe que o carregador do Angr carregará o executável PIE com um endereço base de
0x400000, que precisa ser adicionado aos deslocamentos do iaito antes de passá-lo para o Angr.
O script de solução final é apresentado abaixo:
import angr # Versão: 9.2.2
import base64
load_options = {}
b = angr.Project("./validate", load_options = load_options)
# A função de validação da chave começa em 0x401760, então é onde criamos o estado inicial.
# Isso acelera muito as coisas porque estamos contornando o codificador Base32.
options = {
angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS,
}
state = b.factory.blank_state(addr=0x401760, add_options=options)
simgr = b.factory.simulation_manager(state)
simgr.explore(find=0x401840, avoid=0x401854)
# 0x401840 = Product activation passed
# 0x401854 = Incorrect serial
found = simgr.found[0]
# Obtém a string solução de *(R11 - 0x20).
addr = found.memory.load(found.regs.r11 - 0x20, 1, endness="Iend_LE")
concrete_addr = found.solver.eval(addr)
solution = found.solver.eval(found.memory.load(concrete_addr,10), cast_to=bytes)
print(base64.b32encode(solution))
Como discutido anteriormente na seção "Instrumentação Binária Dinâmica))", o mecanismo de execução simbólica constrói uma árvore binária das operações para a entrada do programa fornecida e gera uma equação matemática para cada caminho possível que pode ser tomado. Internamente, o Angr explora todos os caminhos entre os dois pontos especificados por nós, e passa as equações matemáticas correspondentes para o solver retornar resultados concretos significativos. Podemos acessar essas soluções via lista simulation_manager.found, que contém todos os caminhos possíveis explorados pelo Angr que satisfazem nossos critérios de busca especificados.
Observe mais de perto a parte posterior do script onde a string de solução final está sendo recuperada. O endereço da string é obtido do endereço r11 - 0x20. Isso pode parecer mágico à primeira vista, mas uma análise cuidadosa da função em 0x00001760 contém a pista, pois determina se a string de entrada fornecida é uma chave de licença válida ou não. Na desmontagem acima, você pode ver como a string de entrada para a função (no registrador R0) é armazenada em uma variável local da stack 0x0000176c str r0, [var_20h]. Portanto, decidimos usar este valor para recuperar a solução final no script. Usando found.solver.eval você pode fazer perguntas ao solver como "dada a saída desta sequência de operações (o estado atual em found), qual deve ter sido a entrada (em addr)?".
Em ARMv7, R11 é chamado fp (function pointer), portanto
R11 - 0x20é equivalente afp-0x20:var int32_t var_20h @ fp-0x20
Em seguida, o parâmetro endness no script especifica que os dados são armazenados no formato "little-endian", que é o caso para quase todos os dispositivos Android.
Além disso, pode parecer que o script está simplesmente lendo a string solução da memória do script. No entanto, está lendo da memória simbólica. Nem a string nem o ponteiro para a string realmente existem. O solver garante que a solução que fornece é a mesma como se o programa fosse executado até aquele ponto.
Executar este script deve retornar a seguinte saída:
$ python3 solve.py
WARNING | ... | cle.loader | O binário principal é um executável independente de posição. Está sendo carregado com um endereço base de 0x400000.
b'JACE6ACIARNAAIIA'
Agora você pode executar o binário validate em seu dispositivo Android para verificar a solução (consulte Validador de Licença Android).
Você pode obter soluções diferentes usando o script, pois existem várias chaves de licença válidas possíveis.
Para concluir, aprender execução simbólica pode parecer um pouco intimidador no início, pois requer compreensão profunda e prática extensiva. No entanto, o esforço é justificado considerando o tempo valioso que pode economizar em contraste com a análise manual de instruções desmontadas complexas. Normalmente, você usaria técnicas híbridas, como no exemplo acima, onde realizamos análise manual do código desmontado para fornecer os critérios corretos para o mecanismo de execução simbólica. Consulte o capítulo iOS para mais exemplos de uso do Angr.