DeFinery
Property-Based Automated Program Repair of DeFi Protocols
Abstract
Programming errors enable security attacks on smart contracts, which are used to manage large sums of financial assets. Automated program repair (APR) techniques aim to reduce developers’ burden of manually fixing bugs by automatically generating patches for a given issue. Existing APR tools for smart contracts focus on mitigating typical smart contract vulnerabilities rather than violations of functional specification. However, in decentralized financial (DeFi) smart contracts, the inconsistency between intended behavior and implementation translates into the deviation from the underlying financial model, resulting in irrecoverable monetary losses for the application and its users. In this work, we propose DeFinery—a technique for automated repair of a smart contract that does not satisfy a user-defined correctness property, financial or otherwise. To explore a larger set of diverse patches while providing formal correctness guarantees w.r.t. the intended behavior, we combine search-based patch generation with semantic analysis of an original program for inferring its specification. Our experiments in repairing nine real-world and benchmark smart contracts reveal that DeFinery efficiently navigates the search space and generates higher-quality patches that cannot be obtained by other smart contract APR tools.
Framework Overview
DeFinery comprises two main components: a semantic analysis module and a patch generation module.
(1) First, semantic analysis (SA) module symbolically executes an input smart contract w.r.t. a property and a sequence of functions leading to its violation.
(2) For each execution path, it generates a “test case” by setting symbolic variables to concrete values generated by an SMT-solver. To enable more thorough assessment of patches, it also summarizes the observed valid behaviors in a symbolic summary.
(3) Given a set of function names appearing in the trace, test cases, and a symbolic summary, the patch generation (PG) module mutates these functions’ code using a genetic algorithm and a set of heuristics.
(4) For each generated candidate, it invokes the symbolic execution component to check the test cases and analyzes the results. If all test cases pass, we assume the patch might be plausible.
(5) In this case, the SA module is used to build a symbolic summary once again—this time for a patched smart contract. An SMT-solver is then used to perform conditional equivalence checking between the original and the patched symbolic summaries under valid inputs.