Trusted Deployer: A Tool for Safe Creation and Upgrade of Ethereum Smart Contracts

• Juliandson Ferreira UFPE
• Pedro Antonino The Blockhouse Technology Limited
• Augusto Sampaio UFPE
• A. W. Roscoe The Blockhouse Technology Limited / University College Oxford
• Filipe Arruda UFPE

Resumo

The lack of systematic and, particularly, mechanised support to ensure a safe creation and upgrade of smart contracts has led to the deployment of instances with flaws that have been thoroughly exploited, putting digital assets at risk. Formal verification can potentially help to eliminate these high impact flaws, particularly by allowing one to check whether smart contracts obey some desired properties. We have already proposed the concept of a trusted deployer to address these issues. In this work we present the detailed design of a public, open-source, and off-chain tool that supports the creation and upgrade of smart contracts, ensuring that they meet corresponding formal specifications. We detail the tool’s overall architecture, its usage, and its applicability to real-world smart contracts.