Trusted Deployer: A Tool for Safe Creation and Upgrade of Ethereum Smart Contracts - Ferreira, Juliandson; Antonino, Pedro; Sampaio, Augusto; Roscoe, A. W.; Arruda, Filipe (Anais do Simpósio Brasileiro de Métodos Formais (SBMF), 2024)
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.