详解对Cosmos SDK标准模块的形式化验证

/ Web3完整软件栈先进形式化验证/

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

Cosmos SDK是什么?

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

详解对Cosmos SDK标准模块的形式化验证

来源: https://golden.com/wiki/Tendermint-4AP8KX8Bank模块

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

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

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

详解对Cosmos SDK标准模块的形式化验证

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

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

详解对Cosmos SDK标准模块的形式化验证

这个结构很简单,我们采用Coq(我们的建模和形式化验证语言)作如下定义:

详解对Cosmos SDK标准模块的形式化验证

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

详解对Cosmos SDK标准模块的形式化验证

该引理证明了一个基本的不变性:两个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`作为记录。

详解对Cosmos SDK标准模块的形式化验证

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规范语言中的描述如下:

详解对Cosmos SDK标准模块的形式化验证

关于其他性质的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基础架构,最终为开发者和用户构建一个更加坚实可信的平台。