一句话：提出 DeFinery，结合搜索式补丁生成与语义规约推断，自动修复不满足用户性质约束的 DeFi 智能合约。
智能合约编程错误可导致安全攻击，而现有智能合约自动修复工具多针对典型漏洞，难以处理 DeFi 合约中功能规约违背：实现与预期金融模型不一致会造成资金损失。本文提出 DeFinery，一种面向用户定义正确性质的自动修复技术。它将基于搜索的补丁生成与对原程序的语义分析结合，以推断规约，从而在探索多样补丁的同时提供相对预期行为的形式化正确性保证。作者在 9 个真实世界与基准智能合约上评估，表明 DeFinery 能高效生成高质量补丁，且这些补丁无法被现有工具发现。
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 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. 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 9 real-world and benchmark smart contracts prove that DeFinery efficiently generates high-quality patches that cannot be found by other existing tools.