Securing Smart Contracts: A Dev’s Guide Part I

Introduction

As the popularity of smart contracts has grown since the advent of Ethereum around 2013, the frequency of hacks targeting them has also increased. In June of 2016, one of the first major smart contracts occurred, when a blackhat hacker identified a weakness in The DAO’s code, which allowed them to steal $60M from a re-entrancy exploit.

Since that event, the frequency of hacks has continued to increase. 2022 was an all-time high in stolen funds, with an estimated $3.7B lost. 2023 was a particularly tragic year for DeFi, as three major protocols were exploited: Euler Finance ($197M), Multichain ($126M), and Curve ($69M).

With the number of hacks and the magnitude of dollars exploited so high since the 2021, the number of security audits has drastically increased. By 2023, the growth in the number of vulnerabilities found by auditing firms was 476%, which indicates an increase in smart contract complexity. From 2016 to 2023, the number of issues found increased by 19,642%.

Where do we go from here? While many teams are building security solutions for the EVM world, we believe that these are simply band-aid solutions. At Movement Labs, we believe that a security-oriented blockchain future requires a completely new paradigm: the adoption of Move. This report will serve as Part I to a two-part series, in which Part I will be an initial introduction of Move’s unique security features and Part II will identify specific EVM’s ailments that Move can resolve.

Move and Its Security Features

1. Resource Paradigm

Move’s most distinctive feature is its introduction of the concept, resources. Resources are a unique type that can only be copied or discarded if specified abilities, and can only be moved between accounts and locations, much like physical objects in the real world. This resource-oriented programming model is a key innovation in Move, providing a secure and intuitive way to handle digital assets.

Resources have three distinguishing characteristics:

Strict Ownership:

Move’s resource system is designed to enforce stringent ownership and conservation principles, ensuring that resources—like digital assets or tokens—are meticulously controlled and tracked. This framework prevents resources from being duplicated or lost inadvertently. Each resource in Move is marked with specific capabilities that define its behavior, such as whether it can be duplicated or not. This strict enforcement mechanism ensures that every resource maintains a single, verifiable owner at any time, drastically reducing the possibility of fraud or errors that can occur in systems with less rigid ownership rules.
Intuitive Asset Handling:

With Move, the handling of digital assets is modeled after the movement of physical assets in the real world, adding an intuitive layer to digital transactions. Resources must be explicitly transferred from one account to another, mirroring the physical exchange of items between individuals. This approach not only makes the transactions more tangible and understandable but also ensures detailed tracking and recording of asset movement. Moreover, resources can only be copied or discarded if they possess certain specified abilities, which adds a layer of control and security by restricting unauthorized replication or deletion. This mimics the way physical assets are handled, where transferring ownership or disposal requires physical actions that are difficult to fake or replicate without authorization.
Local State:

In Move, resources are stored directly in individual accounts, not in a shared global state that is typical in other blockchain environments. This account-based storage model significantly reduces the risk areas (attack surface) that could be exploited in smart contracts. By localizing the storage of resources, it becomes much more challenging for attackers to access or manipulate the state of resources across the network. Each account acts as a secure container for its resources, which increases the difficulty for potential security breaches. This localized state management ensures that resources are isolated, which enhances the integrity and security of the smart contracts. As a result, the overall security of the blockchain is improved because attackers must access each account individually rather than exploiting a single vulnerability that could affect the entire network. This design parallels having individual safes in every home instead of a central bank vault, making systemic attacks far less feasible and enhancing security at each point of resource storage.

To showcase the basic functionalities of minting and transferring coins using Move’s resource system, we provide a code example below.

In this example:

Defining a Coin resource:
1. The code defines a Coin struct with a single field value of type u64, representing the amount of the coin.
2. The has key annotation is used to make the Coin struct a resource that can be stored and owned by accounts.
Minting new coins:
1. The mint function is a public function that allows the creation of new coins and moving them to an account.
2. It takes an account parameter of type &signer, representing the account to which the coin will be minted, and an amount parameter of type u64, specifying the value of the coin to be minted.
3. Inside the function, a new Coin resource is created with the given amount, and the move_to function is used to move the newly created coin to the account, ensuring ownership.
Transferring coins between accounts:
1. The transfer function is a public function that enables transferring coins from one account to another.
2. It takes a from parameter of type &signer, representing the account from which the coin will be transferred, a to parameter of type address, indicating the recipient’s address, and an amount parameter of type u64, specifying the amount of coin to be transferred.

The provided code example demonstrates the implementation of a Coin resource in Move. It outlines how to define, mint, and transfer digital currencies securely. The Coin is established as a struct with a unique resource type, ensuring it cannot be duplicated or lost. The minting function allows new coins to be created and securely placed into an account through a defined process that verifies ownership. Additionally, the transfer function enables the movement of coins between accounts, maintaining transaction integrity and asset traceability. This example underscores Move’s strengths in managing digital assets by mirroring real-world asset handling, thus reducing vulnerability to security threats and exemplifying the potential for safer blockchain transactions.

2. Bytecode Verifier

Move takes a unique approach to ensure the security and integrity of its execution environment by focusing on bytecode verification rather than relying solely on the source language. In most existing blockchain languages, the source code is compiled into bytecode, which is then checked and verified before execution. This language flow introduces potential vulnerabilities, as these languages rely on the compiler to act as an imperfect gatekeeper. As a result, a malicious actor could potentially bypass the source language and write malicious bytecode directly, introducing it to the execution environment without going through the compilation and verification steps.

The malicious bytecode could include instructions that perform unauthorized actions, such as:

Transferring funds from other accounts to the attacker’s account without proper authorization.
Modifying the state of the smart contract or other contracts in unexpected ways.
Bypassing access controls or permissions checks that are supposed to be enforced by the smart contract.
Consuming excessive computational resources to cause denial-of-service attacks or disrupt the normal functioning of the blockchain network.

To mitigate this risk, Move takes a different approach. The executable format of Move is bytecode, and all necessary protections are encoded after the point of compilation. While Move still has a source language, the safety guarantees are not embedded into what will eventually be run through the compiler. Instead, the Move source language compiles to bytecode, which is then checked by a bytecode verifier before being executed directly by a bytecode interpreter. By removing the compiler from the trusted base, Move eliminates a possible point of subversion and ensures that all executed code has been properly verified.

The bytecode verifier in Move plays a crucial role in ensuring the safety and integrity of the execution environment by enforcing a wide range of properties.

It checks that procedures and struct declarations are well-typed, enforcing the linearity of resources and ensuring that dependent modules and procedure targets exist, implementing static linking
It verifies that module dependencies are acyclic, preventing circular dependencies that could lead to unexpected behavior.
The bytecode verifier in Move performs comprehensive memory safety checks, ensuring proper stack management, encapsulation, and exclusive access to mutable references, while also preventing memory corruption, dangling references, and data races. These checks collectively contribute to the overall memory safety and security of Move programs.

These comprehensive checks performed by the bytecode verifier in Move contribute to the overall safety and reliability of the execution environment.

3. Move Prover

The Move Prover is a formal verification tool that is used to mathematically prove the correctness and safety of Move smart contracts. It allows developers to specify the intended behavior of their code using formal specifications, and then automatically verifies that the code adheres to these specifications.

Here’s how the Move Prover is used:

Writing Specifications:

Developers start by writing formal specifications for their Move code. These specifications are expressed using the Move Specification Language (MSL), which is a higher-level language that describes the expected behavior of the code. Specifications can include preconditions, postconditions, invariants, and assertions that define the desired properties of the code.
Annotating Code:

Once the specifications are written, developers annotate their Move code with these specifications. They use special annotations, such as `ensures` and `requires`, to indicate the preconditions and postconditions of functions, and `invariant` to specify invariants that should hold throughout the execution of the code.
Running the Prover:

With the code annotated, developers can run the Move Prover on their smart contracts. The prover analyzes the code and specifications and attempts to mathematically prove that the code satisfies the specified properties. It uses techniques such as symbolic execution, theorem proving and Satisfiability Modulo Theories (SMT) solving to reason about the behavior of the code.
Verifying Correctness:

If the Move Prover is able to successfully verify the code, it provides a mathematical guarantee that the code behaves according to the specifications. This means that the code is free from certain classes of errors, such as arithmetic overflows, division by zero, and violations of preconditions or postconditions.
Identifying Errors:

If the Move Prover finds any violations of the specifications or detects potential errors, it generates counterexamples or error traces that demonstrate the problematic behavior. Developers can use this feedback to identify and fix issues in their code or refine their specifications.

The Move Prover is particularly useful for verifying the correctness of critical smart contract components, such as token transfers, access control, and state transitions. By providing mathematical proofs of correctness, the prover helps ensure the security and reliability of Move smart contracts, reducing the risk of bugs, vulnerabilities, and unintended behavior.

The Move Prover offers several key benefits that enhance the development and security of smart contracts. By catching errors and vulnerabilities early in the development process and verifying the absence of common smart contract issues, the prover significantly improves the security of Move smart contracts. Moreover, the mathematical proofs generated by the prover provide strong formal guarantees about code correctness, boosting confidence in its behavior, while also reducing the need for extensive manual testing and debugging efforts. It is a powerful tool that complements the inherent safety features of the Move language.

Conclusion

This report explores the increasing frequency and magnitude of smart contract hacks in the blockchain industry, highlighting the vulnerabilities of the current EVM model. It introduces Move, a programming language with unique security features that can mitigate many of the risks associated with smart contract development and execution. Move’s resource paradigm, bytecode verification, and formal verification tools, such as the Move Prover, offer a more secure and reliable foundation for smart contract development.

The next report will be Part II, in which we will delve deeper into the specific ailments of the EVM model and how Move can resolve them. By identifying the root causes of smart contract vulnerabilities and demonstrating how Move’s features can address these issues, we will provide a comprehensive case for the adoption of Move as the future of secure blockchain development.

At Movement Labs, we are working to make the Move programming language accessible across the entire modular blockchain ecosystem, rather than being controlled by a single network. Our flagship products, M1 and M2, are designed to provide seamless interoperability between Move-based environments and other networks.

References

About Movement Labs Research

Movement Labs Research features technical insights and original research into the Move language, the Move virtual machine, modular blockchain development, and innovations with the Movement Labs SDK and Move Stack. You can find our content at https://blog.movementlabs.xyz/ and follow us on X @mvmt_research for the latest ideas and insights into Move-related development.

About Movement Labs

The first integrated blockchain network, powering the fastest and most secure Layer 2 on Ethereum. Designed to pair smart contract security and parallelization with EVM liquidity and user bases, Movement is bringing the MoveVM to Ethereum through its flagship L2 and connected rollups with the Move Stack. For more information about Movement Labs and a guide to participate in our devnet, please visit: movementlabs.xyz and follow on X @movementlabsxyz and on Discord.