MoveBit (Mobi Security), a security company focusing on serving the Move Ecosystem, has recently started the Formal Verification of Aptos Framework. Aptos is a decentralized public blockchain, Its vision is to promote the development of Web3 and obtain recognition from the market. Its underlying code base, Aptos Framework, is an essential infrastructure for ecosystem construction on the Aptos blockchain, including account, NFT, Token, and other common standards. The security of Aptos Framework is the basis for developing various Move project application security on Aptos. Before Formal Verification, the MoveBit team had a comprehensive understanding of the development resources of Aptos Framework, and collab with Aptos Team to start the formal verification using Move Prover.
The following are examples of the code commit after Formal Verification to Aptos Framework by the MoveBit team:
Added specs for module account & coin.
More Details: https://github.com/aptos-labs/aptos-core/pull/5237
Added specs for module block & aptos_account & state_storage.
More Details: https://github.com/aptos-labs/aptos-core/pull/5478
Updated specs for consensus_config, added spec for transaction_fee & transaction_validation.
Updated specs for reconfiguration and stake and storage_gas.
More Details: https://github.com/aptos-labs/aptos-core/pull/5549
Added specs for Aggregator & AggregatorFactory & OptionalAggregator & StakingConfig & Version & Event & Guide & Timestamp.
More Details: https://github.com/aptos-labs/aptos-core/pull/5653
Added specs for module gas_schedule & aptos_coin & chain_id & chain_status.
More Details: https://github.com/aptos-labs/aptos-core/pull/5771
What is the Move Prover Formal Verification?
Formal Verification is a technique that uses rigorous mathematical methods to describe the behavior and reason about the correctness of computer systems. It has been used in operating systems, compilers, and other fields requiring high accuracy.
Smart contracts deployed on the blockchain manipulate various digital assets, and their correctness is also critical. Move Prover (MVP) is designed to prevent errors in smart contracts written in the Move language. Users can specify the functional properties of smart contracts using the Move Specification Language (MSL), and then use Move Prover to automatically and statically check them.
Briefly, there can be two components in a Move file:
One part is program code, which most of us are familiar with. It is written in the Move programming language. We use it to define data types, and functions.
The other part is the formal specification. It is optional and written in the Move specification language. We use it to describe what properties the program code should satisfy. For example, describe the behavior of a function.
MoveBit will perform formal specification verification according to the code logic. After writing the specification (Specification) and invoking Move Prover, it will verify whether the Move program of the Aptos Framework meets these requirements according to the written specification and help Aptos developers as soon as possible in the development stage. Discover potential problems and allow its users to apply proven procedures to products as quickly as possible.
This article will show the key steps in this formal verification process：
- `withdraw` is a function under the Aptos-framework coin module, which is used to withdraw a specified number of tokens from the signature account, and return tokens. MoveBit provides Formal Verification code for Aptos.
- We verified the functional properties and termination conditions of the `withdraw` function.
`balance` is the balance of (some kind of) token under the `account` account, and `amount` is the balance of the token to be withdrawn. We can see that this function has three abort situations:
1. There is no token of the `CoinType` type under this account.
2. The account balance is insufficient.
3. The account is frozen.
We expect that after executing this function, the balance under the `account` account should be `balance — amount`, and return a token with an amount of `amount`. If our expectations are not met, prover will prompt us that the conditions are not met.
- The deposit function is to deposit the token balance into the receiver’s account
- There are two cases where this function terminates:
The receiver account is frozen
The CoinStore<CoinType> resource does not exist under the receiver account
We expect that after executing this function, the balance of the receiver account will be equal to the balance before acceptance plus the amount transferred. And return a token with an amount of ‘amount’.
Securing Aptos Ecosystem
Aptos attaches great importance to ecosystem security. MoveBit, as a security audit company focusing on Move security, in addition to leveraging formal verification to Aptos Framework, also cooperates with Aptos in the security audit of MoveVM and reached in-depth audit cooperation with many projects which are built on Aptos ecosystem, such as MoveDID, Token Pocket, Starswap, etc. Generally speaking, MoveBit will continue to escort the ecological security of Aptos.
About MoveBit
MoveBit is a security company for the Move ecosystem with a vision to make the Move ecosystem the most secure Web3 destination. The MoveBit team is composed of security leaders from academia and enterprise with 10 years of security experience. The team was one of the earliest contributors to the Move ecosystem, working with Move developers to set the standard for secure Move applications.
MoveBit Social Media Platforms:
Official Website | Twitter | Medium | GitHub
