Securing smart contracts with formal verification and automated program repair

Abstract

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.