arXiv:2502.07644v2 宣布类型: 新 摘要: 为了治理在以太坊上运行的智能合约，已经开发出了多种以太坊请求评论（ERC）标准，每种标准都有一套规则来指导智能合约的行为。违反ERC规则可能会导致严重的安全问题和经济损失，凸显了验证智能合约遵循ERC规则的重要性。当前验证这些规则的方法是手动审计每个单独的合约、使用专家开发的程序分析工具或使用大型语言模型（LLMs），所有这些方法都远不能有效识别ERC规则的违规行为。本文介绍了SymGPT，这是一种将大型语言模型（LLMs）的自然语言理解与形式化的符号执行保证相结合的工具，用于自动验证智能合约是否符合ERC规则。为了开发SymGPT，我们对三个广泛使用的ERC标准中的132条ERC规则进行了实证研究，检查了它们的内容、安全影响和自然语言描述。基于这些研究，我们设计SymGPT，首先指示LLM将ERC规则翻译成定义好的EBNF语法。然后，我们从正式化的规则中综合约束来表示可能发生违规的情况，并使用符号执行来检测这些情况。我们的评估显示，SymGPT在4000个真实世界的合约中发现了5783条ERC规则的违规行为，其中包括1375条带有明确攻击路径以盗取金融资产的违规行为，证明了其有效性。此外，SymGPT在与六种自动化技术和安全专家审计服务的比较中表现出色，进一步凸显了它在当前智能合约分析方法上的优越性。