面向 Solidity 智能合约的自动不变式生成
软件工程
2024-01-02 v1
摘要
智能合约是在区块链上运行的计算机程序，用于自动化执行用户间的交易。合约规范的缺失对智能合约的正确性验证构成了真正的挑战。程序不变式是在整个执行过程中始终保持的性质，刻画了程序行为的一个重要方面。在本文中，我们提出了一种用于 Solidity 智能合约的新型不变式生成框架 INVCON+。INVCON+ 扩展了现有的不变式检测器 InvCon，基于动态推断和静态验证自动生成已验证的合约不变式。与 INVCON+ 不同，InvCon 仅生成极可能成立但尚未针对合约代码进行验证的不变式。特别是，INVCON+ 能够推断出更具表达力的不变式，以捕捉合约代码中更丰富的语义关系。我们在 361 个 ERC20 和 10 个 ERC721 真实世界合约以及常见的 ERC20 漏洞基准上评估了 INVCON+。实验结果表明，INVCON+ 能够高效地生成高质量的不变式规范，可用于保护智能合约免受常见漏洞的威胁。
引用
@article{arxiv.2401.00650,
title = {Automated Invariant Generation for Solidity Smart Contracts},
author = {Ye Liu and Chengxuan Zhang and Yi Li.},
journal= {arXiv preprint arXiv:2401.00650},
year = {2024}
}