FenixEdu™

Dissertação

Model-checking Ethereum smart contracts written in Vyper EVALUATED

Detalhes: A plataforma de blockchain Ethereum foi a primeira a introduzir o conceito de smart contract, um programa de computador armazenado e executado na blockchain. Os smart contracts são capazes de guardar bens digitais e de comunicar entre si, tornando-os ideais para a implementação de aplicações financeiras descentralizadas. Dado que os smart contracts são imutáveis após a sua integração na blockchain e que efectuam transacções de bens com valor monetário, é da máxima importância que o seu comportamento seja o esperado e que sejam resilientes a ataques. Uma forma de assegurar ambos é através da verificação formal. O objectivo deste trabalho foi desenvolver uma ferramenta que traduza automaticamente smart contracts escritos em Vyper para a linguagem nuXmv. Vyper é uma nova linguagem de programação para contratos Ethereum, desenhada para ser mais simples e segura, enquanto que o nuXmv é um verificador de modelos utilizado para verificar propriedades de invariância e temporais. Esta tradução permite utilizar o nuXmv para tentar provar propriedades de smart contracts especificadas naquele formato. Tendo em conta as limitações da linguagem nuXmv, definimos uma sub-linguagem do Vyper, denominada MiniVyper, juntamente com as suas sintaxe concreta e semântica operacional, a segunda servindo como base para a tradução. Este trabalho representa não só uma das primeiras tentativas de definir uma técnica de verificação formal específica para smart contracts Vyper, como uma das primeiras descrições formais de um subconjunto desta linguagem. Testámos este método de verificação traduzindo e verificando propriedades de contratos reais e detectámos alguns erros de concepção.
Keywords: blockchain, Ethereum, Vyper, verificação de modelos, verificação formal, semântica operacional

Discussão: Dezembro 18, 2019, 16:0