Apresentando Scribble by ConsenSys Diligence

NewsDevelopersEnterpriseBlockchain ExplainedEvents and ConferencesPressboletins informativos

Assine a nossa newsletter.

Endereço de email

Nós respeitamos sua privacidade

HomeBlogNews

Apresentando Scribble by ConsenSys Diligence

por ConsenSys 8 de dezembro de 2020 Postado em 8 de dezembro de 2020

Garantir que os contratos inteligentes sejam seguros e livres de bugs nunca foi tão importante. Infelizmente, continua sendo uma tarefa difícil. Embora existam ferramentas úteis para teste automático e verificação formal, garantir a correção de contratos inteligentes continua a ser uma tarefa demorada e desafiadora. Para piorar as coisas, cada ferramenta muitas vezes tem uma curva de aprendizagem íngreme e muitas vezes é incerto se é mesmo a certa para o trabalho.

É por isso que desenvolvemos o Scribble: uma linguagem de verificação e ferramenta de verificação de tempo de execução. Embora inicialmente criado para teste automático de propriedade durante as auditorias, decidimos compartilhar este projeto com a comunidade!

O que é rabisco?

Quando falamos sobre Scribble, estamos falando sobre duas coisas.

Primeiro, Scribble é uma linguagem de especificação para escrever propriedades.

Em segundo lugar, Scribble é uma ferramenta de verificação em tempo de execução que usa a linguagem de especificação Scribble.

NOTA: O Scribble não realiza nenhuma verificação por si só. Isto faz habilite outras ferramentas para testar e verificar propriedades.

Rabisco é uma linguagem

Scribble define uma linguagem específica de domínio para escrever propriedades sobre contratos inteligentes. Nós construímos a linguagem com base na sintaxe de solidez, para torná-la mais fácil de aprender. Esta linguagem de especificação permite que você anote um contrato inteligente de solidez com propriedades.

NOTA: uma propriedade é uma declaração lógica que você espera que seja verdadeira, por exemplo, “Todos os carros são vermelhos”. Em termos de solidez, muitas vezes você terá propriedades como: “Somente o proprietário pode fazer uma alteração em X”. Ou “Função sendToken (), não deve alterar o equilíbrio de éter deste contrato”.

Você pode usar vários tipos de anotação para diferentes tipos de propriedades. Por exemplo, invariantes ou pós-condições.

Este é um exemplo de anotação Rabisco:

Screen Shot 2020 12 08 às 12 06 15 PM

Como você pode ver, as anotações assumem a forma de um comentário embutido colocado acima de uma definição de função. Adicionamos a chamada cláusula if_succeeds, que verifica se uma condição se mantém após a execução da função. Neste caso, verificamos se o resultado da função é sempre diferente de zero.

Leia a documentação do Scribble

Baseamos a linguagem Scribble em conceitos comprovados, como pós-condições, invariantes e lógica temporal. Mas também veremos como podemos apresentar novas ideias para atender melhor aos problemas específicos de domínio dos contratos inteligentes.

Rabisco é uma ferramenta

O Scribble pode pegar um contrato anotado com propriedades e compilá-lo em um novo contrato. Neste novo contrato, Scribble terá adicionado código Solidity que levanta uma afirmação sempre que uma propriedade é violada. Chamamos esse processo de instrumentação.

Adicionar código executável que verifica as propriedades é chamado de verificação de tempo de execução e torna mais fácil trabalhar com as ferramentas existentes sem muitas adaptações. Este é o caso porque a maioria das ferramentas já interpretará o código de solidez e será capaz de pesquisar violações de propriedade imediatamente!

Porque você pode usar técnicas de teste automático existentes (como nosso fuzzer Harvey), você poderá começar a testar depois de escrever apenas uma propriedade. Acreditamos que este seja um benefício significativo; Você se beneficia com o teste automático imediatamente, em vez de gastar muito tempo antecipadamente para obter uma massa crítica de anotações. Algo que geralmente é necessário com abordagens de verificação tradicionais.

Você pode começar a testar e analisar um contrato rapidamente e até mesmo decidir mais tarde se esforçar para verificar um contrato inteligente completamente!

Metas

Auditoria

Estamos usando o Scribble durante as auditorias para formular propriedades. Usando técnicas de análise automática, como difusão e execução simbólica, testaremos e encontraremos automaticamente violações para essas propriedades.

Entre em contato conosco para saber mais sobre fuzzing e testes baseados em propriedades durante as auditorias

Padrão

O Scribble visa trabalhar com diferentes ferramentas e técnicas; não queremos apenas habilitar o teste baseado em propriedade, mas também a verificação formal fácil. O benefício de usar uma única linguagem de especificação universal é que você só se esforça para escrever propriedades uma vez, mas colhe o benefício de usar várias ferramentas.

Adoção

Com o Scribble, esperamos diminuir a barreira ou entrada para testes automáticos e verificação formal. Também queremos reduzir o investimento de tempo necessário para desenvolver contratos inteligentes corretos e seguros, resultando em um ecossistema mais seguro.

Onde você pode conseguir?

Abrimos totalmente o código-fonte do Scribble e agora está disponível em github.com/consensys/scribble.

NOTA: Esta é uma versão beta, os aspectos do idioma serão alterados e você pode encontrar alguns bugs.

Você pode instalar facilmente o Scribble com npm:

Screen Shot 2020 12 08 às 12 06 35 PM Instale o Scribble

Boletim informativo Assine nosso boletim informativo para obter as notícias mais recentes da Ethereum, soluções empresariais, recursos para desenvolvedores e muito mais. Endereço de e-mailConteúdo exclusivoRelatório