PropertyGPT 是一个端到端系统，它利用大型语言模型 (LLM) 来自动生成用于 智能合约 正式验证的全面属性。该白皮书的作者是 Ye Liu、Yue Xue、Daoyuan Wu、Yuqiang Sun、Yi Li、Miaolei Shi 和 Yang Liu。 ^[1]

概述

PropertyGPT 通过使用先进的自然语言处理（特别是 GPT 模型）自动生成验证规则，从而应对 智能合约 安全性的挑战。这项技术理解复杂的代码特征，并自动转移知识以创建高效且广泛适用的安全规则。PropertyGPT 通过减少与制定这些规则相关的成本和时间，从而减少对安全专家的依赖。这种方法使 PropertyGPT 能够快速生成大量适用于 智能合约 多样化和复杂性质的不变验证规则，确保它们符合严格的安全标准。自动化规则生成简化了安全审计流程并降低了总体成本，从而使更多项目能够在开发的早期阶段保护其 智能合约。 ^[1][2]

该系统已经过实施和评估，使用了来自 23 个 Certora 项目的 623 个人工编写的属性，实现了 80% 的召回率。PropertyGPT 在这些项目中检测到了 CVE、攻击事件和零日漏洞，从而获得了漏洞赏金奖励。它使用迁移学习、检索增强生成以及涉及符号执行、模块化验证和有界模型检查的属性验证过程来检测各种 智能合约 漏洞。 ^[1][2]

技术

向量数据库

PropertyGPT 中的向量数据库是一个关键组件，有助于检索相似的代码并将其映射到其原始参考属性。它通过将与参考属性相对应的关键代码嵌入到数值表示（通常是向量）中来构建。

• 向量数据库的创建：向量数据库是通过嵌入与参考属性相关的代码的重要部分来形成的。此过程将代码转换为数值表示或向量。
• 相似代码的检索：当 PropertyGPT 接收用于属性生成的主题代码时，它会查询向量数据库以检索在一定阈值内的相似代码。相似性基于数据库中代码的数值表示，阈值过滤掉不相似的代码。
• 映射到参考属性：从向量数据库检索到相似代码后，PropertyGPT 会将每段代码映射到其原始参考属性。此映射确保生成的属性基于现有的相关属性，从而利用参考属性中编码的知识来实现更准确和特定于上下文的属性生成。

向量数据库充当代码表示的存储库，捕获参考属性的本质，使 PropertyGPT 能够通过检索相似代码并将其映射到参考属性来为未知代码生成自定义属性。嵌入和相似性计算技术的具体细节取决于 PropertyGPT 背后的研究人员选择的方法和算法。 ^[1][2]

迭代属性生成

PropertyGPT 中的迭代属性生成涉及创建和改进主题代码的候选属性，以确保其正确性和可编译性。该过程首先从向量数据库中检索与主题代码相似的参考属性。这些参考属性充当示例，并为生成候选属性提供了一个起点。然后，生成提示指导这些属性的创建，重点关注结构和语法方面，而不是特定的变量或函数名称。 ^[1]

一旦生成候选属性，就会使用属性规范语言 (PSL) 编译器检查它们是否存在编译错误。未能编译的属性表明生成的代码中存在错误或不一致。PropertyGPT 采用修改提示来指导迭代修改过程，指示语言模型修复规则代码并纠正任何错误，同时保持结构和语法一致性。语言模型分析错误，识别必要的修复，并生成属性的修订版本。此迭代过程持续进行，直到属性可编译或达到最大修订尝试次数。 ^[1]

除了通过编译确保属性的语法正确性之外，PropertyGPT 还执行额外的检查以确保属性有意义并捕获预期的行为。例如，它验证属性是否包含目标主题函数，以及它们在功能上对于测试所需的行为是否有意义。通过迭代生成和修改候选属性，PropertyGPT 旨在生成在语法上正确且在功能上对主题代码有意义的属性。这种迭代方法允许改进和完善，从而提高生成属性的准确性和有效性。 ^[1]

属性规范语言 (PSL)

属性规范语言 (PSL) 是 PropertyGPT 中提出的一种中间语言，用于指定 智能合约 属性。PSL 扩展了 Solidity 编程语言，提供了一种结构化且富有表现力的方式来定义属性。它允许定义不变量，这些不变量是在 合约 执行期间必须始终保持的属性。这些不变量是在状态变量上定义的，确保在 合约 的整个生命周期中保持基本特征和约束。 ^[1][3]

函数前置条件和后置条件也使用 Hoare 三元组支持。前置条件指定在执行函数之前必须满足的要求，而后置条件定义函数执行后的预期结果或保证。这有助于确保各个函数的正确性和功能。 ^[1][3]

PSL 中的基于场景的属性是在受限环境或特定条件下定义的，并通过假设和断言实现为不同的规则。假设涉及 合约 的状态或需要满足的条件，而断言检查 合约 中的特定条件或行为。PSL 与 Solidity 共享其大部分语法和结构，从而可以轻松编写合约规范并避免复杂的逻辑绑定。这种简单性增强了编写和维护规范的简易性。 ^[1][3]

PSL 规范是可重用和可升级的，因为 PSL 是 Solidity 的自定义变体，允许继承和模块化管理。这有助于包含其他 合约 规范，从而实现重用和扩展。此外，PSL 规范可以直接从 合约 代码自动生成，从而确保规范质量并减少错误和不一致的可能性。 ^[1][3]

形式化证明器

PropertyGPT 中的形式化证明器是一个组件，旨在验证为 智能合约 生成的属性的正确性。它采用形式化验证技术来严格分析属性和 合约 代码，确保它们在所有可能的执行场景下的准确性。这涉及应用逻辑推理和数学方法来确认系统满足指定的属性或规范。 ^[1]

在 PropertyGPT 中，形式化证明器检查以属性规范语言 (PSL) 指定的合约代码和属性。它分析控制流、数据流和状态转换，以验证是否满足属性。证明器使用模型检查、定理证明或符号执行。模型检查探索所有系统状态和转换，定理证明使用数学逻辑来建立属性，符号执行考虑所有可能的输入和路径来验证属性。 ^[1]

在验证期间，证明器可能会识别出违反属性的反例或场景，帮助开发人员了解导致这些违规的特定条件，并使他们能够解决 合约 代码中的潜在漏洞。通过识别潜在的问题和不一致，形式化证明器增强了智能合约的安全性和可靠性，确保它们按预期运行并降低了漏洞利用或失败的风险。形式化证明器使用的具体技术和算法因合约代码的复杂性、要验证的属性以及所需的保证级别而异。 ^[1]

加权算法

PropertyGPT 中的加权算法根据生成的属性的相关性和重要性为其分配权重。该过程首先使用迭代方法为主题代码生成一组候选属性。然后，通过分析其与主题代码的相似性并考虑代码的上下文和目的来评估每个候选属性的相关性。 ^[1][2]

在此之后，根据复杂性、关键性和影响等因素评估每个候选属性的重要性。根据这些相关性和重要性评估，将权重分配给每个候选属性。候选属性根据其分配的权重进行排名，权重越高表示优先级越高。 ^[1][2]

该算法允许根据用户反馈或特定领域的知识迭代改进权重和排名。这种方法确保了有针对性且高效的属性生成方法，优先考虑用于测试和验证的最相关和最重要的属性。通过考虑相似性的多个维度并相应地分配权重，该算法捕获关键行为，确保正确性并提高形式化验证的有效性。 ^[1][2]