通过形式化验证保护Aptos框架的安全

作者：Aptos Labs, MoveBit, and OtterSec.

Aptos框架经过了持续的严格测试和全面审计。为了进一步提高保证水平，我们对其安全性和正确性进行了正式验证。

我们与OtterSec合作，对Aptos框架进行审计，并确定每个模块的关键安全要求。
我们与MoveBit合作，为框架的大部分内容创建正式规范，然后使用Move Prover进行验证。
这种综合努力使Aptos框架在区块链行业及其他领域获得了无与伦比的质量保证水平。

· 简介
· Move Prover是什么？
· Move规范语言。
· 我们取得了什么成就？
· 形式验证的影响。
· 结论和未来计划。

简介
Aptos框架是一组Move智能合约模块的集合，用于定义Aptos网络的标准和常见链上操作，包括交易的前言和结语、权益证明机制和Aptos数字资产标准。确保Aptos框架的正确性和安全性至关重要，因为此类基础Move模块的意外行为可能导致大量资产损失或干扰网络的正常运行。因此，Aptos框架不断进行严格的测试和全面审计，为了进一步提高保证水平，我们对其安全性和正确性进行了正式验证。本文将解释我们如何使用Move Prover通过形式验证来确保Aptos框架的安全性。

Move Prover是什么？
Move Prover（简称Prover）是用于编写在Move语言中的智能合约的形式验证工具。Move语言与Prover紧密耦合并集成在一起，因为它们已经共同开发和不断演进。Move具有一种富有表现力的规范语言，旨在定义Move智能合约的预期行为。使用自动定理证明技术（例如，模理论的可满足性），Prover自动检查合约是否满足用户给出的规范，针对所有可能的程序变量赋值。如果它不满足，Prover会生成所谓的反例，即对程序变量的赋值，使得规范不成立。Prover快速可靠，可以在智能合约开发过程中常规使用，使运行Prover的体验类似于运行编译器、linters、类型检查器和其他开发工具的体验。

Move规范语言
Move规范允许开发人员指定其智能合约的属性，利用Prover保证它们按照指定的行为运行，而不会在链上增加任何运行时成本。在规范语言中，开发人员可以为函数提供前置和后置条件，包括输入参数和全局内存的条件。开发人员还可以为数据结构和全局内存的内容提供不变量。该语言还支持有界领域（如向量的索引）和有效无界领域（如内存地址和整数）的普遍和存在量词，以及一些谓词P和Q（例如，forall a: address: P(a)，exists i: u64: Q(i)，对于某些谓词P和Q）。虽然量词可以使验证问题变得不可判定并导致超时问题，但它们提供了实用的优势：它们允许更直接地形式化各种属性，提高了规范的清晰度（例如，GasCurve的数据不变量）。

例如，以下规范显示了硬币模块中extract函数的规范：

spec  
  @external  
  def extract(target: coin, balance: u64): void  
  post  
    @assert  
      balance' >= 0 and balance' <= balance  
  where  
    balance' = balance - target

预期提取函数从硬币参数中提取并返回硬币数量。上述规范是函数预期行为的数学表示。 abort_if 子句指定，如果原始硬币的值小于数量，则函数应中止。这也意味着函数在任何其他情况下都不应中止。两个确保子句指定，返回的硬币值等于数量，原始硬币的值减少数量。证明者保证函数实现满足所有输入值和所有硬币类型的规范。证明者的形式验证与测试形成对比，其中单个测试用例仅涵盖输入和硬币类型的特定实例。此外，一旦定义了证明者的规范，它就能使证明者在此后自动检查规范。这种自动化大大降低了与智能合约每次修改重复手动审计相关的成本。

我们取得了哪些成就？
从安全要求到验证：首先要强调的是，我们已经确定了Aptos框架每个模块的高级安全要求，并使用Prover进行了验证。我们与OtterSec合作，对Aptos框架进行了审计，为每个模块确定了关键安全要求。我们全面记录了这些要求，概述了它们的定义、重要性、实施方法和执行方法。执行方法包括审计、测试和在适当情况下进行形式验证。我们还与MoveBit合作，为框架的大部分内容创建了正式规范，然后使用Prover进行了验证。验证结果随后追溯到安全要求文档。

例如，下表是账户模块的高级要求的一部分：

上述行是一项关键要求，即在成功创建账户后，使用正确的默认数据对账户进行初始化，确保账户状态的正确初始化。这是通过以下方式实现的：通过create_account函数创建账户时，会验证状态并将新账户资源移动到new_address下。以下是正式规范和验证：

spec create_account(new_address: address): signer {

    …
    // This enforces high-level requirement 2:
    ensures exists<Account>(new_address);
}

上述ensures子句是create_account函数规范的一部分，该规范指定了高级安全要求。后置条件确保在函数调用结束时Account资源始终存在。

我们将高级安全要求集成到了Move文档生成过程中。因此，这些安全要求描述将自动导入Aptos框架文档中。我们还建立了一个可追溯性框架，将高级属性映射到其相应的正式规范，并将正式规范映射回高级要求，如上文规范所示。例如，可以在此处找到账户模块的高级要求。

按函数：除了高级安全要求的验证之外，我们还与MoveBit合作，从Move函数和模块中系统地推断出规范。这些规范包括每个Move函数的abort条件和后置条件以及结构和模块的不变式。

abort_if子句规范涵盖了重要类别的属性，例如访问控制检查、输入验证和状态验证。Move函数通常在设计时会在以下情况下调用时中止：(1) 没有权限的账户，(2) 输入参数超出预期范围，或(3) 意外全局状态。例如，在Aptos框架的staking config合约中，只有aptos_framework账户（即0x1）可以调用update_recurring_lockup_duration_secs。此外，输入参数new_recurring_lockup_duration_secs应该是非零值。它只能在aptos_framework地址下发布的资源StakingConfig时被调用。这些预期行为通过以下规范捕获：

spec update_recurring_lockup_duration_secs(
    aptos_framework: &signer,
    new_recurring_lockup_duration_secs: u64
){
    aborts_if signer::address_of(aptos_framework) != @aptos_framework;
    aborts_if new_recurring_lockup_duration_secs == 0;
    aborts_if !exists<StakingConfig>(@aptos_framework);
    …
}

根据此abort_if规范，Prover验证了两个方面。首先，它验证函数在满足任何条件时确实会中止。其次，Prover验证函数不会因任何其他条件而中止。这种验证很重要，因为它允许开发人员了解函数可以中止的完整条件集，因此这些规范还可以作为精确的文档。上述函数的完整规范可以在此处找到。

形式验证的影响
形式验证对Aptos框架产生了许多积极影响，为关键函数的执行提供了保证，并在新功能在Aptos网络上生产之前发现了问题。

• 在Aptos进入主网之前，我们已经验证了block::block_prologue中不存在意外的中止行为。这个函数永远不会中止，因为它与每个块一起执行，而故障可能导致整个网络崩溃。区块前导执行涉及22个不同Move模块中的96个Move函数。我们正式规范了所有这些模块，并证明了区块前导执行永远不会在意外情况下失败（或中止）。在此过程中，我们发现并修复了区块前导执行中的一些潜在算术溢出问题。该函数的完整规范可以在此处找到。
• 在代码的规范和验证过程中，我们发现了一些问题。代码已经经过单元测试和审计，因此发现的新问题相对较少。然而，形式验证确保了进一步未知问题的可能性非常低。与测试相比，形式验证不仅表明存在bug，而且证明其不存在。
• 我们已确定和定义了模块中的各种不变量，这大大增强了对它们的行为和安全影响的理解。这种更深入的理解随后指导了对几个模块的改进和重构。
• 规范是自动生成的Aptos框架文档的组成部分，为每个函数和模块提供了清晰详细的预期行为说明（例如，coin::register的规范）。这种精确的安全要求文档对于持续维护和确保质量保证至关重要。
• 最后，将证明者集成到持续集成（CI）测试过程中显著降低了每次合同修改后频繁进行审计的需要。因此，形式验证有效地减少了与审计相关的时间和成本。

结论与未来计划
为了确保Aptos Framework的最高质量和安全性，我们采用了一种结合手动审计、测试和自动化形式验证的方法。与OtterSec合作，对框架进行了审计，并提出了高层次的安全要求，并进行了记录。与MoveBit合作，逐个功能地对框架进行了规范，直到大多数高层次的安全要求最终得到正式验证。在工作中，我们还发现了Move Prover中的一些bug和可用性问题，这些问题已经得到修复，对Aptos Move的所有用户都有益。

这项综合工作为区块链行业及其他行业的Aptos Framework提供了无与伦比的质量保证。展望未来，Aptos Labs致力于维护和发展验证工作，同时改进Prover本身，使其可供整个Aptos生态系统的构建者和审计人员使用，推动空间内软件质量的边界。