Dissertação
Refining High-Level Specifications of Decentralized Finance Protocols to EVM bytecode using the K framework EVALUATED
Blockchains possibilitam uma economia democrática, aberta, e escalável baseada em mecanismos de consenso distribuídos descentralizados sem a necessidade de confiar em terceiros. Estas podem ser desenvolvidas com máquinas virtuais que permitem a execução de programas arbitrários, chamados de Smart Contracts. Em Ethereum, a Ethereum Virtual Machine é a máquina virtual global cujo estado é guardado e concordado por todos os participantes da rede. Recentemente, a quantidade de Smart Contracts implementados em Ethereum e a sua complexidade aumentou rapidamente. A interoperabilidade entre eles que a EVM oferece levou ao emergir de um ecossistema de aplicações e protocolos financeiros, chamado de Finanças Descentralizadas. Considerando que estes protocolos asseguram vastas quantidades de capital, erros ou comportamento não intencional frequentemente leva a perdas financeiras catastróficas para os seus utilizadores. Consequentemente, métodos de verificação formal para estes protocolos têm sido alvo de estudo recentemente. A K Framework é uma das mais sofisticadas e capazes frameworks para definir e verificar linguagens. Esta permite definir especificações executáveis arbitrarias de protocolos tal como executar diretamente o seu bytecode com a implementação da EVM em K. Nesta dissertação o objetivo é melhorar a segurança destes protocolos. Para o atingir introduzimos nova documentação para a MakerDAO, um protocolo pioneiro em DeFi, tal como para a sua especificação abstrata em K. Adicionalmente, estendemos a especificação abstrata com um novo modulo e uma invariante do sistema não trivial. Finalmente, desenvolvemos e demonstramos métodos de refinação que permitem provas de refinamento que conectam especificações abstratas de protocolos com a sua implementação em bytecode.
dezembro 3, 2021, 14:30
Publicação
Obra sujeita a Direitos de Autor
Orientação
ORIENTADOR
João Fernando Peixoto Ferreira
Departamento de Engenharia Informática (DEI)
Professor Auxiliar
