by Aptos Labs, MoveBit, and OtterSec

The Aptos Framework has continuously undergone rigorous testing and comprehensive auditing. To further increase the level of assurance, we have formally verified its security and correctness.

• We worked with MoveBit in creating formal specifications for large parts of the Framework, which were then verified with the Move Prover.
• We worked with OtterSec in auditing the Aptos Framework and identifying critical security requirements for each module.
• This combined effort gives the Aptos Framework an unmatched level of quality assurance in the blockchain industry and beyond.

Introduction

The Aptos Framework is the collection of Move smart contract modules that define standard and common on-chain actions for the Aptos Network, including the prologue and epilogue of transactions, the staking mechanism, and the Aptos Digital Asset Standard. It is imperative to ensure the correctness and security of the Aptos Framework because the unexpected behavior of such foundational Move modules could lead to substantial asset loss or disrupt the normal functioning of the network. For this reason, the Aptos Framework has continuously undergone rigorous testing and comprehensive auditing, and to further increase the level of assurance, we have f_ormally verified its security and correctness._ This article will explain how we have secured the Aptos Framework through formal verification using the Move Prover.

What is the Move Prover?

The Move Prover (Prover for short) is a formal verification tool for smart contracts that are written in the Move language. The Move language is tightly coupled and integrated with the Prover because they have been developed and are evolving together. Move features an expressive specification language designed to define the intended behaviors of a Move smart contract. Employing an automatic theorem-proving technology (e.g., satisfiability modulo theories), the Prover automatically checks whether the contract satisfies the user-given specification for all possible program variable assignments. If it does not, the Prover generates a so-called counter-example, that is an assignment to program variables such that the specification does not hold. The Prover is fast and reliable, and can be used routinely during smart contract development, making the experience of running the Prover similar to the experience of running compilers, linters, type checkers, and other development tools.

The Move Specification Language

The Move specification allows developers to specify the properties of their smart contracts, leveraging the Prover to guarantee they behave as specified without adding any runtime cost on-chain. In the specification language, developers can provide pre and post-conditions for functions, which include conditions over input parameters and global memory. Developers can also provide invariants over data structures as well as the contents of the global memory. The language also supports universal and existential quantification over bounded domains, such as the indices of a vector, as well as effectively unbounded domains, such as memory addresses and integers (e.g., forall a: address: P(a), and exists i: u64: Q(i), for some predicates P and Q). While quantifiers can render the verification problem undecidable and lead to timeout issues, they offer a practical advantage: they allow for a more direct formalization of various properties, enhancing the clarity of specifications (e.g., the data invariant of GasCurve).

As an example, the spec below shows the specification of the extract function in the coin module:

spec extract<CoinType>(  
    coin: &mut Coin<CoinType>,  
    amount: u64  
): Coin<CoinType> {  
    aborts_if coin.value < amount;  
    ensures result.value == amount;  
    ensures coin.value == old(coin.value) - amount;  
}

The extract function is expected to extract and return the amount of coins from the coin parameter. The specification above is the mathematical representation of the expected behavior of the function. The aborts_if clause specifies that the function should abort if the value of the original coin is less than the amount. It also implies that the function should not abort in any other case. The two ensures clauses specify that the value of the returned coin is equal to amount and the value of the original coin decreases by amount. The Prover guarantees that the function implementation satisfies this specification for all input values and all coin types. The Prover’s formal verification contrasts with testing, where a single test case only covers a specific instance of input and coin type. Moreover, once a specification for the Prover is defined, it enables the Prover to automatically check the specification thereafter. This automation significantly reduces the costs associated with repetitive manual audits for every modification of the smart contract.

What have we Achieved?

From Security Requirement to Verification: The first thing to highlight is that we have identified the high-level security requirements of each module of the Aptos framework and verified them using the Prover. We collaborated with OtterSec in auditing the Aptos Framework and identifying critical security requirements for each module. We thoroughly documented these requirements, outlining their definition, criticality, implementation approach, and methods of enforcement. The enforcement methods include audit, test, and, where appropriate, formal verification. We also collaborated with MoveBit in creating formal specifications for large parts of the Framework, which were then verified with the Prover. The verification result is then tracked back to the safety requirement documentation.

For example, the table below is part of the high-level requirements for the account module:

The row above is a critical requirement that, after successfully creating an account, it is initialized with the correct default data, ensuring the proper initialization of the account state. This is implemented in a way that creating an account via the create_account function validates the state and moves a new account resource under new_address. This is formally specified and verified as follows:

spec create_account(new_address: address): signer {  
    …  
    // This enforces high-level requirement 2:  
    ensures exists<Account>(new_address);  
}

The ensure clause above is part of the specification of the create_account function that specifies the high-level security requirement. The post-condition ensures that the Account resource always exists at the end of the function call.

We have integrated the high-level security requirements into the Move documentation generation process. Thus, these security requirement descriptions are imported into the Aptos Framework documentation automatically. We also established a traceability framework that maps high-level properties to their corresponding formal specifications, and maps the formal specifications back to the high-level requirement, as shown in the specification above . For example, the high-level requirements of the account module can be found here.

Function by function: In addition to the high-level security requirement verification, we have also systematically inferred the specifications from the Move functions and modules, collaborating with MoveBit. These specifications include abort conditions and post-conditions of each Move function as well as invariants of structs and modules.

aborts_if specifications cover important classes of properties, such as access control checks, input validation, and state validation. Move functions are normally designed to abort when they are called (1) by an account without permission, (2) with an input argument outside of an expected range, or (3) on an unexpected global state. For example, in the Aptos Framework’s staking config contract, only the aptos_framework account (i.e., 0x1) can call update_recurring_lockup_duration_secs. Also, the input parameter new_recurring_lockup_duration_secs should be non-zero. It should be called only 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(  
    aptos_framework: &signer,  
    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<StakingConfig>(@aptos_framework);  
    …  
}

Given this aborts_if specification, the Prover verifies two things. First, it verifies that the function indeed aborts when any one of the conditions holds. Second, the Prover verifies that the function does not abort on any other condition. This verification is important because it allows developers to understand the complete set of conditions under which the function can abort, thus the specifications also serve as precise documentation. The complete specification of the function above can be found here.

Impact of Formal Verification

Formal verification has had many positive impacts on the Aptos Framework, providing assurance on the execution of the critical functions, and finding issues before new functionality landed on Aptos Network in production.

• Before Aptos went to mainnet, we had already verified the absence of unexpected abort behavior in block::block_prologue. This function must never abort since it is executed with each block, and a malfunction can bring the entire network down. The block prologue complex execution involves 96 Move functions in 22 different Move modules. We formally specified all these modules and proved that the block prologue execution would never fail (or abort) in an unexpected condition. During this process, we identified and fixed some potential arithmetic overflows during the block prologue execution. The complete specification of this function can be found here.
• A number of issues were found during the specification and verification of the code. The code had already undergone unit testing and auditing, resulting in a relatively small number of new findings. However, formal verification ensures that the probability of further unknown issues is very low. In contrast to testing, formal verification does not just show the presence of bugs but proves their absence.
• We have identified and defined various invariants within the modules, significantly enhancing our understanding of their behaviors and their security implications. This deeper insight has subsequently guided the refactoring and improvement of several modules.
• The specifications form an integral part of the automatically generated Aptos Framework documentation, providing a clear and detailed account of the expected behavior for each function and module (e.g., the specification of coin::register). This precise documentation of security requirements is essential for ongoing maintenance and ensuring quality assurance.
• Finally, integrating the Prover into the Continuous Integration (CI) testing process significantly reduces the necessity for frequent audits with each contract modification. Consequently, formal verification has effectively decreased both the time and cost associated with auditing.

Conclusion and Future Plans

In order to ensure the highest quality and security of the Aptos Framework, we have applied a methodology that combines manual auditing, testing, and automated formal verification. In collaboration with OtterSec, the framework was audited, and high-level security requirements were elicited and documented. In collaboration with MoveBit, the Framework was specified, function-by-function, until most of the high-level security requirements were eventually formally verified. During this work, we also found bugs and usability issues in the Move Prover, which have been fixed to the benefit of all users of Aptos Move.

This combined work gives the Aptos Framework an unmatched level of quality assurance in the blockchain industry and beyond. Moving forward, Aptos Labs is committed to maintaining and evolving the verification work as well as improving the Prover itself, keeping it available for builders and auditors across the Aptos ecosystem, pushing the boundaries of software quality in the space.

Source

About MoveBit

MoveBit, a subsidiary brand of BitsLab, is a blockchain security company that specializes in the Move Ecosystem. We are at the forefront of utilizing cutting-edge Formal Verification techniques. The team comprises security professionals with extensive experience in both academia and enterprise. As one of the earliest contributors to the Move ecosystem, we have collaborated closely with Move developers to establish security standards for secure Move applications, making it the most secure Web3 destination.

Requests a quote

• Website: https://www.movebit.xyz/
• Twitter: https://twitter.com/movebit_