Move硬核研究系列 | 智能合约的重要变革，如何使用Move Prover？

Move 是为操作数字资产而生的智能合约语言，其设计初衷是为了从安全角度出发进行合约开发。为了保证其安全性，Move从语言层面进行了大量的安全设计，具体可见前文：

Beosin | 从安全角度看Move语言（上）

Beosin | 从安全角度看Move语言（下）

此外，为了方便开发人员进行安全验证，Move 语言还提供了 Move 的形式化验证工具：Move Prover。目前Beosin审计已将 Move Prover 集成到 Move 的审计服务中。Besoin 安全审计服务在对 Move 合约进行审计时，主要步骤如下：

•熟悉项目架构、目的和使用的框架

•智能合约代码review和人工走查，找逻辑漏洞

•彻查数学运算相关的漏洞

•测试覆盖率审查（aptos move test）

•核心功能的链上测试（aptos-cli）

•智能合约的部署（aptos devnet）

•核心代码的形式化验证（move prover）

本文主要介绍如何使用Move Prover。

Move Prover可以形式验证 Move 模块的特征，并且足够高效，可用于持续集成测试。形式验证方式是为程序提供一个规范，然后根据符号输入对该规范进行检查，使开发者能够证明代码在所有可能的输入中都遵循该规范。

#安装  

#应用场景

1 权限控制

在规范层面上强制执行明确的访问控制策略可以有效防止权限滥用。

例如，在std::offer中，我们可以看到，当接收者不在白名单中，该函数会被终止。

2 数据的不变式

形式验证提供了最好的环境来验证某些变量或资源不超过预期的界限。如以下例子可以保证(target)的balance不超过MAX_BALANCE。

我们甚至可以编写一个全局的数据不变性来保证在程序的任何一个地方，balance都不会超过MAX_BALANCE。

3 资金守恒

验证资金守恒可以确保复杂的Defi协议中的安全问题。例如通过AMM进行交换，如果资金池中一方的资金没有增加，则另一方不可能减少。也就是说没有“免费”的钱。如下图示例。

其他的资金守恒包括借贷协议应该在一系列的存款、借款和取款指令后，始终有充分的抵押；订单簿在订单下达后又被取消的情况下，不应该出现账本变化等等。

Move 审计服务与Move审计项

Beosin安全团队正式推出针对Move智能合约的安全审计服务，旨在提前发现并协助项目方修复项目中的安全风险，保障用户与项目方的资产安全。其主要安全审计项包括：

•溢出漏洞

•重放攻击

•不安全的随机数

•交易顺序依赖

•拒绝服务

•访问控制

•权限不当

•变量覆盖

•业务设计

•业务实现

•可操纵的代币价格

•套利攻击

•Gas优化

•第三方模块安全

•能力安全

•资源安全

•升级安全

•中心化风险

目前Move仍处于发展阶段，Move生态距离成熟尚有一定距离。Move相关的开发者经验欠缺，真正能够熟练开发Move合约的不多，因此更容易出现一些业务层面的漏洞。这需要开发者在Move合约的设计和开发过程中对Move语言的特性以及业务有比较熟练的程度，才可能减少安全漏洞的出现。

下一篇我们将会介绍Move程序审计中容易出现的漏洞点以及例子。

Beosin作为一家总部位于新加坡的区块链安全公司，业务涵盖项目上线前的代码安全审计、项目运行时的安全风险监控、预警与阻断、虚拟货币被盗资产追回、安全合规KYT/AML等“一站式”区块链安全产品+服务，目前已为全球2000多个区块链企业提供安全技术服务，审计智能合约超过2500份，保护客户资产高达5000多亿美元。欢迎点击公众号留言框，与我们联系。