Dissertação

Formal analysis and gas estimation for Ethereum smart contracts EVALUATED

A plataforma Ethereum constitui um ecossistema para o desenvolvimento de smart contracts – programas que se encontram guardados numa blockchain pública e que podem interagir entre si. Sistemas de verificação formal para estas plataformas são muito importantes, uma vez que as modificações feitas na blockchain são irreversíveis e podem envolver valores monetários. Nesta dissertação estudamos a máquina virtual de Ethereum e implementamos uma máquina virtual de Ethereum simbólica em Mathematica na qual é possível executar smart contracts com input simbólico. Esta máquina é utilizada no desenvolvimento de uma ferramenta que simula todos os caminhos possíveis num smart contract e que, no final, devolve todos os estados finais possíveis do sistema. Esta abordagem exaustiva permite a verificação de propriedades acerca do estado global do sistema após a execução de um contrato. Além disso, estendemos as regras semânticas da máquina clássica à maquina simbólica. A execução de código na blockchain tem um custo que depende do estado global do sistema e do input dado ao código. Exploramos a temática dos custos em gas e utilizamos a máquina virtual simbólica na construção de um programa que estima o custo da execução de uma função de um contrato. Esta vai além do que era alcançado por trabalhos anteriores dado que não só considera uma classe de contratos mais alargada como também devolve informação mais detalhada, nomeadamente, aceita código que contém ciclos com um número fixo de iterações e devolve o custo de cada caminho de execução em vez de um único majorante.
verificação formal, execução simbólica, análise de controlo de fluxo, semântica operacional, Ethereum, blockchain

Dezembro 14, 2018, 15:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Paulo Alexandre Carreira Mateus

Departamento de Matemática (DM)

Professor Associado