介绍形式化验证 Cosmos SDK Bank 模块的具体步骤，以及一些验证结果。

撰文：CertiK

CertiK 最近发布了一份关于 Cosmos SDK Bank 模块的先进形式化验证报告，据我们所知，这是针对 Cosmos SDK 形式化验证的首次成功尝试。形式化验证是一项运用数学逻辑来确保系统符合规范，使其在所有可能的输入和条件下都如预期表现的技术。在本文中，我们将介绍形式化验证 Cosmos SDK Bank 模块的具体步骤，以及一些验证结果。

Cosmos SDK 是什么？

Cosmos 软件开发工具包（简称 SDK）是一个能让开发人员构建自定义区块链应用的框架。利用 Cosmos SDK，开发者可以轻松启动自己的 Layer 1 区块链，不用操心从共识层到应用层的设计和实现。Cosmos SDK 提供了任何链都可直接导入和使用的标准核心模块，如 staking、auth、gov 和 mint 模块。

来源: https://golden.com/wiki/Tendermint-4AP8KX8

Bank 模块

Cosmos SDK 中的 bank 模块主管所有与代币管理相关的功能，比如原生代币的转移。发送代币需要满足诸多限制和条件，比如账户要有充足的可用代币，而不包括那些已质押、锁定或正在解绑的代币。在 staking 和 auth 等模块的支持下，bank 模块管理代币发送的全过程。尽管 bank 模块需要依赖于其他几个模块，但由于它们不在本次形式化验证的范围内，所以我们对其功能作了一些假设，以简化流程。

SDK 的 bank 模块由若干子模块构成，其中包括 keeper 和 types，它们是定义模块行为和数据类型的核心组件。我们将重点关注 keeper 子模块，因为它涵盖了模块的主要功能和特性。

keeper 子模块有两个关键组成部分：view 和 send。view keeper 负责管理账户和余额，而 send keeper 则负责更改账户余额，如转账和质押已锁定或未锁定的代币。bank 模块的流程如下图所示，箭头表示从组件到功能或 Keeper 的方向。

来源: https://docs.cosmos.network/v0.46/building-modules/msg-services.html

验证方法

如前文所述，本次验证的范围仅限于 bank 模块。验证开始前，我们首先对 bank 模块内的数据类型制定其形式化规范。例如，bank 模块中有一个代币数据结构，其包含 string 类型的面额和 big.Int 类型的金额，在源代码中定义如下：

这个结构很简单，我们采用 Coq（我们的建模和形式化验证语言）作如下定义：

基于这个定义，我们首先证明关于 coin 基本操作的一些性质，以为 bank 模块的功能完整性打下基础，因为其需要经常修改和操作 coin 类型。例如：

该引理证明了一个基本的不变性：两个 coin 相减不会改变其面额，也不会导致余额为负。

与前述例子类似，对每次状态转换的底层组件都在 Coq 中进行了建模，这些组件包括 KV Store、GasMeter、Error Handling 和 Context。

数据类型的详细规范及其验证请见：https://github.com/CertiKProject/cosmos-sdk-fv/tree/master/coq_proofs/perennial/src/cosmos_sdk_proofs

对 keeper 建模

在完成基础组件的建模后，我们可以对 bank 模块的核心 keeper 进行建模，以描述模块的功能。bank keeper 有两个接口，一个用于代币数据的只读访问，另一个用于代币的转移和供应维护。

View keeper 负责处理账户余额的只读访问，内含四个用于计算账户余额的函数：

1. `GetBalance`：通过地址查询特定面额的账户余额。它考虑两种情况：空字节序列和非空字节序列。形式化验证确保`GetBalance`函数在这两种情况下都能产生正确的结果。

2. `LockedCoins`：返回某地址所对应账户的所有不可消费代币。由于时间限制，我们对一些来自 auth 模块的实现做了假设。

3. `GetAllBalances`：返回指定地址下的所有账户余额。

4. `GetAccountsBalances`：从存储中返回所有账户余额，并以字段`BAddress`和`BCoins`作为记录。

Send 管理器负责处理代币转账和供应。在转账过程中，它会保持代币的供应量，因此不会有新的代币被铸造。

1. `SetBalance`：通过地址为账户设置代币余额。此函数考虑两种情况：设置为零的余额和设置为非零的余额。在这两种情况下，SetBalance 的正确性都得到了证明。

2. `subUnlockedCoin`：从某地址中扣除指定金额（代币）。递归函数`subUnlockedCoins`对一组代币执行同样的操作。这些函数的相关属性被视作公理假设。

3. `addCoin`：为某地址增加指定金额（代币）。递归函数`addCoins`对一组代币执行相同的操作。这些函数的相关属性被视作公理假设。

4. `SendCoins`：从一个账户地址向另一个账户地址发送金额，使两个地址的金都得到更新。如果接收方不存在，将为其新建账户。

利用以上核心组件的模型，我们可以开始进行验证了。

验证过程

我们的验证是通过形式化描述这些函数的不变性质、并在辅助证明系统中进行证明来完成的，主要关注点是「View Keeper」和「Send Keeper」的核心功能。

例如，规范和引理`setBalance_ok`证明了`BaseSendKeeper`模块的`setBalance`函数的正确性，具体证明了以下性质：

1. 当`send.setBalance`返回「Ok」状态时，存在一个`newMultiStore`，此时更新后的环境 `uctx`是通过更新`newMultiStore`，从原来的旧环境 `ctx`衍生而来。

2. 被设置的余额是有效代币（它具有系统中代币所需的属性）。

3. `setBalance_prop`的关系保持，确保函数以符合预期的方式在`newMultiStore`中进行余额更新，并生成更新后的环境`uctx`。

4. 余额设置完成后，使用账户地址`addr`和面额`balance.(Denom)`在更新后的环境`uctx`上调用`view.GetBalance`，将会返回`send.setBalance`所设置的相同余额。

这些性质在 Coq 规范语言中的描述如下：

关于其他性质的 Coq 代码，访问：https://skynet.certik.com/projects/cosmos。

未来的工作

本次验证的基础建立在若干假设和公理之上，我们可以对其进行更深入的核实，以扩大验证的范围。未来工作的重点包括以下领域：

1. 假设的验证：目前的验证于依赖于一系列的假设作为证明的基础。未来可以对这些假设进行验证，以确保它们准确地反映系统的预期行为和性质。

2. Auth 模块的验证：该模块负责管理账户数据以及签名机制，是 Cosmos SDK 的核心组件。在未来可以对其进行全面的形式化验证，保证模块实现及与其他模块的交互准确无误。

3. 关于委托、铸币和销币的更多定理：拓展验证范围，引入更多关于委托、铸币和销币的定理，将有助于更全面地了解系统的运行机制。这些定理可以与 auth 模块的验证相结合，以确保系统的整体一致性和正确性。

4. 拓展整个 Cosmos SDK 基础架构：现阶段的验证工作主要集中在 bank 模块及其相关组件。在未来可以将形式化验证的过程扩展到整个 Cosmos SDK 基础架构，从而增强平台的整体准确性、安全性和稳定性，为开发者和用户提供一个更稳固、更可靠的环境。

5. 与其他模块进行整合：由于 Cosmos SDK 包括各种相互连接的模块，探究它们之间的交互和依赖关系是十分有益的。这需要验证模块之间交互的正确性，并确保某个模块的任何更改都不会对其他模块产生不利影响。

6. 激励机制的建模与验证：Cosmos SDK 也整合了如 staking 和奖励分发等激励机制。未来的研究会对这些机制进行建模和验证，以确保其正确性，并与预期的经济激励保持一致。

本文展示了对 Cosmos SDKbank 模块进行先进形式化验证的首个成功案例，为区块链生态系统的安全性和可靠性基础做了有效的工作。未来的工作将在这一成果的基础上进行扩展，通过验证假设、验证其他模块，并涵盖整个 Cosmos SDK 基础架构，最终为开发者和用户构建一个更加坚实可信的平台。