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.
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
