Move is a relatively new programming language which has seen application in a number of Web3 projects. We recently audited a novel Layer 1 blockchain which supports smart contracts written in Move, and thought we’d take this opportunity to give a general overview of Move. If you’re a smart contract engineer who’s interested in learning about this new programming language, read on.

What is Move?

Move is a domain-specific programming language for writing smart contracts. It is used by several recently-launched projects, including the Aptos, 0L, and Starcoin blockchains. The Sui blockchain uses its own version of Move called Sui Move. Move was originally developed as part of the Diem project, Meta’s now defunct blockchain-based payment network.

"To successfully support a payment system like the Diem Payment Network, we need a programming language that can encode ownership of digital assets and create procedures for the transfer of those assets. There are hundreds of languages already in use, some of which are already native to blockchain implementations. Diem Networks could have chosen a general-purpose language like WebAssembly or Java bytecode, or an existing blockchain language like EVM bytecode or Bitcoin script. Typically, choosing an existing language is the right decision. The community, libraries, and tooling for a language is at least as important as the language design, and each of these takes years to build. Thus, the decision to create a new language should not be taken lightly. We chose to create Move because we saw an opportunity to create a step-change improvement over existing alternatives in several important ways."

– Diem, Why Build Move?

Diem needed to securely support a high volume of transactions, and the team decided to create Move with these goals in mind. In this blog, we'll discuss two features of Move: programmable resources, which help support high transaction rates, and formal verification, which can help improve security. Along the way we'll discuss Move's syntax, type system, and memory model, and examine some of the common mistakes that programmers can make using Move. In an upcoming post, we'll take a technical look at the promise and pitfalls of Move formal verification.

Programmable Resources

One of Move’s key features is its use of programmable resources. A resource is data that directly represents an item of value, such as the number of tokens a user holds. In Move, each account that owns a token typically has a piece of data stored in an account that directly represents the token. This contrasts with the representation of tokens in Solidity, which is typically a single large “mapping” from accounts to the numbers of tokens they own.

This utilization of programmable resources has two primary benefits. Firstly, it leads to a smart contract programming model that supports high transaction rates. If a transaction involves two accounts that interact only with each other, that transaction can happen in parallel with other transactions. This is analogous to the way physical money is handled. If one person is paying cash to another person, it doesn’t matter what other people are doing with their own cash. The Aptos blockchain uses software transactional memory to run transactions in parallel and detect whether two simultaneous transactions might conflict.

The second benefit of programmable resources is that they make it possible to automatically verify that programs do not have certain kinds of errors: for example, that a resource is never silently dropped or duplicated. This is done by the Move compiler. However, it is still possible to introduce arithmetic or logical errors in smart contract code that lead to incorrect values in resources.

The following diagram from the Move documentation on GitHub shows how blockchain data is organized in Move. Move calls the blockchain state global storage. Each blockchain address represents an account, some of which may be externally-owned. Unlike in Ethereum, all addresses can have data stored in them. In the diagram below, owners of BasicCoin have data (a resource) in their accounts representing the amount of BasicCoin they own. The diagram shows that one address, 0x42, also owns a module with code that implements BasicCoin.

When writing smart contracts in Move, it is best practice to store resources in the account that owns the resources rather than the account that contains the code. While it is possible to implement Ethereum-style resource mapping in Move smart contracts, it may not be possible to execute transactions involving such contracts in parallel.

Move’s Security Features

Move includes several features that help developers create more secure smart contracts. As we mentioned, the compiler checks basic usage of resources. Move also has built-in support for formal verification and intentionally excludes language constructs that tend to make formal verification difficult. Additionally, Move has support for generics. Generic programming allows common code to be reused across types. This is important because one way to make code more secure is to write less new code, and reuse code that has been written carefully by experts. For example, many coins share common implementation code. Generic programming allows that code to be shared across different coins, as the Aptos Coin standard shows.

The Move Type System and Rust

When working with data that represents items of value directly, it becomes important to track who owns that data and to limit what can be done with that data (such as copying or deleting the data). Fortunately, there is already a well-developed programming language that has constructs for talking about ownership of data: Rust. The developers of Move were inspired by ideas from Rust, in both types and syntax.

This chart shows the built-in primitive types of Move:

This chart shows constructed types of Move. These are types built from other types:

Things get interesting when it comes to struct types, the only user-defined types in Move. A struct type is a collection of values stored in fields:

In Move, a struct is a “value” type. Values of struct types are laid out linearly in memory or storage. A reference to a struct has to be constructed explicitly. This differs from Solidity, where struct variables are always references to the underlying value. The following diagram illustrates this:

Fields can be any type except reference types. An instance of a struct is created by packing it (as in Rust). Move implements a Rust-like ownership system for values of struct types, where each value is owned by the variable or field that contains it. References do not own any values to which they point. By default, struct values can only be moved to another owner. They cannot be copied or dropped. When a struct value is moved to another owner, it is consumed and it becomes inaccessible to the prior owner. After a value of a struct type is created, only a single copy of the value exists and is usable at a time. The following code illustrates this:

Move has a typing feature called abilities that controls what actions are permissible for a value of a given type. This is inspired by Rust. The four abilities are:

• Copy: value can be copied. Non-copy structs cannot be accessed after they are consumed.
• Drop: value can be dropped. A value is dropped when its owning variable or field goes out of scope Values of non-drop struct types must be consumed, either by explicitly destroying them or “moving” them elsewhere. They cannot just be silently dropped.
• Store: value can be stored inside other structs in global storage.
• Key: the type can be used as a key for global storage operations.

For a struct type, type abilities are declared within struct type declarations, as in the following example:

Resources in Depth

A resource is a struct that has only key and store abilities. In Move, an account can hold at most one resource of each type. Resources cannot be copied or dropped. This makes resources suitable for directly representing items of value such as coins. The direct association between accounts and their resources makes it more difficult to write code that causes accidental losses of value. However, it remains possible to implement incorrect calculations and more subtle logical errors related to resources. That is why we still strongly recommend having a smart contract audit done.

The programming interface for global storage on the blockchain enforces the limitation that each account can hold at most one copy of each resource. A program can create, read from, update, and remove resources in global storage using the following operations:

To avoid forging of resources or improper manipulation of resources, Move enforces strict encapsulation of data. Move code and type declarations are grouped into modules. Code is deployed to an account as part of a module.

When a struct type is declared in a module, only functions defined in the same module can access the fields of the struct type or create values of the struct type. Move struct declarations are treated as abstract data types that hide their inner workings from code outside of their module. Functions in a module are private by default and can only be called from within the module. They can be declared public, which makes them accessible to external code. Modules can have friends, which are other modules they trust, and can declare individual non-public methods to be accessible to friends.

References

A reference is a type of pointer that includes restrictions on how it can be used. A common problem in languages with pointers is dangling references: pointers to memory or storage that has been re-used for another purpose or deallocated. For example, if you create a reference to the last element of a vector and then shrink the vector, the reference now points to invalid memory or storage. Dangling references and other issues related to unrestricted pointers have historically caused the most software security vulnerabilities.

Move handles references similarly to the way Rust handles references. It includes type checking rules that ensure the lifetime of a reference is no longer than the lifetime of the original data. When code creates a reference, the reference does not take ownership of the data. Instead, the code borrows the ability to read or write the data. In reading Move code, operations with the term “borrow” in their names produce references.

The Move language definition does not contain a complete description of reference checking (the “borrow checker”, which ensures that borrowed references do not live too long). A detailed technical paper was published this year, though. Two key rules in the definition are:

• References to references are not allowed, and references cannot be stored in structs. This means that when a function is called with a reference argument, it cannot store the reference in a long-lived data structure, though it can return the reference.. A function call does not extend the lifetime of a reference.
• A reference to a local variable or field of a local variable must not live beyond the end of the scope of the local variable.

Rust-like Syntax

Move has a Rust-like syntax that differs in some places from C-style languages. Here we summarize some important syntax rules to make it easier to browse Move code. Variables are declared using let declarations:

The type annotation : type and initializer =e are optional. When they are omitted, Move uses type inference to determine the type of the variable.

Some examples of variable declarations are:

Move has typical expressions for arithmetic, shift operations, function calls, assignment, and so on. Move has only expressions, not statements. It has if, while, for, break, and continue expressions for flow control. The left-hand side and right-hand side of an if expression must have the same types. while and for loop expressions evaluate to the unit type, which has no value at runtime.

Functions are declared using the syntax:

where id is the name of the function, parameter-list declares the parameters, and return-type is the return type. There are additional annotations required such as acquires annotations. These list the resources from global storage that the function accesses. Thare also annotations for visibility; as described previously, functions can be public, private, or accessible to friend modules.

Support for Formal Verification

It is crucial that smart contracts function securely and correctly since they can hold huge amounts of value. Formal verification is one of the best techniques for ensuring that a program (such as a smart contract) does what it is supposed to do.

In formal verification, a programmer writes specifications to mathematically express the desired behavior of the code. A tool then tries to check that the code meets the specification. You can think of the checking as similar to testing, but with a critical difference. Instead of examining the code's behavior in some specific scenarios, it examines the code's behavior in all possible scenarios. If the check succeeds, the tool could not find any situation under which the specification would be violated. This doesn't mean that it is impossible for the code to violate the specification because there's always the possibility that the tool or the compiler contains a bug that could cause such a violation. However, it provides much higher assurance than running a set of tests.

For some code, especially complex code, the tool may not be able to check automatically that code meets the specifications. A programmer may need to add specifications for smaller parts of the code until the checker can succeed. A programmer may even need to write proofs that the code meets the specifications. The tool then checks that the proofs are correct based on mathematical principles.

Because of the importance of securing smart contracts, some smart contract languages include integrated support for formal verification. The Solidity compiler provides the SMTChecker tool, which assumes that requires clauses are always true and then tries to prove that assert clauses will never fail.

Move also has integrated support for formal verification. It includes a rich specification language that enables the specification of more complex properties than Solidity’s requires and assert clauses, and purposefully omits language constructs that cause problems for formal verification. The Move development environment includes a checker called the “Move Prover”.

Formal verification is near and dear to our hearts at CertiK. We were founded by two Ivy League computer science professors who are experts in formal verification. They are the creators of CertiKOS, the world’s first and only fully-verified multi-core OS kernel and hypervisor. CertiK was created as a company to secure smart contracts by applying formal verification technology to the auditing process. When a programming language with integrated support for formal verification comes along, it catches our attention.

Here is a simple example of a double function and its specification. The double function takes a 64-bit unsigned integer and doubles it. The specification of double given by spec double mathematically describes the expected result.

The specification language is an integrated part of Move. Specifications are separated into spec blocks. Spec blocks specify preconditions (requires) and postconditions (ensures) of functions. A precondition is what must be true before the function is called for the function to operate properly. A postcondition is what must be true when the function returns, assuming the preconditions were true. Spec blocks also specify failure conditions (aborts_if). The specification language supports most regular Move syntax. It also supports important additional features for specifying program behavior, including forall, exists, and implies.

Here is an example of a specification block:

The Move Prover translates specifications and program semantics into logical expressions. These are then passed to Satisfiability Modulo Theory (SMT) solvers such as Z3 and CVC5 to prove or disprove. The following (vastly-simplified) diagram illustrates this:

There are pros and cons to formal verification. Formal verification is considered the “gold standard” for building reliable programs and is used in many mission-critical systems, such as NASA spacecraft. Writing formal specifications for system behavior can expose logical inconsistencies or unclear thinking. However, formally specifying even relatively simple systems can be difficult and time-consuming, even for experts. It is important to ensure that the specifications are correct; the saying Who watches the watchers? applies here. Checkers can also have trouble with more complex programs or specifications, and may take extremely long amounts of time to complete their checks (if they can complete them at all).

As mentioned, in a future post, we'll look more closely at the promise and pitfalls of Move formal verification. Because of the complexities of formal verification, we recommend you have a third party with experience in formal verification audit your contracts or help assist with the formal verification of your contracts.

Conclusion

We hope this post has provided a useful introduction to the Move programming language. Move introduces new approaches to addressing scalability issues and improving security. However, no language is entirely foolproof, and it’s still possible to write non-scalable or incorrect code that interferes with Move’s built-in features.

As with everything in Web3, the rabbit hole is practically endless. There’s some great developer documentation out there if you’re looking to go deeper into the technicalities of this new programming language. And keep an eye out for our upcoming technical deep dive into the Move Prover: a formal verification tool for smart contracts written in Move.