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 形式化验证后的代码提交示例:
-
添加了模块帐户和币的规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5237 -
添加了模块和 aptos_account 和 state_storage 的规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5478 -
更新了 consensus_config 的规范,添加了 transaction_fee 和 transaction_validation 的规范。更新了重新配置和权益以及 storage_gas 的规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5549 -
添加了 Aggregator & AggregatorFactory & OptionalAggregator & StakingConfig & Version & Event & Guid & Timestamp 规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5653 -
添加了模块 gas_schedule & aptos_coin & chain_id & chain_status 的规范。详细链接:https://github.com/aptos-labs/aptos-core/pull/5771
-
withdraw() 是 aptos-framework coin模块下的一个函数,该函数作用是从签名账户中提取指定数量的代币,并将代币返回。MoveBit为aptos提供了形式化验证代码。 -
我们验证了`withdraw`函数的功能性质及中止条件.
`balance` 是`account`账户下(某种)代币的余额,`amount`为要取出的代币余额, 我们可以看到,该函数有三种中止(abort)的情况:
1. 该账户下不存在`CoinType`类型的代币。
2. 该账户下余额不足
3. 该账户被冻结
我们预期执行完该函数后,`account`账户下的余额应该为`balance - amount`,且返回一个金额为`amount`的代币。如果没有达到我们的预期,那么prover会提示我们条件没有满足。
- deposit函数作用是将代币余额存入接收者的账户。
-
该函数有两种中止的情况:
1. 接收者的账户被冻结
2. 接收者的账户下不存在CoinStore<CoinType>资源
我们预期执行完该函数后接收者账户的余额等于接受前的余额加上转入的金额。且返回一个金额为amount的代币。
关于MoveBit
MoveBit(莫比安全)团队是一家服务于 Move 生态的安全公司,其愿景是让 Move 生态成为最安全的 Web3 生态系统。MoveBit 团队由学术界安全大牛和企业界安全领军人物组成,具有10年的安全经验,在NDSS、CCS 等顶级国际安全学术会议上发表安全研究成果。团队是 Move 生态最早期的贡献者,与 Move 开发者共同制定安全 Move 应用的标准。MoveBit 已经陆续与全球多家知名交易所、公链项目合作,为合作伙伴提供安全审计服务。
MoveBit 社交媒体平台:
官方网址:https://www.movebit.xyz/
Twitter:https://twitter.com/MoveBit_
Medium:https://movebit.medium.com/