一句话:用验证器反馈训练的统计模型加速生成-验证式补丁搜索,实现智能合约漏洞的全自动、安全可保证修复。
智能合约属于安全关键软件,人工调试困难且易错,而现有自动修复技术难以同时兼顾高修复率、全自动与安全性保证。SmartFix 采用“生成-验证”范式:迭代枚举候选补丁,并调用安全验证器确认补丁正确性,从而提供安全保证。该范式的核心挑战在于搜索空间巨大且基于验证的补丁校验开销高昂。为此,作者提出利用验证器反馈信息构建统计模型,对搜索过程进行加速,从而在保持全自动与安全保证的同时大幅提升修复效率。在真实以太坊智能合约上的实验表明,SmartFix 对关键漏洞类别的修复成功率达到 94.8%,显著超过现有最先进技术 sGuard 的 65.4%。
We present SmartFix, a new technique for repairing vulnerable smart contracts. There is an urgent need to develop automatic bug-repair techniques for smart contracts, as smart contracts are safety-critical software and manual debugging is burdensome and error-prone. While several repair approaches have been proposed recently, they are unsatisfactory since no existing techniques can achieve high repairability, full automation, and safety guarantee at the same time, posing significant problems for practical use. SmartFix aims to address these shortcomings by using a “generate-and-verify” approach that iteratively enumerates candidate patches while validating their correctness by invoking a safety verifier. However, in this approach, a technical challenge arises as the search space is huge and the verification-based patch validation is expensive. To address this challenge, we present a novel technique for accelerating the generate-and-verify repair procedure using statistical models derived from the verifier’s feedback. Experimental results on real-world Ethereum smart contracts show that SmartFix is able to achieve a fix success rate of 94.8% for critical classes of vulnerabilities, far outperforming sGuard, the existing state-of-the-art technique whose success rate is 65.4%.