Move is a programming language specifically designed for building secure and formally verified smart contracts. Move’s language features provide a strong set of security protections through strict type enforcement and load-time verifications. Developers who master Move’s built-in resources and programming patterns can produce more secure projects than those developed in conventional languages that lack these features.

However, in the course of our work auditing smart contracts written in Move, most notably the novel Layer 1 blockchain Aptos, we have encountered multiple instances of developers either neglecting to use Move’s built-in protection mechanisms or adopting programming patterns that work counter to Move’s design philosophy. Such patterns are partially due to the relatively steep learning curve involved with adopting a new language, and partially a result of programmers simply “migrating” legacy code designs. We call such programming patterns immovables. This article presents a few such examples along with our suggestions for how to fix them.

Benefits of the Move Programming Language

(Note: This article summarizes some of our experiences in auditing Move smart contract code. It requires some basic knowledge about the Move language. See here for a detailed introduction to Move.

Some of the most important security features of Move include type safety, resource safety, and reference safety. Move embeds type information at the bytecode level, and provides mechanisms to specify and enforce resource ownership. The permitted behavior of each resource object is strictly verified at load time and enforced at run-time. In addition, the Move language design ensures no dangling references through ownership rules, similar to the Rust programming language. This article is not intended to be a review of the aforementioned features, but rather a discussion of the consequences and remediation of failing to utilize Move’s in-built features when writing smart contracts.

Aptos is a major blockchain project written using Move. Our team of expert engineers comprehensively reviewed Aptos's core code, and this blog post summarizes some of the issues encountered for the benefit of future projects leveraging the Move programming language.

Similar to Rust, Move provides a simplified and more restricted type system for developers to flexibly manage and transfer assets, while providing the security and protections against attacks on those assets. As shown in the example below, Move eliminates signed integer types from the primitive types, and only supports unsigned integers for built-in integer overflow detection.

Code Snippet 1: A simple u64 addition with built-in overflow detection

In Code Snippet 1, we define a function to add two u64 values. A runtime ARITHMETIC_ERROR will be triggered if the addition overflows, as shown in the test case below.

Move also provides a Prover that helps developers formally verify the properties of contract code. Developers can specify preconditions and postconditions for each function in spec blobs. After that, the Move Prover can prove whether the specified conditions are met, and provide concrete input if there is any violation. For example, we can verify the built-in overflow detection by writing the following spec.

 Spec 1. Specification for Code Snippet 1.

Immovables Resulting From Developers’ Legacy Burden

Despite having a number of powerful security features, Move developers still face the challenges of writing secure smart contracts. Inexperienced developers might use unsuitable legacy programming patterns with which they are more familiar or misuse some Move features due to the steep learning curve.

We noticed a few instances of programming patterns in recently developed projects written in Move that are countering the protection offered by the language’s strong type system and abstractions. Some of these patterns tend to bring back the same vulnerabilities that Move’s designers were trying to remove with novel language features. A couple of examples of these legacy patterns are:

We call these legacy patterns the immovables in Move-based smart contracts. These immovables are especially common because many projects were ported by developers from projects built in other programming languages such as Solidity, which does not have the same strong type features (and constraints) in its language design. Below are a few examples of such patterns and their issues. We also provide some recommended remediations for each example.

Immovable #1: Resurrecting Vulnerable Types

Lots of smart contracts use signed integers for math in contract implementations. For developers that are used to implementing a contract using a signed integer, discovering that there are no signed integer types in Move might come as a surprise.

While experienced developers can choose to learn the built-in type in Move and reimplement the contract with only unsigned numbers, some developers choose to bring the signed integer type back to their Move code. We have observed a few cases in some Move projects. Below is a simplified version.

 Code Snippet 2: A vulnerable I128 implementation used in some Move contracts.

In this example, a developer chooses to implement their type of signed integer (i.e. I128). This is likely due to the fact that the reference implementation uses signed integers and the developer simply decided to keep the design. Using the above implementation actually introduces integer overflow problems.

Remediation

We advise developers not to import these unrecommended types to Move projects. The best practice is to redesign the application using the built-in Move types. However, for those cases where legacy patterns (such as signed integer objects) have to be used, we can leverage Move’s built-in prover to add a level of verification.

Below is an example of using the Move Prover to find property violations using the following specification. The spec ensures that the addition of two positive integers should result in a positive integer as well.

 Spec 2. Specification for Code Snippet 2.

With the above specification, we can run the built-in Move Prover. The outcome is shown below.

 Output 2. The Move Prover’s output for Spec 2 and Code Snippet 2.

The output shows that the Move Prover captured a violation of the spec. We recommend developers utilize the Prover to verify the self-defined type if they have to reintroduce legacy types.

Immovable #2: Misunderstood Reference Safety

The second example of an immovable pattern is related to the Move resource type. Move provides a new storage model that separates resource storages (defined as structs) under each account’s address, indexed by its type information. Developers need to add abilities annotations to control the copy, key, store, and drop properties of the resource.

The example below is a simplified buggy code that is supposed to manage a global resource Config. Multiple CoinStores are maintained in the Config indexed by coin_type. In each CoinStore, there is a fees field, specifying the fee rates for the current coin. In this example, the increase_fees function is intended to locate the global CoinStore resource and increases the fees field by 1.

 Code Snippet 3: Invalid update to global resource CoinStore.

The code contains a bug that results from the misuse of resource copy. The increase_fee function that calls the borrow_mut function, which should return a mutable reference of the CoinStore. However, it returns an owned object of CoinStore, which is a copy of the original one in the vector. As a result, any update in the increase_fees function doesn’t affect the global storage. Note that the implicit copy behavior of the CoinStore is allowed because that the developer assigns the copy ability to the structure definition.

 Spec 3. Specification for Code Snippet 3.

We can use the Move Prover to detect such bugs by specifying the Config resource to be modified by the increase_fees function. The Prover gives the unsatisfied error message as shown below, indicating that the increase_fees function does not change global resource Config.

 Output 3. Move Prover’s unsatisfied output for Code Snippet 3 and Spec 3.

Remediation

The above code can be simplified and made secure by adopting the Move resource ownership pattern. Below is an implementation using a config structure with a generic phantom type.

 Code Snippet 4: Recommended programming pattern to organize resources in Move.

We can further write the following spec to ensure the increase_fees function changes the global state.

 Spec 4. Specification for Code Snippet 4.

With the remediated implementation, the Prover proves the implementation satisfies the specification without raising any error.

 Output 4. Move Prover’s output for Code Snippet 4 and Spec 4.

Summary

This article highlights a few error-prone programming patterns we have encountered in Move projects. Such practices are mostly due to the porting of legacy programming designs from non-type-safe languages.

Fortunately, the Move language offers a built-in Prover that can help verify implementations. We show that some of the error-prone programming patterns can be verified and fixed by leveraging the Move Prover. A more thorough approach for developers is to learn and adopt the new design patterns in Move.

Stay tuned for an in-depth exploration of the Move Prover in an upcoming blog post.