/ Web3完整软件栈先进形式化验证/
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基础架构，最终为开发者和用户构建一个更加坚实可信的平台。
