Advertência
Este artigo não é uma classificação da eficácia dos analisadores automáticos. Eu os aplico aos meus próprios contratos, intencionalmente sintetizando erros e estudo as reações. Esse estudo não pode ser a base para determinar “melhor ou pior”; para isso, faz sentido realizar um estudo cego em uma grande amostra de contratos, o que, dada a natureza caprichosa desse tipo de software, é extremamente difícil. É bem possível que um pequeno erro no contrato possa desabilitar uma grande parte da lógica do analisador, e um simples sinal heurístico pode adicionar uma quantidade enorme de pontos ao analisador, encontrando um bug generalizado que os concorrentes simplesmente não conseguiram adicionar. Erros na preparação e compilação de contratos também podem desempenhar um papel. Todo o software em questão é bastante jovem e está sendo constantemente desenvolvido, portanto, não tome comentários críticos como problemas irreparáveis.
O objetivo do artigo é fornecer ao leitor uma compreensão de como os métodos de análise de código em diferentes analisadores funcionam e a capacidade de usá-los corretamente, em vez de "fazer uma escolha". Uma escolha razoável é usar várias ferramentas ao mesmo tempo, com foco nas mais adequadas para o contrato analisado.
Configuração e preparação para o lançamento
O Mythril usa vários tipos de análise de uma só vez, eis alguns bons artigos sobre o assunto: o mais importante , isto ou aquilo. Antes de continuar, faz sentido lê-los.
Primeiro, vamos criar nossa própria imagem do Mythril no Docker (não importa o que queremos mudar?):
git clone https://github.com/ConsenSys/mythril-classic.git cd mythril-classic docker build -t myth .
Agora tente executá-lo em nossos contracts/flattened.sol (eu uso o mesmo contrato discutido na introdução ), no qual existem dois contratos principais, Ownable pelo Zeppelin e nosso Booking . Ainda temos um problema com a versão do compilador, eu a corrigi da mesma maneira que no artigo anterior, adicionando linhas ao Dockerfile que substituirá a versão do compilador:
COPY --from=ethereum/solc:0.4.20 /usr/bin/solc /usr/bin
Após reconstruir a imagem, você pode tentar executar a análise de contrato. Imediatamente vamos usar os sinalizadores -v4 e --verbose-report para ver todos os avisos. Vamos lá:
docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ -v4 \ --verbose-report \ -x contracts/flattened.sol
Aqui trabalhamos com um contrato achatado sem dependências. Para analisar um contrato Booking.sol separado e fazer com que o Mythril selecione todas as dependências, você pode usar algo como isto:
docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ --solc-args="--allow-paths /tmp/node_modules/zeppelin-solidity/ zeppelin-solidity=/tmp/node_modules/zeppelin-solidity" \ -v4 \ --verbose-report \ -x contracts/Booking.sol
Prefiro trabalhar com a opção achatada, pois modificaremos muito no código. Mas o Mythril também possui um modo extremamente conveniente - --truffle , que simplesmente --truffle tudo o que a truffle , verificando todo o projeto quanto a vulnerabilidades. Outra característica importante é a capacidade de especificar o nome do contrato a ser analisado por dois pontos; caso contrário, o Mythril analisará todos os contratos que encontrar. Acreditamos que o Ownable do OpenZeppelin é um contrato seguro e só vamos analisar o Booking , portanto a linha final a ser executada é:
docker run -v $(pwd):/tmp -w /tmp myth:latest -x contracts/flattened.sol:Booking -v4 --verbose-report
Iniciar e implantar contrato
Iniciamos o analisador com a linha acima, examinamos a saída e obtemos, entre outras coisas, esta linha:
mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) The analysis was completed successfully. No issues were detected.
Acontece que nosso contrato não foi criado e "corrigido" no emulador. É por isso que recomendo usar o sinalizador -v4 para todos os tipos de análise para ver todas as mensagens e não perder uma única importante. Vamos descobrir o que há de errado. A solução para esse problema prático é bastante importante para entender como usar o Mythril corretamente.
Portanto, estamos lendo sobre o Mythril: It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities . Se você não conhece muito esses termos, recomendo o wiki sobre testes concólicos aqui , mas aqui está uma boa apresentação sobre a verificação de contaminação do x86. Resumindo: Mythril emula a execução de um contrato, corrige as ramificações pelas quais a execução pode ir e tenta alcançar um estado "quebrado" do contrato, classificando várias combinações de parâmetros e tentando contornar todos os caminhos possíveis. Aqui está um exemplo de diagrama de ação do artigo acima:
1. . symbolic-, . 2. , , trace . , , . 3. . 4. trace-. 5. symbolic execution trace, symbolic , , , . 6. , . , . 7. : , , input-, , . input- , .6 . 8. .4
Se você simplificá-lo bastante, o Mythril, tendo encontrado uma ramificação no código, pode entender sob quais conjuntos de variáveis é possível entrar em uma e na outra ramificação. Em cada ramo, o Mythril sabe se leva a assert , transfer , selfdestruct e outros códigos de operação relevantes à segurança. Portanto, o Mythril analisa quais conjuntos de parâmetros e transações podem levar a uma violação de segurança. E a maneira como o Mythril corta ramos que nunca obtêm controle e analisa o fluxo de controle é seu truque principal. Mais detalhes sobre o intestino Mythril e a caminhada nos galhos estão escritos aqui .
Devido à natureza determinística da execução inteligente de contratos, a mesma sequência de instruções sempre leva estritamente a um conjunto de alterações de estado, independentemente da plataforma, arquitetura ou ambiente. Além disso, as funções nos contratos inteligentes são bastante curtas e os recursos são extremamente limitados; portanto, analisadores como o Mythril, combinando execução simbólica e nativa, podem funcionar de maneira extremamente eficiente para contratos inteligentes.
No processo, o Mythril usa o conceito de "estado" - este é o código do contrato, seu ambiente, um ponteiro para o comando atual, armazenamento do contrato e o estado da pilha. Aqui está a documentação:
The machine state μ is defined as the tuple (g, pc, m, i, s) which are the gas available, the program counter pc ∈ P256, the memory contents, the active number of words in memory (counting continuously from position 0), and the stack contents. The memory contents μm are a series of zeroes of size 256.
O gráfico de transição entre estados é o principal objeto de estudo. No caso de uma inicialização bem-sucedida da análise, as informações sobre este gráfico são exibidas no log de análise. Além disso, o Mythril pode criar esse gráfico de forma legível por humanos, usando a opção --graph .
Agora, entendendo mais ou menos o que o Mythril fará, continuaremos a entender por que o contrato não é analisado e de onde veio [WARNING]: No contract was created during the execution of contract creation . Para começar, torci as --create-timeout e --max-depth (conforme recomendado) e, não obtendo o resultado, pensei que o construtor fosse o culpado - algo nele não funcionava. Aqui está o código dele:
function Booking( string _description, string _fileUrl, bytes32 _fileHash, uint256 _price, uint256 _cancellationFee, uint256 _rentDateStart, uint256 _rentDateEnd, uint256 _noCancelPeriod, uint256 _acceptObjectPeriod ) public payable { require(_price > 0); require(_price > _cancellationFee); require(_rentDateStart > getCurrentTime()); require(_rentDateEnd > _rentDateStart); require(_rentDateStart+_acceptObjectPeriod < _rentDateEnd); require(_rentDateStart > _noCancelPeriod); m_description = _description; m_fileUrl = _fileUrl; m_fileHash = _fileHash; m_price = _price; m_cancellationFee = _cancellationFee; m_rentDateStart = _rentDateStart; m_rentDateEnd = _rentDateEnd; m_noCancelPeriod = _noCancelPeriod; m_acceptObjectPeriod = _acceptObjectPeriod; }
Lembre-se do algoritmo de ação do Mythril. Para executar o rastreio, é necessário chamar o construtor do contrato, porque toda a execução subsequente dependerá de quais parâmetros o construtor foi chamado. Por exemplo, se você chamar o construtor com _price == 0 , o construtor lançará uma exceção ao require(_price > 0) . Mesmo que o Mythril itere sobre os muitos valores de _price , o construtor ainda será interrompido se, por exemplo, _price <= _cancellationFee . Neste contrato, há uma dúzia de parâmetros associados a restrições estritas, e o Mythril, é claro, não consegue adivinhar as combinações válidas de parâmetros. Ele tenta ir para o próximo ramo de execução, classificando os parâmetros do construtor, mas ele praticamente não tem chance de adivinhar - há muitas combinações de parâmetros. Portanto, o cálculo do contrato não dá certo - todas as formas require(...) de algum tipo de require(...) , e obtemos o problema acima.
Agora, temos duas maneiras: a primeira é desativar todos os require no construtor, comentando-os. O Mythril poderá chamar o construtor com qualquer conjunto de parâmetros e tudo funcionará. Mas isso significa que, examinando um contrato com esses parâmetros, o Mythril encontrará erros possíveis com valores incorretos passados ao construtor. Simplificando, se o Mythril encontrar um erro que surgir, se o criador do contrato especificar _cancellationFee um bilhão de vezes o preço do aluguel do _mprice , não haverá utilidade nesse erro - esse contrato nunca será bloqueado e os recursos para encontrar erros serão gastos. Implicamos que o contrato ainda está preso a parâmetros mais ou menos consistentes; portanto, para análises posteriores, faz sentido especificar parâmetros construtores mais realistas para que o Mythril não procure por erros que nunca ocorrerão se o contrato for fechado corretamente.
Passei muitas horas tentando entender exatamente onde a implantação é interrompida, incluindo e desativando várias partes do construtor. Além dos meus problemas, o construtor usa getCurrentTime() , que retorna a hora atual, e não está claro como essa chamada lida com o Mythril. Não vou descrever essas aventuras aqui, porque provavelmente com o uso regular, essas sutilezas serão conhecidas pelo auditor. Portanto, escolhi a segunda maneira: limitar os dados de entrada e simplesmente remover todos os parâmetros do construtor, mesmo getCurrentTime() , simplesmente codificou os parâmetros necessários diretamente no construtor (idealmente, esses parâmetros devem ser obtidos do cliente):
function Booking( ) public payable { m_description = "My very long booking text about hotel and beautiful sea view!"; m_fileUrl = "https://ether-airbnb.bam/some-url/"; m_fileHash = 0x1628f3170cc16d40aad2e8fa1ab084f542fcb12e75ce1add62891dd75ba1ffd7; m_price = 1000000000000000000; // 1 ETH m_cancellationFee = 100000000000000000; // 0.1 ETH m_rentDateStart = 1550664800 + 3600 * 24; // current time + 1 day m_rentDateEnd = 1550664800 + 3600 * 24 * 4; // current time + 4 days m_acceptObjectPeriod = 3600 * 8; // 8 hours m_noCancelPeriod = 3600 * 24; // 1 day require(m_price > 0); require(m_price > m_cancellationFee); require(m_rentDateStart > 1550664800); require(m_rentDateEnd > m_rentDateStart); require((m_rentDateStart + m_acceptObjectPeriod) < m_rentDateEnd); require(m_rentDateStart > m_noCancelPeriod); }
Além disso, para que tudo comece, você também deve definir o parâmetro max-depth . Funcionou para mim com esse construtor com --max-depth=34 na instância do AWS t2.medium. Ao mesmo tempo, no meu laptop, que é mais poderoso, tudo começa sem nenhuma max-depth . A julgar pelo uso desse parâmetro , é necessário construir ramificações para análise, e seu valor padrão é infinito ( código ). Portanto, gire este parâmetro com rotação, mas garanta que o contrato desejado seja analisado. Você pode entender isso por mensagens como:
mythril.laser.ethereum.svm [INFO]: 248 nodes, 247 edges, 2510 total states mythril.laser.ethereum.svm [INFO]: Achieved 59.86% coverage for code: .............
A primeira linha descreve apenas o gráfico que será analisado, leia o resto das linhas você mesmo. Recursos computacionais sérios são necessários para analisar as várias ramificações que podem ser executadas; portanto, ao analisar contratos grandes, você terá que esperar até em um computador rápido.
Procure por erros
Agora vamos procurar erros e adicionar os nossos. O Mythril procura ramificações nas quais a transmissão, a autodestruição, a afirmação e outras ações importantes do ponto de vista da segurança ocorrem. Se uma das instruções acima for encontrada em algum lugar do código do contrato, o Mythril estuda as maneiras pelas quais é possível chegar a essa agência e, além disso, exibe a sequência de transações que levam a essa agência!
Primeiro, vamos ver o que o Mythril emitiu para o contrato de Booking longa duração. Primeiro aviso:
==== Dependence on predictable environment variable ==== SWC ID: 116 Severity: Low Contract: Booking Function name: fallback PC address: 566 Estimated Gas Usage: 17908 - 61696 Sending of Ether depends on a predictable variable. The contract sends Ether depending on the values of the following variables: - block.timestamp Note that the values of variables like coinbase, gaslimit, block number and timestamp are predictable and/or can be manipulated by a malicious miner. Don't use them for random number generation or to make critical decisions. -------------------- In file: contracts/flattened.sol:142 msg.sender.transfer(msg.value-m_price)
e surge porque
require(m_rentDateStart > getCurrentTime());
na função de fallback.
Observe que o Mythril percebeu que getCurrentTime() oculto em getCurrentTime() . Apesar do significado do contrato não ser um erro, o fato de o Mythril associar block.timestamp à transmissão é excelente! Nesse caso, o programador deve entender que a decisão é tomada com base no valor que o mineiro pode controlar. E, se no futuro surgir um leilão ou outro leilão de um serviço neste local do contrato, é preciso levar em consideração a possibilidade de ataques anteriores.
Vamos ver se o Mythril vê uma dependência do block.timestamp se escondermos a variável em uma chamada aninhada como esta:
function getCurrentTime() public view returns (uint256) { - return now; + return getCurrentTimeInner(); } + function getCurrentTimeInner() internal returns (uint256) { + return now; + }
E sim! O Mythril continua vendo a conexão entre block.timestamp e a transferência da transmissão, isso é extremamente importante para o auditor. A conexão entre a variável controlada pelo invasor e a decisão tomada após várias alterações no estado do contrato pode ser muito mascarada pela lógica, e o Mythril permite que você rastreie. Embora não valha a pena confiar no fato de que todas as conexões possíveis entre todas as variáveis possíveis serão getCurrentTime() para você: se você continuar zombando da função getCurrentTime() e fizer uma profundidade de aninhamento tripla, o aviso desaparecerá. Cada chamada de função para o Mythril requer a criação de novas ramificações de estado, portanto, analisar níveis muito profundos de aninhamento exigirá recursos enormes.
É claro que há uma chance bastante séria de eu simplesmente usar incorretamente os parâmetros de análise ou o ponto de corte ocorrer em algum lugar nas profundezas do analisador. Como eu disse, o produto está em desenvolvimento ativo, no momento em que escrevo, vejo confirmações no repositório com a menção de max-depth ; portanto, não leve a sério os problemas atuais, já encontramos evidências suficientes de que o Mythril pode efetivamente procurar conexões implícitas entre variáveis.
Primeiro, adicione ao contrato uma função que transmita a transmissão a qualquer pessoa, mas somente após o cliente enviar a transmissão ao contrato. State.PAID que qualquer pessoa pegasse 1/5 do éter, mas somente quando o contrato estiver no estado State.PAID (ou seja, somente depois que o cliente pagou o número alugado com o éter). Aqui está a função:
function collectTaxes() external onlyState(State.PAID) { msg.sender.transfer(address(this).balance / 5); }
Mythril encontrou o problema:
==== Unprotected Ether Withdrawal ==== SWC ID: 105 Severity: High Contract: Booking Function name: collectTaxes() PC address: 2492 Estimated Gas Usage: 2135 - 2746 Anyone can withdraw ETH from the contract account. Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent a equivalent amount of ETH to it. This is likely to be a vulnerability. -------------------- In file: contracts/flattened.sol:149 msg.sender.transfer(address(this).balance / 5) -------------------- -------------------- Transaction Sequence: { "2": { "calldata": "0x", "call_value": "0xde0b6b3a7640000", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" }, "3": { "calldata": "0x01b613a5", "call_value": "0x0", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" } }
Ótimo, ou seja, Mythril chegou a realizar duas transações, que levam ao fato de que você pode retirar o éter do contrato. Agora altere o requisito State.RENT para State.RENT , desta forma:
- function collectTaxes() external onlyState(State.PAID){ + function collectTaxes() external onlyState(State.RENT) {
Agora collectTaxes() pode ser chamado apenas quando o contrato estiver no estado State.RENT e, neste momento, não há nada na balança, porque o contrato já enviou a transmissão inteira ao proprietário. E o importante aqui é que o Mythril desta vez NÃO gera o erro ==== Unprotected Ether Withdrawal ==== ! Sob a condição onlyState(State.RENT) , o analisador não chegou à ramificação de código que envia éter do contrato com um saldo diferente de zero. O Mythril passou por opções diferentes para os parâmetros, mas você pode entrar no State.RENT apenas enviando toda a transmissão ao locador. Portanto, é impossível chegar a esse ramo do código com um saldo diferente de zero, e o Mythril absolutamente não incomoda o auditor!
Da mesma forma, o Mythril encontrará selfdestruct e assert , mostrando ao auditor quais ações podem levar à destruição do contrato ou à quebra de uma função importante. Não darei esses exemplos, apenas tentarei criar uma função semelhante à acima, apenas chamando selfdestruct - selfdestruct e distorcer sua lógica.
Além disso, não esqueça que uma das partes do Mythril é a execução simbólica, e essa abordagem, por si só, sem emular a execução, pode determinar muitas vulnerabilidades. Por exemplo, qualquer uso de "+", "-" e outros operadores aritméticos pode ser considerado uma vulnerabilidade de "Estouro de número inteiro" se um dos operandos for de alguma forma controlado pelo invasor. Mas repito novamente, o recurso mais poderoso do Mythril é a combinação de execução simbólica e nativa e a determinação de valores de parâmetros que levam à ramificação lógica.
Conclusão
Obviamente, para mostrar toda a gama de possíveis problemas que o Mythril é capaz de detectar, serão necessários não apenas um, mas vários artigos. Para todo o resto, ele sabe fazer tudo isso em um blockchain real, encontrando os contratos e vulnerabilidades necessários por assinaturas, criando belos gráficos de chamadas, formatando relatórios. O Mythril também permite que você escreva seus próprios scripts de teste, fornecendo uma interface baseada em python ao contrato e testando funções individuais, corrigindo valores de parâmetros ou até implementando sua própria estratégia para trabalhar com código desmontado com um grau de flexibilidade arbitrário.
O Mythril ainda é um software bastante jovem, esse não é o IDA Pro e há muito pouca documentação, exceto alguns artigos. O valor de muitos parâmetros só pode ser lido no código Mythril, começando com cli.py. Espero que uma descrição completa e aprofundada da operação de cada parâmetro apareça na documentação.
Além disso, quando o contrato é mais ou menos grande, a saída de vários erros ocupa muito espaço, mas eu gostaria de receber informações compactadas sobre o erro encontrado, porque ao trabalhar com o Mythril, você deve definitivamente observar o caminho da análise, ver quais contratos foram testados da melhor maneira possível e poder desativar à força erros específicos que o auditor considera falso-positivos.
Mas, em geral, o Mythril é uma ferramenta excelente e extremamente poderosa para analisar contratos inteligentes e, no momento, deve estar no arsenal de qualquer auditor. Ele permite que você preste pelo menos atenção a partes críticas do código e detecte relacionamentos ocultos entre variáveis.
Para resumir, as recomendações para o uso do Mythril são:
- Limitar as condições iniciais do contrato em estudo Se, durante a análise, o Mythril gastar muitos recursos em ramificações que nunca serão implementadas na prática, ele perderá a capacidade de encontrar erros realmente importantes, portanto, você deve sempre tentar diminuir a área de ramificações em potencial.
- Verifique se a análise do contrato foi iniciada, não perca mensagens como
mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) , caso contrário, você pode considerar erroneamente que não há bugs. - Você pode desabilitar arbitrariamente ramificações no código do contrato, dando ao Mythril menos variação na escolha de ramificações e economizando recursos. Tente fazer sem restrições
max-depth , para não "cortar" a análise, mas tome cuidado para não mascarar o erro. - Preste atenção a cada aviso, mesmo comentários leves às vezes valem a pena adicionar pelo menos um comentário ao código do contrato, facilitando para outros desenvolvedores.
No próximo artigo, trataremos do analisador Manticore, mas aqui está o índice dos artigos prontos ou planejados para a escrita:
Parte 1. Introdução. Compilação, nivelamento, versões do Solidity
Parte 2. Slither
Parte 3. Mythril (este artigo)
Parte 4. Manticore (durante a escrita)
Parte 5. Equidna (durante a escrita)