Automated Vulnerability Fixing in (DeFi) Smart Contracts

According to some reports, as much as $1.3 billion were lost in DeFi hacks in 2021. Many of these attacks were enabled by well-known smart contract vulnerabilities or were caused by trivial mistakes made by smart contract developers. Automated program repair techniques aim to alleviate developers' burden of manually fixing such bugs by automatically generating patches for a given issue. The three challenges of smart contract repair are: identify the bug, fix the bug without breaking anything, and determine what constitutes "breaking something" in the absence of the formal specification. In this talk, we discuss how formal analysis techniques may assist in solving those issues. First, we use symbolic execution to detect the bug via detecting a violation of specific properties. We also demonstrate how symbolic execution can also be used to automatically infer specification of a smart contract. This allows us to assess the patches that we generate by mutating the source code of a smart contract. Our multi-component technique efficiently navigates the search space, generates higher-quality patches, and assesses them against the inferred specification.