Securing the Aptos Framework with Formal Verification

Author:Aptos Labs, MoveBit, and OtterSec.

The Aptos framework undergoes ongoing rigorous testing and comprehensive audits. To further increase the level of assurance, we formally validated its security and correctness.

We worked with OtterSec to audit the Aptos framework and identify critical security requirements for each module.
We worked with MoveBit to create a formal specification for much of the framework, which was then validated using Move Prover.
This combined effort has given the Aptos framework an unparalleled level of quality assurance in the blockchain industry and beyond.

- introduction
- What is Move Prover?
- Move regulates language.
- What have we achieved?
- Effects of formal validation.
- Conclusions and future plans.

summary
The Aptos Framework is a collection of Move smart contract modules used to define the standards and common on-chain operations of the Aptos network, including transaction preambles and conjunctions, proof-of-interest mechanisms, and the Aptos Digital Asset Standard. Ensuring the correctness and security of the Aptos framework is critical, as unintended behavior of such underlying Move modules can result in the loss of large amounts of assets or disrupt the normal operation of the network. As a result, the Aptos framework is continually subjected to rigorous testing and comprehensive audits, and to further increase the level of assurance, we have formally validated its security and correctness. This article explains how we use Move Prover to ensure the security of the Aptos framework through formal validation.

What is Move Prover?
Move Prover (Prover for short) is a formal verification tool for writing smart contracts in the Move language, which is tightly coupled and integrated with Prover as they have been co-developed and evolved.Move has an expressive specification language designed to define the expected behavior of Move smart contracts. Using automatic theorem proving techniques (e.g., modulo theoretic satisfiability), Prover automatically checks whether the contract satisfies the specification given by the user, assigning values to it for all possible program variables. If it does not, Prover generates so-called counterexamples, i.e., assignments to program variables that make the specification unsatisfiable.Prover is fast and reliable enough to be used routinely during smart contract development, making the experience of running Prover similar to that of running compilers, linters, type checkers, and other development tools.

Move normative language
The Move specification allows developers to specify the properties of their smart contracts, using Prover to ensure that they run according to the specified behavior without adding any runtime cost to the chain. In the specification language, developers can provide pre- and post-conditions for functions, both for input parameters and for global memory. Developers can also provide invariants for data structures and the contents of global memory. The language also supports universal and existential quantifiers for bounded domains (e.g., indexes of vectors) and valid unbounded domains (e.g., memory addresses and integers), as well as some predicates P and Q (e.g., forall a: address: P(a), exists i: u64: Q(i), for some predicates P and Q). While quantifiers can make the verification problem undecidable and lead to timeout problems, they offer practical advantages: they allow for a more direct formalization of various properties, improving the clarity of the specification (e.g., data invariants for GasCurve).

For example, the following specification shows the specification of the extract function in the Coin module:

spec
  @external
  def extract(target: coin, balance: u64): void
  post
    @assert
      balance' >= 0 and balance' <= balance
  where
    balance' = balance - target

The expected extract function extracts and returns the number of coins from the coin argument. The above specification is a mathematical representation of the function's expected behavior. The abort_if clause specifies that the function should abort if the value of the original coin is less than the quantity. This also means that the function should not abort in any other case. The two ensure clauses specify that the value of the coin returned is equal to the quantity and the value of the original coin decreases by the quantity. The prover ensures that the function implementation satisfies the specification for all input values and all coin types. The formal verification of the provers is contrasted with testing, where a single test case covers only specific instances of the inputs and coin types. Furthermore, once the specification of the prover is defined, it enables the prover to automatically check the specification thereafter. This automation significantly reduces the costs associated with repeating manual audits for each modification of a smart contract.

What have we achieved?
From Security Requirements to Validation: The first thing to emphasize is that we have identified high-level security requirements for each module of the Aptos Framework and validated them using Prover. Working with OtterSec, we conducted an audit of the Aptos framework and identified critical security requirements for each module. We fully documented these requirements, outlining their definitions, significance, implementation methods, and enforcement methods. The implementation methodology included auditing, testing and, where appropriate, formal validation. We also worked with MoveBit to create a formal specification for much of the framework, which was then validated using Prover. The results of the validation were then traced back to the security requirements document.

For example, the following table is part of the high-level requirements for the Accounts module:

The above line is a key requirement to initialize the account with the correct default data to ensure that the account state is correctly initialized after the account is successfully created. This is accomplished in the following way: when an account is created via the create_account function, the state is validated and the new account resource is moved under new_address. The following is the formal specification and validation:

spec create_account(new_address: address): signer {

    ...
    // This enforces high-level requirement 2.
    ensures exists(new_address); ... // This enforces high-level requirement 2.
}

The above ensures clause is part of the create_account function specification, which specifies high-level security requirements. The postcondition ensures that the Account resource is always present at the end of the function call.

We have integrated advanced security requirements into the Move document generation process. As a result, these security requirement descriptions are automatically imported into the Aptos Framework documentation. We also built a traceability framework that maps high-level attributes to their corresponding formal specifications and maps the formal specifications back to the high-level requirements, as shown in the specification above. For example, the high-level requirements for the Accounts module can be found here.

By function: in addition to the verification of high-level security requirements, we worked with MoveBit to systematically infer specifications from Move functions and modules. These specifications include abort conditions and postconditions for each Move function as well as invariants for structures and modules.

The abort_if clause specification covers important classes of attributes such as access control checking, input validation, and state validation.Move functions are typically designed to abort when called on (1) an account with no permissions, (2) an input parameter out of the expected range, or (3) an unexpected global state. For example, in the Aptos Framework staking config contract, only the aptos_framework account (i.e., 0x1) can call update_recurring_lockup_duration_secs. in addition, the input parameter new_recurring_lockup_ duration_secs should have a non-zero value. It can only be called when the resource StakingConfig is published under the aptos_framework address. These expected behaviors are captured by the following specification:

spec update_recurring_lockup_duration_secs(
    new_recurring_lockup_duration_secs: u64
    new_recurring_lockup_duration_secs: u64
){
    aborts_if signer::address_of(aptos_framework) ! = @aptos_framework;
    aborts_if new_recurring_lockup_duration_secs == 0;
    aborts_if !exists(@aptos_framework);
    ...
}

According to this abort_if specification, Prover verifies two things. First, it verifies that the function does abort when any condition is met. Second, Prover verifies that the function does not abort for any other condition. This validation is important because it allows the developer to understand the complete set of conditions under which the function can abort, so these specifications also serve as precise documentation. The full specifications for the above functions can be found in thehere (literary)Find.

Impact of formal validation
Formal validation has had a number of positive impacts on the Aptos framework, providing assurance that key functions are executing and identifying issues before new functionality is produced on the Aptos network.

• We have verified that there is no unexpected abort behavior in block::block_prologue before Aptos enters the main network. This function never aborts because it executes with each block, and a failure could cause the entire network to crash. Block prelogue execution involves 96 Move functions in 22 different Move modules. We formally standardize all of these modules and prove that block-leading execution never fails (or aborts) under unexpected circumstances. In the process, we identified and fixed a number of potential arithmetic overflow problems in block leading execution. The full specification of this function can be found in thehere (literary)Find.
• During the specification and validation of the code, we identified a number of issues. The code has been unit tested and audited, so relatively few new issues have been identified. However, formal validation ensures that the likelihood of further unknown issues is very low. In contrast to testing, formal validation not only indicates the presence of a bug, but proves its absence.
• We have identified and defined various invariants in the modules, which has greatly enhanced the understanding of their behavior and security implications. This deeper understanding has subsequently guided the improvement and refactoring of several modules.
• The specification is an integral part of the automatically generated Aptos Framework documentation, providing a clear and detailed description of the expected behavior for each function and module (e.g., the specification for coin::register). This precise documentation of security requirements is essential for ongoing maintenance and to ensure quality assurance.
• Finally, integrating the provers into the Continuous Integration (CI) testing process significantly reduces the need for frequent audits after each contract modification. As a result, formal validation effectively reduces the time and cost associated with audits.

Conclusions and future plans
In order to ensure the highest quality and security of the Aptos Framework, a combination of manual auditing, testing and automated formal validation was utilized. Working with OtterSec, the framework was audited and high level security requirements were made and documented. Working with MoveBit, the framework was standardized on a function-by-function basis until most of the high-level security requirements were finally formally verified. In the course of our work, we also identified a number of bugs and usability issues in Move Prover that have been fixed to the benefit of all users of Aptos Move.

This comprehensive work provides unparalleled quality assurance for the Aptos Framework for the blockchain industry and beyond. Going forward, Aptos Labs is committed to maintaining and evolving the validation effort, as well as improving the Prover itself so that it is available to builders and auditors across the Aptos ecosystem, pushing the boundaries of software quality in the space.