Pós-Graduação em Ciência da Computação – UFPE
Defesa de Dissertação de Mestrado Nº 2.052

Aluno: Juliandson Estanislau Ferreira
Orientador: Prof. Augusto Cezar Alves Sampaio
Co-orientador: Prof. Pedro Ribeiro Gonçalves Antonino (Universidade de Oxford)
Título: Specification is Law: Safe Creation and Upgrade of Ethereum Smart 
Contracts
Data: 12/09/2022
Hora/Local: 10h – Virtual – Interessados em assistir entrar em contato com o aluno
Banca Examinadora:
Prof. Alexandre Cabral Mota (UFPE / Centro de Informática)
Prof.  Fabiola Gonçalves Pereira Greve (UFBA / Departamento de Ciência da Computação)
Prof. Augusto Cezar Alves Sampaio (UFPE / Centro de Informática)


RESUMO:

Contratos inteligentes são a base do paradigma “code is law”. O código do 
contrato inteligente descreve indiscutivelmente como seus ativos devem ser 
gerenciados – uma vez criado, seu código normalmente é imutável. Contratos 
inteligentes com falhas apresentam significativa evidência contra a 
praticidade desse paradigma; os bugs resultaram em perdas de ativos no 
valor de milhões de dólares. Para resolver esse problema, a comunidade 
Ethereum propôs (i) ferramentas e processos para auditar/analisar contratos 
inteligentes e (ii) padrões de design que implementam um mecanismo para 
tornar o código do contrato mutável. Individualmente, (i) e (ii) abordam 
apenas parcialmente os desafios levantados pelo paradigma “code is law”. 
Neste trabalho, combinamos elementos de (i) e (ii) para criar uma estrutura 
sistemática que se afasta do “code is law” e dá origem a um novo 
paradigma “specification is law”. Ele permite que contratos sejam criados e 
atualizados, mas somente se eles atenderem a uma especificação formal 
correspondente. A estrutura é centrada em um trusted deployer: um serviço 
off-chain que verifica e reforça formalmente essa noção de conformidade. 
Com essa estrutura, contratos com falhas devem ser impedidos de serem 
implantados e atualizações seguras podem ser realizadas para otimizar o 
código do contrato, por exemplo. Prototipamos essa estrutura e investigamos 
sua aplicabilidade a contratos que implementam três padrões Ethereum 
amplamente usados: o ERC20 Token Standard, ERC3156 Flash Loans e ERC1155 
Multi Token Standard.

Palavras-chave: Formal Verification, Smart Contracts, Ethereum, Solidity, 
Safe Deployment e Safe Upgrade.

Comentários desativados