Como usar o Manticore para encontrar bugs em contratos inteligentes

O objetivo deste tutorial é mostrar como usar o Manticore para encontrar bugs em contratos inteligentes automaticamente.

Instalação

Manticore requer >= python 3.6. Pode ser instalado via pip ou usando o docker.

Manticore via docker

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

O último comando executa o eth-security-toolbox em um docker que tem acesso ao seu diretório atual. Você pode alterar os arquivos do seu host e executar as ferramentas nos arquivos do docker

Dentro do docker, execute:

solc-select 0.5.11
cd /home/trufflecon/

Manticore via pip

pip3 install --user manticore

solc 0.5.11 é recomendado.

Executando um script

Para executar um script python com python 3:

python3 script.py

Introdução à execução simbólica dinâmica

Execução Simbólica Dinâmica em poucas palavras

A execução simbólica dinâmica (DSE) é uma técnica de análise de programa que explora um espaço de estado com um alto grau de consciência semântica. Esta técnica é baseada na descoberta de "caminhos de programa", representados como fórmulas matemáticas chamadas de predicados de caminho. Conceitualmente, esta técnica opera em predicados de caminho em duas etapas:

1. Eles são construídos usando restrições na entrada do programa.
2. Eles são usados para gerar entradas de programa que farão com que os caminhos associados sejam executados.

Esta abordagem não produz falsos positivos, no sentido de que todos os estados de programa identificados podem ser acionados durante a execução concreta. Por exemplo, se a análise encontrar um integer overflow, é garantido que será reproduzível.

Exemplo de Predicado de Caminho

Para ter uma ideia de como o DSE funciona, considere o seguinte exemplo:

1function f(uint a){
2
3  if (a == 65) {
4      // Um bug está presente
5  }
6
7}
Copiar

Como f() contém dois caminhos, um DSE construirá dois predicados de caminho diferentes:

• Caminho 1: a == 65
• Caminho 2: Not (a == 65)

Cada predicado de caminho é uma fórmula matemática que pode ser fornecida a um chamado solucionador SMT (opens in a new tab), que tentará resolver a equação. Para o Caminho 1, o solucionador dirá que o caminho pode ser explorado com a = 65. Para o Caminho 2, o solucionador pode atribuir a a qualquer valor diferente de 65, por exemplo a = 0.

Verificando propriedades

O Manticore permite controle total sobre toda a execução de cada caminho. Como resultado, ele permite que você adicione restrições arbitrárias a quase tudo. Este controle permite a criação de propriedades no contrato.

Considere o seguinte exemplo:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // sem proteção contra overflow
3  return c;
4}
Copiar

Aqui, há apenas um caminho a ser explorado na função:

• Caminho 1: c = a + b

Usando o Manticore, você pode verificar se há overflow e adicionar restrições ao predicado de caminho:

• c = a + b AND (c < a OR c < b)

Se for possível encontrar uma valoração de a e b para a qual o predicado de caminho acima seja viável, significa que você encontrou um overflow. Por exemplo, o solucionador pode gerar a entrada a = 10, b = MAXUINT256.

Se você considerar uma versão corrigida:

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
Copiar

A fórmula associada com a verificação de overflow seria:

• c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

Esta fórmula não pode ser resolvida; em outras palavras, esta é uma prova de que em safe_add, c sempre aumentará.

O DSE é, portanto, uma ferramenta poderosa que pode verificar restrições arbitrárias em seu código.

Executando no Manticore

Veremos como explorar um contrato inteligente com a API do Manticore. O alvo é o seguinte contrato inteligente example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
Exibir tudo
Copiar

Execute uma exploração autônoma

Você pode executar o Manticore diretamente no contrato inteligente com o seguinte comando (project pode ser um arquivo Solidity ou um diretório de projeto):

$ manticore project

Você receberá a saída de casos de teste como este (a ordem pode mudar):

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
Exibir tudo

Sem informações adicionais, o Manticore explorará o contrato com novas transações simbólicas até que não explore novos caminhos no contrato. O Manticore não executa novas transações após uma que falhou (ex: após uma reversão).

O Manticore produzirá a informação em um diretório mcore_*. Entre outras coisas, você encontrará neste diretório:

• global.summary: cobertura e avisos do compilador
• test_XXXXX.summary: cobertura, última instrução, saldos da conta por caso de teste
• test_XXXXX.tx: lista detalhada de transações por caso de teste

Aqui o Manticore encontra 7 casos de teste, que correspondem a (a ordem do nome do arquivo pode mudar):

Resumo da exploração f(!=65) denota f chamado com qualquer valor diferente de 65.

Como você pode perceber, o Manticore gera um caso de teste único para cada transação bem-sucedida ou revertida.

Use a flag --quick-mode se você quiser uma exploração rápida de código (ela desativa detectores de bugs, computação de gás, ...)

Manipular um contrato inteligente através da API

Esta seção descreve em detalhes como manipular um contrato inteligente através da API Python do Manticore. Você pode criar um novo arquivo com a extensão python *.py e escrever o código necessário adicionando os comandos da API (cujos fundamentos serão descritos abaixo) neste arquivo e, em seguida, executá-lo com o comando $ python3 *.py. Você também pode executar os comandos abaixo diretamente no console do python; para executar o console, use o comando $ python3.

Criando Contas

A primeira coisa que você deve fazer é iniciar uma nova cadeia de blocos com os seguintes comandos:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
Copiar

Uma conta que não seja de contrato é criada usando m.create_account (opens in a new tab):

1user_account = m.create_account(balance=1000)
Copiar

Um contrato Solidity pode ser implantado usando m.solidity_create_contract (opens in a new tab):

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Iniciar o contrato
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Exibir tudo
Copiar

Resumo

• Você pode criar contas de usuário e de contrato com m.create_account (opens in a new tab) e m.solidity_create_contract (opens in a new tab).

Executando transações

O Manticore suporta dois tipos de transação:

• Transação bruta: todas as funções são exploradas
• Transação nomeada: apenas uma função é explorada

Transação bruta

Uma transação bruta é executada usando m.transaction (opens in a new tab):

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
Copiar

O chamador, o endereço, os dados ou o valor da transação podem ser concretos ou simbólicos:

• m.make_symbolic_value (opens in a new tab) cria um valor simbólico.
• m.make_symbolic_buffer(size) (opens in a new tab) cria uma matriz de bytes simbólica.

Por exemplo:

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
Copiar

Se os dados forem simbólicos, o Manticore explorará todas as funções do contrato durante a execução da transação. Será útil ver a explicação da Função de Fallback no artigo Hands on the Ethernaut CTF (opens in a new tab) para entender como a seleção de funções funciona.

Transação nomeada

As funções podem ser executadas pelo nome. Para executar f(uint var) com um valor simbólico, de user_account, e com 0 ether, use:

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
Copiar

Se o value da transação não for especificado, ele será 0 por padrão.

Resumo

• Argumentos de uma transação podem ser concretos ou simbólicos
• Uma transação bruta explorará todas as funções
• A função pode ser chamada pelo seu nome

Espaço de trabalho

m.workspace é o diretório usado como diretório de saída para todos os arquivos gerados:

1print("Os resultados estão em {}".format(m.workspace))
Copiar

Encerrar a exploração

Para parar a exploração, use m.finalize() (opens in a new tab). Nenhuma transação adicional deve ser enviada depois que este método for chamado e o Manticore gerará casos de teste para cada caminho explorado.

Resumo: Executando no Manticore

Juntando todas as etapas anteriores, obtemos:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Os resultados estão em {}".format(m.workspace))
15m.finalize() # para a exploração
Exibir tudo
Copiar

Todo o código acima pode ser encontrado em example_run.py (opens in a new tab)

Obtendo caminhos que lançam exceções

Agora, vamos gerar entradas específicas para os caminhos que levantam uma exceção em f(). O alvo ainda é o seguinte contrato inteligente example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Copiar

Usando informações de estado

Cada caminho executado tem seu estado da cadeia de blocos. Um estado está pronto ou é encerrado, o que significa que ele atinge uma instrução THROW ou REVERT:

• m.ready_states (opens in a new tab): a lista de estados que estão prontos (não executaram um REVERT/INVALID)
• m.killed_states (opens in a new tab): a lista de estados que são encerrados
• m.all_states (opens in a new tab): todos os estados

1for state in m.all_states:
2    # faça algo com o estado
Copiar

Você pode acessar as informações de estado. Por exemplo:

• state.platform.get_balance(account.address): o saldo da conta
• state.platform.transactions: a lista de transações
• state.platform.transactions[-1].return_data: os dados retornados pela última transação

Os dados retornados pela última transação são uma matriz, que pode ser convertida em um valor com ABI.deserialize, por exemplo:

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
Copiar

Como gerar um caso de teste

Use m.generate_testcase(state, name) (opens in a new tab) para gerar um caso de teste:

1m.generate_testcase(state, 'BugFound')
Copiar

Resumo

• Você pode iterar sobre o estado com m.all_states
• state.platform.get_balance(account.address) retorna o saldo da conta
• state.platform.transactions retorna a lista de transações
• transaction.return_data são os dados retornados
• m.generate_testcase(state, name) gera entradas para o estado

Resumo: Obtendo caminhos que lançam exceções

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Verifique se uma execução termina com um REVERT ou INVALID
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Exceção encontrada {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Exibir tudo
Copiar

Todo o código acima pode ser encontrado em example_run.py (opens in a new tab)

Observe que poderíamos ter gerado um script muito mais simples, pois todos os estados retornados por terminated_state têm REVERT ou INVALID em seu resultado: este exemplo teve como objetivo apenas demonstrar como manipular a API.

Adicionando restrições

Veremos como restringir a exploração. Vamos assumir que a documentação de f() afirma que a função nunca é chamada com a == 65, então qualquer bug com a == 65 não é um bug real. O alvo ainda é o seguinte contrato inteligente example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Copiar

Operadores

O módulo Operators (opens in a new tab) facilita a manipulação de restrições, entre outras coisas, ele fornece:

• Operators.AND,
• Operators.OR,
• Operators.UGT (maior que sem sinal),
• Operators.UGE (maior ou igual que sem sinal),
• Operators.ULT (menor que sem sinal),
• Operators.ULE (menor ou igual que sem sinal).

Para importar o módulo, use o seguinte:

1from manticore.core.smtlib import Operators
Copiar

Operators.CONCAT é usado para concatenar uma matriz a um valor. Por exemplo, o return_data de uma transação precisa ser alterado para um valor para ser verificado em relação a outro valor:

1last_return = Operators.CONCAT(256, *last_return)
Copiar

Restrições

Você pode usar restrições globalmente ou para um estado específico.

Restrição global

Use m.constrain(constraint) para adicionar uma restrição global. Por exemplo, você pode chamar um contrato a partir de um endereço simbólico e restringir esse endereço a valores específicos:

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
Copiar

Restrição de estado

Use state.constrain(constraint) (opens in a new tab) para adicionar uma restrição a um estado específico. Pode ser usado para restringir o estado após sua exploração para verificar alguma propriedade nele.

Verificando a restrição

Use solver.check(state.constraints) para saber se uma restrição ainda é viável. Por exemplo, o seguinte irá restringir o symbolic_value a ser diferente de 65 e verificar se o estado ainda é viável:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # o estado é viável
Copiar

Resumo: Adicionando restrições

Adicionando restrição ao código anterior, obtemos:

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Verifique se uma execução termina com um REVERT ou INVALID
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # não consideramos o caminho onde a == 65
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Bug encontrado, os resultados estão em {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'Nenhum bug encontrado')
Exibir tudo
Copiar

Todo o código acima pode ser encontrado em example_run.py (opens in a new tab)

Última atualização da página: 26 de abril de 2024

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+6

Ver colaboradores