MASTG-TECH-0089: Execução Simbólica (Symbolic Execution)

Você pode encontrar uma introdução à análise binária usando frameworks de análise binária em Análise Dinâmica no Android. Recomendamos que você revise esse conteúdo e refresque os conceitos sobre este assunto.

Para Android, utilizamos o motor de execução simbólica do Angr para resolver um desafio. Nesta seção, usaremos primeiro o Unicorn para resolver o desafio iOS UnCrackable Nível 1 e depois revisitaremos o framework de análise binária Angr para analisar o desafio, mas em vez de execução simbólica, usaremos seus recursos de execução concreta (ou execução dinâmica).

Angr¶

Angr é uma ferramenta muito versátil, fornecendo múltiplas técnicas para facilitar a análise binária, enquanto suporta diversos formatos de arquivo e conjuntos de instruções de hardware.

O backend Mach-O no Angr não é bem suportado, mas funciona perfeitamente para o nosso caso.

Ao analisar manualmente o código em Análise de Código Native Desmontado, chegamos a um ponto em que realizar mais análises manuais tornou-se incômodo. A função no offset 0x1000080d4 foi identificada como o alvo final que contém a string secreta.

Se revisitarmos essa função, podemos ver que ela envolve múltiplas chamadas de subfunções e, interessantemente, nenhuma dessas funções tem dependências de outras chamadas de biblioteca ou chamadas de sistema. Este é um caso perfeito para usar o motor de execução concreta do Angr. Siga os passos abaixo para resolver este desafio:

Obtenha a versão ARM64 do binário executando lipo -thin arm64 <app_binary> -output uncrackable.arm64 (ARMv7 também pode ser usado).
Crie um Project do Angr carregando o binário acima.
Obtenha um objeto callable passando o endereço da função a ser executada. Da documentação do Angr: "Um Callable é uma representação de uma função no binário que pode ser interagida como uma função nativa do Python.".
Passe o objeto callable acima para o motor de execução concreta, que neste caso é claripy.backends.concrete.
Acesse a memória e extraia a string do ponteiro retornado pela função acima.

import angr
import claripy

def solve():

    # Carrega o binário criando um projeto do angr.
    project = angr.Project('uncrackable.arm64')

    # Passa o endereço da função para o callable
    func = project.factory.callable(0x1000080d4)

    # Obtém o valor de retorno da função
    ptr_secret_string = claripy.backends.concrete.convert(func()).value
    print("Endereço do ponteiro para a string secreta: " + hex(ptr_secret_string))

    # Extrai o valor do ponteiro para a string secreta
    secret_string = func.result_state.mem[ptr_secret_string].string.concrete
    print(f"String Secreta: {secret_string}")

solve()

Acima, o Angr executou um código ARM64 em um ambiente de execução fornecido por um de seus motores de execução concreta. O resultado é acessado da memória como se o programa fosse executado em um dispositivo real. Este caso é um bom exemplo onde os frameworks de análise binária nos permitem realizar uma análise abrangente de um binário, mesmo na ausência de dispositivos especializados necessários para executá-lo.