Dissertação

Formal verification of Ethereum smart contracts using Isabelle/HOL EVALUATED

O conceito de blockchain foi desenvolvido com o objectivo de descentralizar a troca de bens, suprimindo a necessidade de intermediários durante o processo. Propõe-se a atingir uma confiança digital entre as partes envolvidas. A blockchain consiste num arquivo público e imutável, constituído por blocos ordenados cronologicamente tais que cada contém o registo de um conjunto finito de transacções. A plataforma Ethereum, que esta tese aborda particularmente, é implementada numa arquitectura blockchain e introduz, ainda, a possibilidade de guardar programas Turing completos, denominados por smart contracts. Apesar de a sua linguagem núcleo ser EVM bytecode, também podem ser implementados usando linguagens de alto nível, sendo Solidity a mais usada. Entre as suas aplicações destacam-se o armazenamento de informação descentralizado, a tokenização de bens e a gestão de sistemas de verificação de identidades digitais. Nesta tese é proposto um método para a verificação formal de smart contracts escritos em Solidity. Uma linguagem imperativa que descreve grande parte da linguagem Solidity, é implementada no assistente de prova Isabelle/HOL, ao qual é associada a uma semântica de execução big-step. Propriedades acerca dos programas são descritas usando cálculo de Hoare, um sistema formal é definido para a linguagem, para o qual são apresentados resultados de correcção e completude. É descrita a verificação de um smart contract de voto electrónico que demonstra a complexidade de prova que consegue ser alcançada com este método. São também apresentados exemplos de vulnerabilidade existentes como bugs de overflow ou re-entrância.
verificação formal, Isabelle/HOL, cálculo de Hoare, Ethereum, blockchain, contractos inteligentes

Dezembro 18, 2019, 18:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Pedro Miguel dos Santos Alves Madeira Adão

Departamento de Engenharia Informática (DEI)

Professor Auxiliar

ORIENTADOR

Paulo Alexandre Carreira Mateus

Departamento de Matemática (DM)

Professor Catedrático