KWasm: uma nova semântica executável para a blockchain

Recentemente, a Runtime Verification, Inc. recebeu uma generosa bolsa da dlab para ajudar a financiar nossos esforços para escrever uma semântica para o WebAssembly, em antecipação ao seu uso como uma linguagem de programação du jour em vários projetos de blockchain. O nome deste projeto é KWasm. Este é o primeiro de uma série de posts que irão relatar nosso progresso neste projeto. Embora as postagens futuras sejam mais técnicas e destaquem o progresso e os desafios, este post é mais introdutório por natureza.

Então, o que está incluído no post exatamente? Começamos com uma introdução da empresa seguida por uma breve visão geral de dois tópicos mais próximos aos nossos corações - semântica de linguagem de programação e verificação formal. Em seguida, analisamos o KEVM, um projeto de semântica semelhante ao que estamos realizando para o WebAssembly, antes de concluirmos com um mergulho superficial no projeto KWasm, incluindo uma breve introdução da própria linguagem de programação do WebAssembly.

Vamos começar.

Quem é a Runtime Verification?

A Runtime Verification Inc. (RV) é uma empresa de tecnologia com sede em Urbana, Illinois. A empresa emprega uma nova abordagem de análise de software para analisar programas de computador estaticamente e à medida que são executados, identificando assim bugs, erros, falhas e possíveis explorações. A Runtime Verification é a principal desenvolvedora do K Framework. O K Framework gera automaticamente ferramentas para análise formal a partir de uma única especificação de uma linguagem de programação. A Runtime Verification fornece serviços de verificação sob medida para empresas e instituições aeroespaciais, automotivas e blockchain.

A Runtime Verification foi fundada em 2010 e originalmente começou a trabalhar com as unidades de P&D de empresas do espaço incorporado, que trabalham com empresas como Toyota, Boeing e Denso. Essas equipes de P&D foram responsáveis por escrever códigos de missão crítica para aviões, automóveis e ônibus espaciais. Códigos dessa natureza não devem falhar, mesmo que façam parte de sistemas complexos interagindo com o mundo mecânico. Vidas e meios de subsistência dependem diretamente da correção do código. É aqui que brilha a verificação formal, que é onde a Runtime Verification brilha.

A empresa foi reimaginada em 2017, depois de ser abordada por dois cofundadores da Ethereum, que perguntaram se havíamos considerado a aplicação de verificação formal para a blockchain. Exploramos oportunidades nessa indústria nascente em parcerias com construtores de infraestrutura como a IOHK e a Ethereum Foundation.

Avançamos rápido para 2019 e fornecemos serviços de verificação formal não apenas para construtores de infraestrutura, mas também para empresas, grandes e pequenas, que criam produtos e serviços em cima dessa infraestrutura. Até o momento, trabalhamos com IOHK, Ethereum Foundation, Algorand, Web3 Foundation, Tezos Foundation, Gnosis e MakerDAO.

Semântica de linguagem de programação e verificação formal — por que eu deveria me importar?

Veja como a Wikipedia define “semântica”:

“A semântica é o campo preocupado com o rigoroso estudo matemático do significado das linguagens de programação. Ela faz isso avaliando o significado de strings sintaticamente válidas definidas por uma linguagem de programação específica, mostrando a computação envolvida.”

Para tornar as coisas mais confusas, a palavra “semântica” denota tanto o nome do campo de estudo quanto a coisa que estuda. É semelhante a como “filosofia” pode se referir tanto ao campo como um todo, quanto a uma escola específica de pensamento. Uma semântica de uma linguagem de programação, digamos, para a EVM (Ethereum Virtual Machine), é uma expressão matemática correta por construção da linguagem de programação em questão. Em essência, é um conjunto de definições matemáticas que descreve o que um programa deve fazer. Pode conter declarações dizendo coisas como: “If cond is TRUE, then if cond then A else B = A”. Como você pode imaginar, os programadores geralmente têm fortes intuições sobre a semântica das linguagens que utilizam. Uma vez tendo uma semântica, você pode começar a executar e verificar programas escritos nessa linguagem de programação. Usando EVM novamente como exemplo, com uma semântica EVM você pode começar a executar e verificar formalmente contratos inteligentes.

Vamos agora tentar definir a verificação formal.

A verificação formal é o processo de provar rigorosamente que um modelo formal possui certas propriedades desejadas. O modelo formal e as propriedades são definidos usando formalismos matemáticos/lógicos. Quando o modelo formal é o de um programa em uma linguagem de programação específica e as propriedades desejadas capturam os requisitos desse programa, a verificação formal se torna a verificação do programa. Exemplos de propriedades que podem ser verificadas são “este loop termina” ou “o saldo variável nunca fica abaixo de 0”.

A verificação formal requer que primeiro escrevamos a especificação legível por humanos de um programa. A especificação libera o que o programa deve fazer. Uma vez que você tem a especificação, poderá verificar se o programa faz exatamente isso ou não. Na Runtime Verification, fazemos a verificação formal no nível de bytecode, em oposição ao próprio código-fonte. O resultado é um alto nível de garantia em relação à correção funcional do código. Se a verificação fosse feita no nível do código-fonte, não poderíamos saber se o bytecode que é implantado não possui bugs introduzidos pelo compilador.

Então, por que você deve verificar formalmente um contrato inteligente?

Contratos inteligentes, se escritos para uma blockchain não permissionada, são publicados em uma rede pública principal para o mundo inteiro ver. Isso significa exposição do seu código. Dado que os contratos inteligentes são usados para armazenar e transferir tokens, muitas vezes de um valor monetário significativo, eles são os principais alvos de ataque. Assim, você verifica seu contrato para eliminar bugs e erros em seu código que podem ser explorados por agentes mal-intencionados.

Descobrimos problemas em todos os contratos que verificamos formalmente. Nem sempre foram problemas que podem ser explorados, mas problemas que os clientes optaram por corrigir porque estão comprometidos com a exatidão de seus contratos. Contratos que parecem corretos podem ser quebrados com inputs específicos em casos específicos. Simplificando, a mente humana simplesmente não consegue acompanhar todos esses casos, e é por isso que são necessárias ferramentas baseadas em modelos matemáticos da infraestrutura da computação, ou seja, o bytecode EVM.

KEVM

Agora vamos mergulhar um pouco no KEVM, algo que mencionei acima. O KEVM está próximo e é querido dos nossos corações porque é sem dúvida o projeto que nos levou ao espaço blockchain e serviu como precursor do projeto KWasm. É importante mencionar que o KEVM foi generosamente financiado por Charles Hoskinson e pela Input Output Hong Kong (IOHK).

O KEVM é a primeira semântica executável por máquina, matematicamente formal, legível por humanos e completa da Máquina Virtual Ethereum (EVM). Como tal, o KEVM é capaz de passar pelos conjuntos completos de testes EVM VMTests e GeneralStateTests, e é utilizado na verificação formal de contratos inteligentes, depuração e muito mais. Um aspecto chave do KEVM (que ele herda por ser uma especificação K) é que a mesma semântica que é usada para executar os conjuntos de testes de conformidade é usada para verificação formal, o que significa que temos alta confiança de que os resultados de nossa verificação são precisos.

O KEVM foi proposto várias vezes como uma especificação oficial do EVM (mais notavelmente aqui: https://ethereum-magicians.org/t/jello-paper-as-canonical-evm-spec/2389), porque está escrito em um estilo totalmente legível por humanos e é testável (ao contrário do Yellow Paper da Ethereum). Ele é atualizado com os mais recentes hard forks da rede Ethereum, para que nossos esforços formais de verificação sejam relevantes para a blockchain Ethereum mais recente.

A maior conquista do KEVM, em nossa opinião, é que ele tem sido usado por terceiros para fazer a verificação (principalmente para verificar os contratos multicolaterais Dai usados pelo Maker Dao https://github.com/makerdao/k- dss). É claro que nós mesmos o usamos extensivamente para verificar contratos para nossos clientes, mas é bom saber que as pessoas estão tentando usar e melhorar nossas ferramentas. Para facilitar isso, discutimos muitas melhorias de usabilidade com terceiros que utilizam o KEVM e as implementamos (ou ajudamos a implementá-las) quando elas fizerem sentido para a visão geral do K. É ótimo termos uma ferramenta que nossos especialistas em K podem usar para verificar formalmente contratos, mas ainda melhor é ver a comunidade em geral testando e avaliando nossas ferramentas, fornecendo feedback e até mesmo implementando suas próprias ferramentas (por exemplo, o KLab da DappHub: https://github.com/dapphub/klab).

KWasm — nosso plano

Antes de mergulharmos em nosso plano para o KWasm, a semântica totalmente executável do WebAssembly, vamos ver brevemente o próprio WebAssembly. O texto abaixo foi retirado diretamente de https://webassembly.org/

WebAssembly (abreviado como Wasm) é um formato de instrução binária para uma máquina virtual baseada em pilha. O Wasm foi projetado como um destino portátil para compilação de linguagens de alto nível, como C/C++/Rust, permitindo a implantação na web para aplicativos cliente e servidor. É eficiente e rápido, seguro e protegido, aberto e depurável e parte da plataforma open web.

A Runtime Verification desenvolveu a semântica KWasm em antecipação às blockchains de próxima geração, muitas das quais usam Wasm. Embora o KEVM seja usado extensivamente pela Runtime Verification e pela comunidade mais ampla da Ethereum para verificar contratos inteligentes, a mudança iminente para o EWasm como a máquina virtual de destino – e o desenvolvimento de outras blockchains direcionadas ao Wasm – significa que as ferramentas em torno do EVM precisam ser redirecionadas para o Wasm.

Interessado em saber mais sobre a mudança para o EWasm? Confira estes artigos:

1. https://www.coindesk.com/open-heart-surgery-inside-ethereums-crucial-replacement-of-the-evm
2. https://hackernoon.com/diving-into-ethereums-virtual-machine-the-future-of-ewasm-wrk32iy
3. https://ewasm.readthedocs.io/en/mkdocs/

Embora tenhamos feito um grande progresso no KWasm, ainda há trabalho a ser feito para ajustar a semântica para execução simbólica.

Execução simbólica

A execução simbólica é a execução de um programa, apenas com variáveis em vez de valores concretos em alguns lugares. Pense assim: semântica é uma descrição de como um programa deve computar seu resultado. Computação e cálculo são apenas dois lados da mesma moeda. Dado o programa a = 2; b = 3; c = 5; print(1/(c*(b+a))); podemos computar que o programa exibirá o output 25. Não importa a aparência do programa, sempre podemos executá-lo e ver o que ele produz, assim como podemos calcular qualquer expressão aritmética, por exemplo, (2 + 3) * 5.

A execução simbólica está para a computação o que a álgebra está para o cálculo. Dada a expressão (X + (X+1)) * (X + 2), não podemos computar um resultado. Podemos apenas reescrevê-la, por exemplo, para 2X² + 5X + 2. O que podemos fazer, porém, é fazer deduções sobre a expressão. E como a expressão concreta, com valores 2, 3 e 5, é apenas um caso especial da expressão algébrica, qualquer coisa que possamos deduzir sobre a expressão algébrica também é válida para a expressão concreta e todas as expressões semelhantes. Por exemplo, sabemos que para qualquer valor de X > -½, (X + (X+1)) * (X + 2) é positivo. Também podemos descobrir se existem condições extremas interessantes como, se o resultado pode ser 0, o que pode (em -2 e -½).

Na execução simbólica, em vez de resultados totalmente avaliados, acabamos com resultados simbólicos. Por exemplo, dê uma olhada no programa a seguir. Quais são os perigos?

function foo(int a, b, c) {
assert (a > b, b >= 0)
if (c != 0) {
d = c * a
if (b == -a) {
return d;
} else {
d = d + b * c;
return 1 / d; // Área de perigo.
}
}
return 0;
}

Digamos que iremos passar do assert. Executando esse programa simbolicamente, percebemos que ele pode retornar 0, c * a, ou 1/ (c * (b + a)), com a, b e c desconhecidos. Agora queremos decidir se esta divisão é segura. Obviamente não é se a, b e c puderem ser qualquer valor. Mas é raro que as variáveis sejam completamente irrestritas. Por exemplo, neste caso as condições assert e if garantem que c != 0 e que a > b >= 0, nesse caso, as coisas parecem seguras. Mas o programador pode ter perdido a possibilidade de overflow: se os valores integer são 4 bytes, c = 2³¹, b = 0 e a = 2, obtemos uma divisão por 0.

Muitas vezes é difícil detectar esses casos com testes. Em um exemplo fictício como o acima, um verificador pode usar caneta e papel para garantir que todos os resultados possíveis sejam cobertos. Com programas maiores, é mais fácil (e mais rápido) usar a execução simbólica para obter expressões algébricas dos possíveis estados que um programa pode ter quando termina. Eles podem ser analisados manualmente ou, como fazemos na Runtime Verification, com ferramentas automatizadas, como solucionadores SMT (mais sobre isso em um post posterior).

O ajuste virá em três formas: (i) ajustar o backend Haskell do K Framework para poder lidar com provas do KWasm, (ii) ajustar o KWasm para ser mais adequado para execução simbólica e (iii) adicionar lemas padrão ao pacote global que todas as provas KWasm podem usar. Todas as três categorias beneficiarão todos os usuários do KWasm que tentam verificar contratos inteligentes escritos em Wasm.

Agora, vamos dar uma olhada nas entregas esperadas para este projeto

• Selecione seis programas Wasm para verificar utilizando o KWasm, e em cada verificação, use incrementalmente mais recursos do Wasm e uma lógica de programa mais complicada.
• Escreva especificações K para cada algoritmo, aproximadamente uma por mês, juntamente com as atualizações do KWasm necessárias para verificar a viabilidade do algoritmo.
• Integre as especificações K desenvolvidas ao KWasm CI (Kwasm Continuous Integration), para que futuras atualizações do KWasm não quebrem as especificações.
• Esboce e publique a documentação online atualizada em pushes para o repositório KWasm.

Desde o início iremos (i) selecionar o programa “mensal” alvo para verificar, (ii) implementar o referido programa no WASM e, finalmente, (iii) verificar o referido programa.

O primeiro algoritmo que verificaremos será um contrato WRC20 (https://gist.github.com/axic/16158c5c88fbc7b1d09dfa8c658bc363), a adaptação WASM de um ERC20. O ERC20 é o padrão de token mais básico usado na Ethereum e é o bloco de construção de muitos outros tokens. Este programa não tem loops nem manipulação de heap, por isso serve como um bom primeiro passo para resolver problemas no KWasm em relação à execução simbólica, além de ser altamente aplicável ao domínio do contrato inteligente. Nota rápida, o contrato WRC20 não possui todos os recursos de um ERC20 (com permissões e função s totalBalance), ele pode apenas transferir tokens e consultar saldos.

Interessado em um pouco mais de informações sobre o ERC20? Confira esses recursos.

1. Padrões do token ERC20: https://eips.ethereum.org/EIPS/eip-20
2. Postagem do blog da Runtime Verification sobre nossa especificação executável do ERC20: https://runtimeverification.com/blog/erc20-k-formal-executable-specification-of-erc20/
3. Interfaces, contratos e utilitários relacionados ao ERC20, criados pelo grandes amigos do Open Zeppelin: https://github.com/OpenZeppelin/openzeppelin-contracts/tree/master/contracts/token/ERC20

Esperamos que você tenha gostado deste post introdutório. Como mencionado anteriormente, as postagens futuras se concentrarão em atualizações específicas do projeto KWasm. Mais uma vez, um grande obrigado à Emurgo, SOSV e dlab pelo apoio.

Obrigado por ler.

Artigo publicado por Patrick MacKay em 17 de novembro de 2019, traduzido por Paulinho Giovannini. Você pode encontrar a publicação original aqui.