by Aptos Labs and OtterSec
The Aptos Network uses the Move smart contract language as the underlying programming model. While Move is designed for an ecosystem of secure smart contracts, a faulty implementation of Move itself can jeopardize those properties. At Aptos Labs, we are committed to making Move as secure as possible, together with the community. We are both investing in tools for writing correct smart contracts (e.g. the Move Prover, developed predominantly by Aptos), as well as the correctness of runtime core components like the Move Virtual Machine. In this article we describe how we, together with our partners, achieve the latter via auditing, bug bounties, fuzzing, and security hardening of the underlying implementation.
Move’s security is based on a few basic properties. These properties are defined in terms of the bytecode that the Move execution engine consumes and are independent of the source language:
- Type safety: Each value has a unique and unforgeable type. For example, it is not possible to take some value of type
addressand turn it into a security relevant token of type
- Modular encapsulation: Resources in storage can only be manipulated from code within modules that are declaring those resources. Only functions with matching visibilities can be called cross-module.
- Ownership and lifetime: Move’s ability system enforces that a value is not copied, dropped, stored, or used as a key unless the corresponding ability is declared for the value type.
- Reference safety: References do not outlive the values that they are pointing to. A mutable reference is exclusively owned, such that aliasing is not possible.
The traditional architecture of the Move virtual machine delegates validation of the above properties to the (bytecode) verifier as seen in the diagram below:
The following are the questions that we are interested in:
- Is the bytecode verifier complete, and does it guarantee that all of the properties above are satisfied for every program? This is important because violating any of the properties above can potentially result in the loss of assets.
- Can a given Move bytecode program crash the execution engine? Because in a replicated state machine, all nodes execute the same programs, this can be used to halt the network.
- Can a given program cause the execution engine to run out of resources (memory or time)? This can be exploited for DoS attacks slowing or suspending the network.
At the core of developing bug-free code are disciplined software engineering practices paired with the right tools. At Aptos, we are following the rigorous process of mandatory code review and continuous testing and integration, combined with the best practices of the Rust ecosystem. In addition to these traditional aspects, we are also applying the following measurements to keep Move as safe as it is designed to be.
One of the most respected measurements in the industry to gain confidence in blockchain networks is auditing. At Aptos Labs, we contracted Certik (report) and Halborn for auditing the Move Virtual machine. Multiple critical issues were found, one of them in the category of type safety.
In addition to external auditing, Aptos Labs led and organized a community auditing effort, focused on the bytecode verifier. Engineers from Mysten Labs, Starcoin, and auditing companies like MoveBit and OtterSec teamed up with Aptos engineers for this effort, investing about 6 person weeks of auditing time. The results of this are captured in this spreadsheet, referring to dozens of documents created during this audit. This auditing effort found and addressed multiple issues before Aptos hit mainnet.
Last, but not least, we have a close collaboration with OtterSec. The OtterSec team performed manual code reviews and developed fuzzing technology for various targets, identifying multiple critical issues in both the Move VM and Aptos framework code. They also led efforts to add redundant defense-in-depth logic to the Move VM (see below), influencing our ongoing design work to mitigate further loss of funds vulnerabilities.
Aptos Labs runs a bug bounty program. For critical bugs of the kind which can lead to loss of assets, bounties of up to $1,000,000 are offered. Similarly, crash bugs can be rewarded with up to $100,000.
With the bounty program, we have worked closely with a talented set of security researchers to find and fix bugs. A few of those bugs were in the critical category, while other bugs have been crashes found by using fuzzers.
Aptos Labs has stood to its commitments in bug bounties, and significant bounties were paid out. Moreover, Aptos Labs has continued to utilize the expertise of whitehats we met via the bounty program and intend on continuing to work together with this community.
The bounty program motivated us to invest in fuzzing at Aptos Labs ourselves. The Move VM code has been modified to implement the
Arbitrary Rust fuzzing trait at relevant points, thus enabling the use of ‘cargo fuzz’ to dynamically generate and validate bytecode modules… We have a few continuous jobs running with those fuzzing targets.
One way to achieve extra assurance of security is via redundancy. We added a so-called paranoid mode to the Move VM, which enforces type safety and the other rules mentioned above at execution time. While the bytecode verifier already checks such properties when the code enters the system, the paranoid mode reverifies the same checks again during bytecode execution time. The paranoid mode was extensively discussed within the Move community, with Aptos engineers leading the design. For more information see this PR (final version) and this PR (intermediate version).
At Aptos Labs, we are committed to making Move as secure as possible, and invested heavily into this area. Here we described ongoing efforts around auditing, bug bounties, fuzzing, and hardening conducted by us and our partners. Moving forward, we plan to continue to invest in this space. We will continue to offer a bug bounty program, engage with reputable security auditors, and drive development of security hardening tools, e.g., fuzzing technology.