Em um esforço de verificação formal, Ethereum busca a certeza do contrato inteligente

Há uma nova palavra da moda em blockchain chegando a tempo para o outono: verificação formal.

A frase (usada para descrever a aplicação da matemática para verificar programas de software) tem sido evocada até agora de forma esparsana imprensa. Mas se a conversa na cúpula de desenvolvedores da Ethereum na semana passada serviu de indicação, ela pode desempenhar um papel cada vez maior, dadas as questões de segurança que ainda cercam contratos inteligentes e blockchains de forma mais ampla.

Como evidenciado por várias palestras dedicadas ao assunto na Devcon2, a ideia de que novas garantias poderiam ser dadas aos codificadores de Ethereum está sendo amplamente adotada por sua comunidade de desenvolvimento. O conceito já está sendo proposto como uma forma de inspirar confiança em tudo, desde o próprio protocolo Ethereum até seu blockchain experimental de proof-of-stake.

Que isso tenha acontecido talvez não seja nenhuma surpresa, dado o colapso repentino do The DAO neste verão, até o momento o maior contrato inteligente já lançado na plataforma de desenvolvimento de aplicativos descentralizados.

Mas enquantoverificação formal pode parecer complexo, mas o conceito pode ser resumido sucintamente quando aplicado ao Ethereum – os codificadores atualmente usam uma linguagem amplamente nova (Solidity) para escrever contratos inteligentes, escrevendo comandos que são então traduzidos em bytecode para uso pela máquina virtual Ethereum (EVM) e disseminados para os nós da rede para execução.

Em certo sentido, a verificação formal pode ser vista como uma forma mais objetiva de garantir que, quando diferentes partes componentes da rede recebem essas instruções, elas as executam conforme pretendido em nome dos usuários.

Grant Passmore, cofundador da Aesthetic Integration, é um empreendedor que vê uma oportunidade em ajudar nesse esforço, usando o Devcon2 para lançar o Imandra Contracts, uma plataforma de verificação formal para contratos inteligentes de blockchain.

No evento, ele evocou a ideia de que o Ethereum poderia servir como um "paraíso" para verificação formal (um ponto de contato amplamente citado em conversas), dados os objetivos de sua comunidade e as responsabilidades significativas que ela deseja confiar ao código.

Passmore disse ao CoinDesk:

"A comunidade Ethereum está em uma posição única, onde depois do DAO, entendemos que engenharia rigorosa é necessária. Você T pode abordar a escrita de um contrato inteligente como um aplicativo da web."

Em outros lugares, palestrantes como Philip Daian, da Cornell, falaram sobre o interesse na metodologia de forma mais ampla, dizendo ao público que acredita que a verificação formal pode ajudar o Ethereum a resolver problemas importantes.

"Será uma parte crítica do quadro geral. Estou ansioso para usar o Ethereum para definir o padrão e mostrar às pessoas como isso é feito", disse ele.

Rodinhas de treinamento

Dada a ênfase recente que as empresas financeiras têm colocado na exploraçãolinguagens de contratação inteligente, talvez tenha sido o conceito de aplicação de verificação formal ao Solidity o tópico de discussão mais frequente.

Desenvolvido para a plataforma Ethereum , o Solidity enfrentou críticas por ser amplamente não testado e difícil de escrever, principalmente por ser tão novo. Tais problemas foram, sem dúvida, amplificados devido a problemascom o compilador da linguagem, a falta de bibliotecas públicas e o colapso do DAO, que foi examinado por membros notáveis de sua comunidade de desenvolvimento.

Diante disso, Christian Reitweissner, criador do Solidity, reconheceu que há um esforço para implementar a verificação formal para que os erros possam ser detectados de forma mais eficaz pelos codificadores do Ethereum .

Reitweissner disse à CoinDesk que os desenvolvedores de contratos inteligentes poderiam um dia usar ferramentas formais de verificação para, por exemplo, determinar se há erros imprevistos em seu trabalho. Ele indicou que tal ferramenta poderia ser usada para determinar se, ao adicionar dois saldos, o resultado se estendeu mais do que o campo alocado pelo compilador.

"Isso poderia acontecer e a ferramenta de verificação formal [iria] detectar isso automaticamente. Você pode detectar isso logo no início e reagir a isso dentro do contrato inteligente", explicou ele.

Reitweissner disse que a equipe Solidity já estava explorando como aplicar a verificação formal ao seu trabalho. Já emoutubro passado, havia protótipos de como um kit de ferramentas chamado Why3 poderia ser usado para essa finalidade, embora tais ofertas ainda não estejam disponíveis para a linguagem completa.

Campo de provas

O fato de o Ethereum poder ser usado para testar como a verificação formal pode ser aplicada às Finanças de forma mais ampla também foi um tópico muito discutido durante a conferência.

Passmore, por exemplo, disse que a Aesthetic Integration vem trabalhando na aplicação da verificação formal no trabalho com instituições financeiras desde 2014 e que, até agora, os clientes têm procurado usá-la em áreas limitadas, como dark pools, onde os traders exigem certeza sobre a imparcialidade.

Em contratos inteligentes, Passmore sugeriu que vê o Ethereum como uma comunidade que pode impulsionar ainda mais a aceitação.

"Quando começamos a trabalhar com muitos dos nossos clientes bancários, ouvimos que eles estavam interessados no espaço, mas estavam preocupados com a correção dos contratos inteligentes", disse ele.

O avanço da verificação formal também atraiu Yoichi Hirai por razões semelhantes. Um engenheiro de verificação formal agora empregado pela Ethereum Foundation, seu interesse no conceito começou como pesquisador e em seu emprego anterior na líder de segurança cibernética FireEye.

Em uma palestra na conferência, Hirai falou sobre sua frustração ao aplicar a verificação formal em ambientes onde ele não tinha acesso ao código-fonte ou as tarefas eram talvez muito amplas para promover o conceito.

"Encontrei o Ethereum, vi o EVM, o artigo amarelo, a especificação, tinha apenas 32 páginas e pensei que poderia realmente traduzi-lo e escrever provas sobre contratos inteligentes", disse ele.

O Ethereum, por outro lado, oferece o que ele chamou de "especificação menor" e um "problema solucionável" para engenheiros determinarem a melhor forma de traduzir o Solidity em bytecode.

"Acredito que muitos outros pesquisadores de verificação formal estão chegando", disse ele.

Nenhuma solução mágica

No entanto, apesar do entusiasmo, há medidas sendo tomadas para alertar sobre o quanto a verificação formal pode alcançar. O desenvolvedor Alex Beregszaszi, que está trabalhando em atualizações para o EVM, falou sobre a necessidade de um conjunto de soluções para ajudar os desenvolvedores a garantir que o código do contrato inteligente esteja funcionando conforme o esperado.

Passmore também observou que é difícil dizer se seu novo sistema poderia ter detectado problemas com o DAO, já que ferramentas formais de verificação ainda exigem intervenção Human .

"Você pode codificar problemas que aconteceram com o DAO e verificar se T há problemas com eles, mas precisa saber o que procurar", explicou ele.

As limitações foram reconhecidas por Reitweissner e Passmore, ambos alertando os desenvolvedores para não pensarem na verificação formal como uma “bala de prata”.

Reitweissner, no entanto, vê a metodologia como ONE que irá progredir à medida que for mais amplamente utilizada, com os desenvolvedores a tornarem-se lentamente melhores na identificação de problemas e no desenvolvimento de repositórios onde o conhecimento de problemas comuns pode ser tornado acessível.

Dessa forma, Passmore acredita que a comunidade Ethereum está tendo sucesso em "evangelizar" o conceito, algo que ele acredita que acabará por promover a pesquisa sobre blockchain.

Passmore concluiu:

"Embora isso seja algo a que muitos nunca foram expostos, a verificação formal é o que precisamos. É uma curva de aprendizado, mas deve ser adotada, e isso é emocionante."

Imagens via Pete Rizzo para CoinDesk