11.12.2024

Lição: 292: Execução Simbólica com Manticore

No mundo dos contratos inteligentes e blockchain, garantir a correção e segurança do seu código é fundamental. Um método eficaz para verificar contratos inteligentes é a execução simbólica, uma técnica que nos permite explorar todos os possíveis caminhos de execução de um programa. O Manticore é uma poderosa ferramenta de execução simbólica que podemos usar para analisar contratos inteligentes do Ethereum escritos em Solidity. Esta aula irá guiá-lo pelos fundamentos da execução simbólica usando o Manticore, juntamente com exemplos práticos.

O que é Manticore?

Manticore é um mecanismo de execução simbólica desenvolvido para contratos inteligentes e binários. Ele permite que pesquisadores de segurança e desenvolvedores analisem o código em busca de vulnerabilidades, simulando cada caminho possível de execução. O Manticore interpreta o bytecode de contratos inteligentes e fornece uma estrutura para explorar diferentes entradas e condições sem realmente executar transações na rede Ethereum.

Configurando o Manticore

Antes de usarmos o Manticore, precisamos tê-lo instalado em nosso sistema. Você pode instalá-lo seguindo estas etapas:

1. Verifique se você tem o Python 3.6 ou posterior instalado.

2. Instale o Manticore usando o pip:

   pip install manticore

3. Instale as dependências necessárias para Solidity:

   sudo apt-get install python3-dev libffi-dev gcc build-essential

Uma vez instalado, você pode usar o Manticore para analisar contratos inteligentes.

Exemplo de Contrato Inteligente

Vamos criar um contrato inteligente simples em Solidity que iremos analisar com o Manticore. Aqui está um contrato básico que inclui uma função vulnerável permitindo que qualquer usuário deposite fundos:

pragma solidity ^0.8.0;

contract Vulnerable {
    mapping(address => uint) public balances;

    function deposit() public payable {
        require(msg.value > 0, "Você deve enviar ether");
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint amount) public {
        require(balances[msg.sender] >= amount, "Saldo insuficiente");
        (bool success, ) = msg.sender.call{value: amount}("");
        require(success, "Transferência falhou");
        balances[msg.sender] -= amount;
    }
}

Este contrato permite que os usuários depositem e retirem Ether. No entanto, a função withdraw é vulnerável a ataques de reentrada porque atualiza o saldo após enviar o Ether.

Analisando com Manticore

Podemos usar o Manticore para analisar nosso contrato vulnerável. Primeiro, compile o contrato usando o compilador Solidity e obtenha o bytecode e o ABI. Salve o bytecode do contrato em um arquivo chamado vulnerable.bin.

Executando o Manticore

Agora, vamos usar o Manticore para explorar o contrato:

manticore vulnerable.bin

À medida que o Manticore é executado, ele analisará os diferentes caminhos de execução do contrato e ajudará a identificar potenciais vulnerabilidades. Dentro do ambiente do Manticore, você verá várias restrições e condições geradas para cada caminho.

Escrevendo Testes para o Manticore

Aqui está um script de exemplo usando o Manticore para testar a função withdraw para encontrar vulnerabilidades de reentrada.

from manticore.ethereum import ManticoreEVM

class VulnerableToken(ManticoreEVM):
    def __init__(self):
        super().__init__()
        self.contract = self.solidity_compile('''
        pragma solidity ^0.8.0;

        contract Vulnerable {
            mapping(address => uint) public balances;

            function deposit() public payable {
                require(msg.value > 0, "Você deve enviar ether");
                balances[msg.sender] += msg.value;
            }

            function withdraw(uint amount) public {
                require(balances[msg.sender] >= amount, "Saldo insuficiente");
                (bool success, ) = msg.sender.call{value: amount}("");
                require(success, "Transferência falhou");
                balances[msg.sender] -= amount;
            }
        }
        ''')  # Esta linha é onde você define seu contrato dentro do Manticore.

    def test_reentrancy(self):
        # Gerar valores simbólicos para o atacante
        attacker_balance = self.MK_UINT(1)  # O atacante tem algum Ether
        self.contract.deposit.value(attacker_balance)()  # Chama depósito com valor simbólico

        # Chama a função withdraw
        withdraw_amount = self.MK_UINT(1)  # O atacante tenta retirar

        # Executa withdraw
        self.contract.withdraw(withdraw_amount)

VulnerableToken().run()

Este script configura um ambiente Manticore para verificar a vulnerabilidade de reentrada na função withdraw. Ele simula um atacante que deposita Ether e depois tenta retirar, potencialmente levando à reentrada.

Interpretação dos Resultados

Após executar a análise, o Manticore gerará saídas que indicam os caminhos explorados, assim como quaisquer estados onde um ataque poderia potencialmente ter sucesso. Ao se concentrar em reentrâncias, procure estados onde a verificação do saldo passa, mas antes da atualização do saldo ocorrer.

Conclusão

O Manticore é uma ferramenta poderosa para desenvolvedores e pesquisadores de segurança analisarem e verificarem a segurança de contratos inteligentes por meio da execução simbólica. Nesta aula, aprendemos sobre execução simbólica, configuramos o Manticore e analisamos um contrato vulnerável básico.

Continue explorando os recursos do Manticore, experimente contratos mais complexos e mantenha a ênfase na segurança para garantir que seus contratos inteligentes permaneçam robustos e seguros. Boa codificação!

Navigation