Um guia para ferramentas de segurança de contratos inteligentes

Vamos usar três técnicas distintas de teste e análise de programas:

• Análise estática com o Slither. Todos os caminhos do programa são aproximados e analisados ao mesmo tempo, por meio de diferentes apresentações do programa (por exemplo, grafo de fluxo de controle).
• Fuzzing com o Echidna. O código é executado com uma geração pseudoaleatória de transações. O fuzzer tentará encontrar uma sequência de transações que viole uma determinada propriedade.
• Execução simbólica com o Manticore. Uma técnica de verificação formal que traduz cada caminho de execução em uma fórmula matemática, sobre a qual restrições podem ser verificadas.

Cada técnica tem vantagens e armadilhas, e será útil em casos específicos:

* se todos os caminhos forem explorados sem tempo limite (timeout)

O Slither analisa contratos em segundos, no entanto, a análise estática pode levar a falsos alarmes e será menos adequada para verificações complexas (por exemplo, verificações aritméticas). Execute o Slither por meio da API para acesso rápido a detectores integrados ou por meio da API para verificações definidas pelo usuário.

O Echidna precisa ser executado por vários minutos e produzirá apenas verdadeiros positivos. O Echidna verifica propriedades de segurança fornecidas pelo usuário, escritas em Solidity. Ele pode não detectar bugs, pois é baseado em exploração aleatória.

O Manticore realiza a análise mais "pesada". Assim como o Echidna, o Manticore verifica propriedades fornecidas pelo usuário. Ele precisará de mais tempo para ser executado, mas pode provar a validade de uma propriedade e não relatará falsos alarmes.

Fluxo de trabalho sugerido

Comece com os detectores integrados do Slither para garantir que nenhum bug simples esteja presente agora ou seja introduzido posteriormente. Use o Slither para verificar propriedades relacionadas à herança, dependências de variáveis e problemas estruturais. À medida que a base de código cresce, use o Echidna para testar propriedades mais complexas da máquina de estado. Volte ao Slither para desenvolver verificações personalizadas para proteções indisponíveis no Solidity, como proteção contra a substituição (override) de uma função. Por fim, use o Manticore para realizar a verificação direcionada de propriedades críticas de segurança, por exemplo, operações aritméticas.

• Use a CLI do Slither para detectar problemas comuns
• Use o Echidna para testar propriedades de segurança de alto nível do seu contrato
• Use o Slither para escrever verificações estáticas personalizadas
• Use o Manticore quando quiser uma garantia aprofundada de propriedades críticas de segurança

Uma observação sobre testes unitários. Testes unitários são necessários para construir software de alta qualidade. No entanto, essas técnicas não são as mais adequadas para encontrar falhas de segurança. Eles são normalmente usados para testar comportamentos positivos do código (ou seja, o código funciona conforme o esperado no contexto normal), enquanto as falhas de segurança tendem a residir em casos extremos que os desenvolvedores não consideraram. Em nosso estudo de dezenas de revisões de segurança de contratos inteligentes, a cobertura de testes unitários não teve efeito sobre o número ou a gravidade das falhas de segurança (opens in a new tab) que encontramos no código de nossos clientes.

Determinando propriedades de segurança

Para testar e verificar seu código de forma eficaz, você deve identificar as áreas que precisam de atenção. Como os recursos gastos em segurança são limitados, definir o escopo das partes fracas ou de alto valor da sua base de código é importante para otimizar seu esforço. A modelagem de ameaças pode ajudar. Considere revisar:

• Avaliações Rápidas de Risco (opens in a new tab) (nossa abordagem preferida quando o tempo é curto)
• Guia para Modelagem de Ameaças de Sistemas Centrados em Dados (opens in a new tab) (também conhecido como NIST 800-154)
• Modelagem de ameaças de Shostack (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• Uso de asserções (opens in a new tab)

Componentes

Saber o que você deseja verificar também ajudará a selecionar a ferramenta certa.

As áreas amplas que são frequentemente relevantes para contratos inteligentes incluem:

• Máquina de estado. A maioria dos contratos pode ser representada como uma máquina de estado. Considere verificar se (1) nenhum estado inválido pode ser alcançado, (2) se um estado for válido, ele pode ser alcançado e (3) nenhum estado prende o contrato.

  • O Echidna e o Manticore são as ferramentas preferidas para testar especificações de máquina de estado.

• Controles de acesso. Se o seu sistema tiver usuários privilegiados (por exemplo, um proprietário, controladores, ...), você deve garantir que (1) cada usuário possa executar apenas as ações autorizadas e (2) nenhum usuário possa bloquear ações de um usuário com mais privilégios.

  • O Slither, o Echidna e o Manticore podem verificar se há controles de acesso corretos. Por exemplo, o Slither pode verificar se apenas funções na lista de permissões não possuem o modificador onlyOwner. O Echidna e o Manticore são úteis para controles de acesso mais complexos, como uma permissão concedida apenas se o contrato atingir um determinado estado.

• Operações aritméticas. Verificar a solidez das operações aritméticas é fundamental. Usar SafeMath em todos os lugares é um bom passo para evitar overflow/underflow, no entanto, você ainda deve considerar outras falhas aritméticas, incluindo problemas de arredondamento e falhas que prendem o contrato.

  • O Manticore é a melhor escolha aqui. O Echidna pode ser usado se a aritmética estiver fora do escopo do solucionador SMT.

• Correção de herança. Os contratos em Solidity dependem fortemente de herança múltipla. Erros como uma função de sombreamento (shadowing) sem uma chamada super e ordem de linearização c3 mal interpretada podem ser facilmente introduzidos.

  • O Slither é a ferramenta para garantir a detecção desses problemas.

• Interações externas. Os contratos interagem entre si, e alguns contratos externos não devem ser confiáveis. Por exemplo, se o seu contrato depende de oráculos externos, ele permanecerá seguro se metade dos oráculos disponíveis for comprometida?

  • O Manticore e o Echidna são a melhor escolha para testar interações externas com seus contratos. O Manticore possui um mecanismo integrado para criar stubs de contratos externos.

• Conformidade com padrões. Os padrões do Ethereum (por exemplo, ERC-20) têm um histórico de falhas em seu design. Esteja ciente das limitações do padrão no qual você está construindo.

  • O Slither, o Echidna e o Manticore ajudarão você a detectar desvios de um determinado padrão.

Folha de dicas para seleção de ferramentas

Outras áreas precisarão ser verificadas dependendo de seus objetivos, mas essas áreas de foco mais amplas são um bom começo para qualquer sistema de contratos inteligentes.

Nossas auditorias públicas contêm exemplos de propriedades verificadas ou testadas. Considere ler as seções Automated Testing and Verification dos seguintes relatórios para revisar propriedades de segurança do mundo real:

• 0x (opens in a new tab)
• Balancer (opens in a new tab)