MoveBit(莫比安全)作为专注于服务Move生态的安全公司,近期和 Aptos 合作开展了 Aptos Framework 的形式化验证工作。Aptos 是一个顶级公链,其愿景是将 Web3 带入主流,并获得顶级资本的投资,而其底层基础代码库 Aptos Framework 是 Aptos 公链上的通用 Move 库,包括了账户、NFT、Token 等通用标准,是生态建设的重要基础设施。

Aptos Framework 的安全性是 Aptos 上开发各种 Move 项目应用安全的基础。在此形式化验证工作之前,MoveBit 团队全面了解分析了 Aptos Framework 的开发资源和框架架构,并和 Aptos Team 合作开启了基于 Move Prover 的形式化验证。

以下是 MoveBit 团队对 Aptos Framework 形式化验证后的代码提交示例:

  1. 添加了模块帐户和币的规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5237
  2. 添加了模块和 aptos_account 和 state_storage 的规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5478
  3. 更新了 consensus_config 的规范,添加了 transaction_fee 和 transaction_validation 的规范。更新了重新配置和权益以及 storage_gas 的规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5549
  4. 添加了 Aggregator & AggregatorFactory & OptionalAggregator & StakingConfig & Version & Event & Guid & Timestamp 规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5653
  5. 添加了模块 gas_schedule & aptos_coin & chain_id & chain_status 的规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5771
什么是 Move Prover 形式化验证?
形式化验证是一种使用严格的数学方法来描述行为和推理计算机系统的正确性的技术。现在已经广泛应用在芯片验证、航空航天、操作系统、编译器等对正确性要求高的领域。
部署在区块链上的智能合约操作着各种数字资产,它们的安全性也十分关键。Move Prover就是为尽可能防止 Move 语言编写的智能合约中的错误而设计。用户可以使用 Move 规范语言指定智能合约的功能属性,然后使用 Move Prover 静态地检查它们。
简单地说,Move 文件中可以分两种:
一部分是程序代码,这是我们多数人最熟悉的部分。它用 Move 程序语言写成。我们用它定义数据类型、函数。
另一部分是形式规范。它是可选的,用 Move 规范语言写成。我们用它说明程序代码应该满足怎样的性质,比如描述函数的行为和全局的属性。
MoveBit 主要根据代码逻辑进行形式规范验证,写完规范后调用 Move Prover,Move Prover会按照写好的规范去验证 Aptos Framework 的 Move 程序有没有满足这些要求,帮助 Aptos 的开发人员在开发阶段尽早发现潜在的问题, 并让其用户可以尽快将已经验证过的程序运用到产品当中。 
本文将对此形式化验证过程中的关键步骤进行展示:
  1. withdraw()  是 aptos-framework coin模块下的一个函数,该函数作用是从签名账户中提取指定数量的代币,并将代币返回。MoveBit为aptos提供了形式化验证代码。
    MoveBit 对 Aptos Framework开展形式化验证
  2. 我们验证了`withdraw`函数的功能性质及中止条件.

    `balance` `account`账户下(某种)代币的余额,`amount`为要取出的代币余额, 我们可以看到,该函数有三种中止(abort)的情况:

    1. 该账户下不存在`CoinType`类型的代币。

    2. 该账户下余额不足

    3. 该账户被冻结

    我们预期执行完该函数后,`account`账户下的余额应该为`balance - amount`,且返回一个金额为`amount`的代币。如果没有达到我们的预期,那么prover会提示我们条件没有满足。

    MoveBit 对 Aptos Framework开展形式化验证
  3. deposit函数作用是将代币余额存入接收者的账户。MoveBit 对 Aptos Framework开展形式化验证
  4. 该函数有两种中止的情况:

    1. 接收者的账户被冻结

    2. 接收者的账户下不存在CoinStore<CoinType>资源

    我们预期执行完该函数后接收者账户的余额等于接受前的余额加上转入的金额。且返回一个金额为amount的代币。

    MoveBit 对 Aptos Framework开展形式化验证
构建Aptos生态安全
Aptos 极其重视生态安全的建设,MoveBit 作为专注于 Move 生态安全的安全审计公司,除了对 Aptos Framework 展开形式化验证,与 Aptos 协作了 MoveVM 的安全审计,并且与 Apots 生态上的 MoveDID, Token Pocket, Starswap,OminBTC,Pontem 等项目达成了合作,MoveBit 将会持续为 Aptos 生态安全保驾护航

关于MoveBit

MoveBit(莫比安全)团队是一家服务于 Move 生态的安全公司,其愿景是让 Move 生态成为最安全的 Web3 生态系统。MoveBit 团队由学术界安全大牛和企业界安全领军人物组成,具有10年的安全经验,在NDSSCCS 等顶级国际安全学术会议上发表安全研究成果。团队是 Move 生态最早期的贡献者,与 Move 开发者共同制定安全 Move 应用的标准。MoveBit 已经陆续与全球多家知名交易所、公链项目合作,为合作伙伴提供安全审计服务。

 MoveBit 社交媒体平台:

官方网址:https://www.movebit.xyz/

Twitterhttps://twitter.com/MoveBit_

Mediumhttps://movebit.medium.com/