Analysis of the Security of Move Language

Move language, as a new generation smart contract language, took into account the security issues of blockchain and smart contracts from the very beginning of its design. This article will explore the security of Move language from three aspects: language features, operating mechanisms, and verification tools.

1. Security Features of Move Language

The Move language abandons the nonlinear logic based on flexibility, does not support dynamic dispatch and recursive external calls, and instead uses concepts such as generics, global storage, and resources to implement alternative programming patterns. These designs help avoid security vulnerabilities such as reentrancy.

The main components of the Move language include:

• Module: Composed of structure types and process definitions, it can import type definitions from other modules and call processes from other modules.

• Struct: Can be defined as a resource type, stored in global key-value storage.

• Process: Define the functions of the module, which can include initialization, secure and insecure processes.

The global storage mechanism of the Move language allows modules to store persistent data and has exclusive read and write access to its declared resource types. This mechanism helps enforce security constraints.

Two important static checking features of Move language:

1. Invariant Check: Defining the conservation of system state through a specification language.

2. Bytecode Verifier: Enforces safety types and linearization to prevent illegal operations.

2. The Operating Mechanism of Move

The Move program runs in a virtual machine and cannot directly access system memory. Program execution is based on the stack, with global storage divided into memory ( heap ) and global variable ( stack ).

The execution state of the Move VM consists of the call stack, memory, global variables, and operation array. Its characteristics include:

• Static jump, avoid dynamic dispatch.
• Call stack adjacency to prevent reentrancy
• Separation of data storage and call stack

This design enhances security and execution efficiency.

3. Move Prover

Move Prover is a formal verification tool that uses deductive verification algorithms to verify whether a program meets its expectations. Its workflow:

1. Receive Move source files and specifications
2. Compile to bytecode and validator object model
3. Convert to Boogie intermediate language
4. Generate verification conditions
5. Use the Z3 solver for verification
6. Generate Diagnostic Report

Move Specification Language is used to describe program behavior specifications and can be written independently of business code.

Summary

The Move language has comprehensively considered language features, virtual machine execution, and security tools, effectively avoiding many common vulnerabilities. However, it is still recommended to use third-party security audit services, and have a security company complete the specification code writing and verification.