Securing smart contracts with formal verification and automated program repair

• Main Author: Tolmach, Palina
• Other Authors: Liu Yang
• Format: Thesis-Doctor of Philosophy
• Language: English
• Published: Nanyang Technological University 2023
• Subjects: Engineering::Computer science and engineering::Software::Software engineering
• Online Access: https://hdl.handle.net/10356/169305
• Institution: Nanyang Technological University

Bugs enable security attacks on smart contracts—computer programs operating on the blockchain and managing significant financial assets. In 2022, smart contracts control tens of billions of dollars, forming an entire ecosystem of so-called decentralized financial (DeFi) applications. The ever-increasing popularity of DeFi is largely attributed to its key principles, such as transparency, permissionlessness, and immutability. Unfortunately, the devastating hacks that accompany smart contract adoption demonstrate how these properties can also have adverse effects on the security of decentralized applications, considering that, like any other software, smart contracts can contain bugs or vulnerabilities. A seminal property of smart contracts—immutability—makes sure that all these implementation errors will have a long-lasting effect on the application. Considering that smart contracts also hold large amounts of funds, it is crucial to ensure that they are secure, correct, and free of vulnerabilities. A common approach to ensuring security and correctness of safety-critical software, including smart contracts, is through formal verification. However, despite the extensive research done on smart contract verification, there is still no obvious solution for safe smart contract development. This thesis contributes a series of theoretical and practical improvements for major components of the security and correctness assurance pipeline for smart contracts. The contributions cover a wide range of problems, including consolidation of existing smart contract specification and verification research; symbolic execution and model checking techniques for formal analyses of smart contracts w.r.t. custom security and correctness properties in a compositional manner; as well as a novel approach for property-based automated repair of individual or a group of interacting smart contracts, which combines semantics-based specification inference with search-based patch generation to produce diverse patches with solid correctness guarantees. First, we conduct a large-scale survey of formal modeling, specification, and verification techniques for smart contracts. We utilize a multi-layer framework for categorization of formal techniques proposed in 202 analyzed publications. We also contribute a taxonomy of properties specified for smart contracts across different domains. The holistic view of formal techniques adopted in this thesis helps us identify trends and challenges in smart contract analysis and establish the connections between various types of smart contract properties and the formalization and verification approaches supporting them, creating a clearer guideline for choosing a suitable formal analysis technique. Major research gaps identified within the survey include limited support of property-based analyses, as well as the need for analyzing complex compositions of smart contracts. Our survey also recognizes automated repair of smart contracts as a promising direction, considering the high costs and risks of manual bug fixing. To address the lack of property-based and compositional analyses, we present a formal approach to model and verify a system of interconnected DeFi smart contracts in a compositional manner. To perform a case study of two interacting DeFi protocols, we develop formal definitions for the key elements of DeFi applications and model their implementations and interactions using a process-algebraic formal modeling language. Based on this model, we perform model checking to verify relevant correctness properties of the analyzed protocols automatically. We also contribute a set of safety and correctness financial properties that should hold across all protocols’ interactions and demonstrate how these properties can be violated due to the unintended effects of stacking DeFi protocols together. Although effective in smart contract verification, this approach requires manual translation of smart contracts’ code into the modeling language, making the entry threshold high for a regular smart contract developer. To make smart contract analysis more practical, we propose another technique that formalizes the source code automatically—an easy-to-use symbolic execution engine SolSEE for smart contracts implemented in Solidity—the most popular smart contract language. Our results demonstrate that SolSEE outperforms other existing source-level analysis tools for Solidity in terms of advanced language features supported as well as the analysis flexibility, which makes it effective in analyzing interacting smart contracts based on user-defined properties. SolSEE also offers a graphical interface, enabling visual inspection and debugging of smart contract executions. Finally, to assist smart contract developers with bug fixing, we propose a novel automated program repair technique for smart contracts called DeFinery. Different from existing smart contracts repair tools that only fix common vulnerabilities, DeFinery automatically rectifies a smart contract that violates a user-defined correctness property. To generate a larger set of diverse patches while offering strong correctness guarantees, DeFinery combines search-based patch generation with semantic inference of the original smart contract’s specification. Our experiments show that DeFinery efficiently produces high-quality patches that other existing tools are unable to synthesize.