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 pelo pip ou usando o docker.

Manticore através do Docker

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

O último comando roda a 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 através do docker

Dentro do docker, execute:

solc-select 0.5.11
cd /home/trufflecon/

Manticore através do 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 uma Nutshell

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 baseia-se na descoberta de "caminhos do programa", representados como fórmulas matemáticas chamadas de predicados de caminho. Conceitualmente, esta técnica opera em predicados de caminho em dois passos:

1. Eles são construídos usando restrições na entrada de dados do programa.
2. Eles são usados para gerar entradas no 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 identificados do programa podem ser acionados durante a execução concreta. Por exemplo, se a análise encontrar um integer overflow, é certo que será reproduzível.

Exemplo de Predicado do Caminho

Para se ter uma idéia 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, uma DSE construirá dois caminhos diferentes atribuídos:

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

Cada caminho atribuido é uma fórmula matemática que pode ser dada a uma chamada SMT solver(opens in a new tab), que tentará resolver a equação. Para o Caminho 1, o solver dirá que o caminho pode ser explorado com a = 65. Para o Caminho 2, o solver pode dar para a qualquer valor diferente de 65, por exemplo, a = 0.

Verificando propriedades

A Manticore permite um controle total sobre toda a execução de cada caminho. Como resultado, permite que você adicione restrições arbitrárias a quase qualquer coisa. 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; // no overflow protection
3  return c;
4}
 Copiar

Aqui há apenas um caminho para explorar na função:

• Caminho 1: c = a + b

Usando o Manticore, você pode verificar se há overflow, e adicionar restrições à previsão do caminho:

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

Se é possível encontrar uma avaliação de um e b para a qual o caminho predicado acima é viável, significa que encontrou um transbordamento ("overflow"). Por exemplo, o solver pode gerar a entrada a = 10 , b = MAXUINT256.

Se você considerar uma versão fixa:

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 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 que em safe_add, c irá sempre aumentar.

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

Executando sob Manticore

Veremos como explorar um contrato inteligente com a API Manticore. O alvo é o seguinte contrato inteligente exemplo.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

Executar uma exploração independente

Você pode executar a Manticore diretamente no contrato inteligente pelo seguinte comando (projeto pode ser um Arquivo Solidity, ou um diretório de projeto):

$ manticore project

Você obterá 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, Manticore explorará o contrato com novas transações simbólicas até que não explore novos caminhos do contrato. Manticore não executa novas transações após uma falha (por exemplo: após um reversão).

Manticore irá gerar as informações em um diretório mcore_*. Entre outros, você encontrará nesse diretório:

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

Aqui, Manticore encontrou 7 casos de teste, que correspondem à (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, 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 (ele desativa detectores de bugs, cálculo de gas, ...)

Manipule um contrato inteligente através da API

Esta seção descreve detalhes sobre como manipular um contrato inteligente através da API Manticore Python. Você pode criar um novo arquivo com a extensão python *. y e escreva o código necessário adicionando os comandos da API (básicos dos quais serão descritos abaixo) neste arquivo e então execute-o com o comando $ python3 *. a. Também você pode executar os comandos abaixo diretamente no console python, para executar o console use o comando $ python3.

Criando Contas

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

1from manticore.ethereum import ManticoreEVM
 Copiar

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

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

Um contrato de 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 contratos com m.create_account(opens in a new tab) and m.solidity_create_contract(opens in a new tab).

Executando transações

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 pode ser concreto ou simbólico:

• m.make_symbollic_value(opens in a new tab) cria um valor simbólico.
• m.make_symbollic_value(opens in a new tab) cria um valor simbólico "byte array".

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, Manticore irá explorar todas as funções do contrato durante a execução da transação. Será útil ver a explicação de Função de Fallback nas Mãos do CTF Ethernaut(opens in a new tab), artigo para entender como a seleção de função funciona.

Transação nomeada

Funções podem ser executadas através de seu nome. Para executar f(uint var) com um valor simbólico, do 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 valor da transação não for especificado, ela é 0 por padrão.

Resumo

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

Espaço de trabalho

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

1print("Results are in {}".format(m.workspace))
 Copiar

Terminar a Exploração

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

Resumo: Executando sob Manticore

Juntando todos os passos 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("Results are in {}".format(m.workspace))
15m.finalize() # stop the exploration
Exibir tudo
 Copiar

Todo o código acima você pode encontrar no exemple_run.py(opens in a new tab)

Obtendo caminhos

Agora vamos gerar entradas específicas para os caminhos levantando uma exceção em f(). O alvo é ainda o seguinte contrato inteligente exemplo.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 do estado

Cada caminho executado tem seu estado de blockchain. Um estado ou está pronto ou é morto, o que significa que atinge um caminho de 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 estão mortos
• m.all_states(opens in a new tab): todos os estados

1for state in m.all_statees:
2    # faz algo com estado
 Copiar

Você pode acessar 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 um array, que pode ser convertido para um valor com ABI.deserialize, por exemplo:

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

Como gerar caixa de teste

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

1m.generate_testcase(estado, '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
• Transtion.return_data são os dados retornados
• m.generate_testcase(state, name) gera entradas para o estado

Resumo: Obtendo o caminho de lançamento

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## Verificando se a execução termina com um REVERT ou INVALID
15for state in m.terminated_states:
16    last_tx = state.platform.transactions[-1]
17    if last_tx.result in ['REVERT', 'INVALID']:
18        print('Throw found {}'.format(m.workspace))
19        m.generate_testcase(state, 'ThrowFound')
Exibir tudo
 Copiar

Todo o código acima você pode encontrar no exemple_run.py(opens in a new tab)

Note que poderíamos ter gerado um script muito mais simples, como todos os estados retornados por terminated_state REVERT ou INVALID no seu resultado: este exemplo foi destinado apenas para demonstrar como manipular a API.

Adicionar Restrições

Veremos como restringir a exploração. Vamos fazer a suposição de que a documentação de f() que afirma que a função nunca é chamada com a == 65, então qualquer erro com a == 65 não é um bug de verdade. O alvo é o seguinte contrato inteligente exemplo.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 Operadores(opens in a new tab) facilita a manipulação de restrições, entre outras que fornece:

• Operadores.AND,
• Operadores.OR,
• Operators.UGT (não assinado maior que),
• Operators.UGE (não assinado maior ou igual a),
• Operators.UGT (não assinado menor que),
• Operators.ULE (menor que ou igual a).

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 a ser verificado contra 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 um constraint ("restrição") global. Por exemplo, você pode chamar um contrato de um endereço simbólico e restringir este endereço para serem 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 o estado de . onstrain(restrição)(opens in a new tab) para adicionar uma restrição a um estado específico. Ele pode ser usado para restringir o estado após sua exploração para verificar alguma propriedade nele.

Verificando a constraint ("restrição")

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

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

Resumo: Adicionando constraints ("restrições")

Adicionando constraints ("restrições") 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## Verificar se a execução termina com um REVERT ou INVALID
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # we do not consider the path were a == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug found, results are in {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No bug found')
Exibir tudo
 Copiar

Todo o código acima você pode encontrar no exemple_run.py(opens in a new tab)