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