MoveBit

May 31, 2023

How to Verify Smart Contracts on the Sui Blockchain

Sui is the first permissionless Layer 1 blockchain designed from the ground up to enable creators and developers to build experiences that cater to the next billion users in web3. Sui is horizontally scalable to support a wide range of application development with unrivaled speed at low cost. Sui uses the Sui Move language as its smart contract language, which is derived from the Move programming language. Move, the next generation of smart contract programming language, takes security as the primary design objective. Move claims to be able to guarantee the security of smart contracts using the Formal Verification tool–Move Prover (MVP). So how to use the Move Prover on Sui? Will the Move Prover become an indispensable tool for securing programming on Sui in the future?

What’s Move Prover?

Move Prover is a tool that uses Formal Verification to verify smart contracts written in the Move language. Formal Verification is a technique that uses rigorous mathematical methods to describe behavior and reason about the correctness of computer systems. Now it has been adopted in operating systems, compilers, and other fields where correctness is prioritized.

Smart contracts deployed on the Sui blockchain manipulate various digital assets, and their correctness is also critical. Move Prover (MVP) is designed to prevent errors in smart contracts written in the Move language. Users can specify the functional properties of smart contracts using the Move Specification Language (MSL), then use the Move Prover to automatically and statically check them.
Simply put, there can be two components in a Move file:

  • One part is the program code, which is the part most of us are familiar with. It is written in the Move programming language (sometimes simply called the Move language). We use it to define data types, and functions.

  • The other part is formal Specification. It is optional and written in the Move specification language. We use it to describe what properties the program code should satisfy. For example, describe the behavior of a function.

When we write formal specifications and fire up the Move Prover, it will verify whether the Move program meets these requirements according to the written specification, and help developers find potential problems as early as possible during the development stage, giving the users of the Move program confidence in the verified properties of the program.
The Move Prover mainly specifies the following three aspects:

  • Struct Invariants: Express what kind of state a structure should have throughout the time;

  • Unit Specification (per single function): Show what kind of specification should be followed by each function of each program;

  • State-machine Specification: Express what kind of state specification the entire global state on the blockchain should follow.

Sui uses the Move language as its smart contract language. Naturally, Move Prover can also be used on Sui. Next, we will describe how to use Move Prover on Sui to verify the smart contract code.

This section focuses on the Function Specifications. We will use the official core code of Sui-Framework as an example, The whole process （installation, writing specs, invoking） includes the following points:

  • How to install and use Sui Move Prover;

  • How to use aborts_ifto specify the possible abort conditions of functions;

  • How to define the postconditions (functional properties) of functions through ensures;

  • How to simplify redundant specifications through Schema.

Contents in this section:

This section focuses on the Function Specifications. We will use the official core code of Sui-Framework as an example, The whole process （installation, writing specs, invoking）includes the following points:

  • How to install and use Sui Move Prover;

  • How to use aborts_if to specify the possible abort conditions of functions;

  • How to define the postconditions (functional properties) of functions through ensures ；

  • How to simplify redundant specifications through Schema.

Install the dependencies of Move Prover for Sui

Before using Move Prover, we first install some of its external dependencies, including boogie, z3, etc. The official GitHub repository of the Move language provides us with files to install these commands, please execute the following command in the terminal. (If dependencies installation fails, please check if the terminal needs to be configured with a proxy.)

mkdir move_lang && cd move_lang
git clone https://github.com/move-language/move.git
cd move
./scripts/dev_setup.sh -yp
. ~/.profile

After the above command is executed, type boogie /version . If the output is something like “Boogie program verifier version X.X.X”, which means the installation has been successful.

boogie /version
Boogie program verifier version 2.15.8.0, Copyright (c) 2003-2014, Microsoft.

Secondly, install Sui Cli (installation guide: https://docs.sui.io/build/install) and then type sui -V in the command line. If the output is similar to “sui xxx”, which means the installation has been successful.

sui -V
sui 0.21.0

Start Verification

Prepare an example for verifying

Create a project

First, let’s create a new folder basic_balance, enter the folder and create a new Move project named BasicBalance through Sui official command sui move new BasicBalance :

mkdir basic_balance
cd basic_balance
sui move new BasicBalance

After creation, you can see that its directory structure is as follows:

BasicBalance
|
|---- Move.toml (text file: Project Configuration File)
|
`---- sources   (Directory: Source Files)

Now we create BasicBalance/sources/balance.move .

The content of “balance.move” is the balance module on Sui-Framework. We copy the code, delete the spec and add two new functions for the convenience of demonstration. The code is as follows:

// Copyright (c) Mysten Labs, Inc.
// SPDX-License-Identifier: Apache-2.0

/// A storable handler for Balances in general. Is used in the `Coin`
/// module to allow balance operations and can be used to implement
/// custom coins with `Supply` and `Balance`s.
module basicbalance::balance {
/// For when trying to destroy a non-zero balance.
const ENonZero: u64 = 0;

/// For when an overflow is happening on Supply operations.
const EOverflow: u64 = 1;

/// For when trying to withdraw more than there is.
const ENotEnough: u64 = 2;

/// A Supply of T. Used for minting and burning.
/// Wrapped into a `TreasuryCap` in the `Coin` module.
struct Supply<phantom T> has store {
    value: u64
}

/// Storable balance - an inner struct of a Coin type.
/// Can be used to store coins which don't need the key ability.
struct Balance<phantom T> has store {
    value: u64
}

/// Get the amount stored in a `Balance`.
public fun value<T>(self: &Balance<T>): u64 {
    self.value
}

/// Get the `Supply` value.
public fun supply_value<T>(supply: &Supply<T>): u64 {
    supply.value
}

/// Create a new supply for type T.
public fun create_supply<T: drop>(_: T): Supply<T> {
    Supply { value: 0 }
}

/// Increase supply by `value` and create a new `Balance<T>` with this value.
public fun increase_supply<T>(self: &mut Supply<T>, value: u64): Balance<T> {
    assert!(value < (18446744073709551615u64 - self.value), EOverflow);
    self.value = self.value + value;
    Balance { value }
}

/// Burn a Balance<T> and decrease Supply<T>.
public fun decrease_supply<T>(self: &mut Supply<T>, balance: Balance<T>): u64 {
    let Balance { value } = balance;
    assert!(self.value >= value, EOverflow);
    self.value = self.value - value;
    value
}

/// Create a zero `Balance` for type `T`.
public fun zero<T>(): Balance<T> {
    Balance { value: 0 }
}

/// Join two balances together.
public fun join<T>(self: &mut Balance<T>, balance: Balance<T>): u64 {
    let Balance { value } = balance;
    self.value = self.value + value;
    self.value
}

/// Split a `Balance` and take a sub balance from it.
public fun split<T>(self: &mut Balance<T>, value: u64): Balance<T> {
    assert!(self.value >= value, ENotEnough);
    self.value = self.value - value;
    Balance { value }
}

/// Destroy a zero `Balance`.
public fun destroy_zero<T>(balance: Balance<T>) {
    assert!(balance.value == 0, ENonZero);
    let Balance { value: _ } = balance;
}
}

The main function of the above code is for creating Balance and Supply resources to increase, decrease, and split their values. The balance module is mainly used by the coin module, which is the core function of the Sui-Framework. Next, let’s see how to use the Move Prover to verify the functions of the balance module.

The First Verification Code

To give us an initial impression of the use of Move Prover, add the following code snippet to balance.move :

spec increase_supply {
pragma aborts_if_is_strict;
}

Syntactically, this code can be added anywhere in the balance module, but in order to clearly understand the correspondence between the definition and the specification when reading the code, it is recommended to place it after the definition of the function increase_supply .

In short, the code block spec increase_supply {...} will contain our property specification for increase_supply. There are many types of property specifications, such as :

  • Will this function abort? Under what circumstances it will abort abnormally?

  • What conditions must be met for calling the parameters of this function?

  • What is the return value of this function?

  • After the function is executed, what changes will be made to the state of the virtual machine?

  • What invariants will this function maintain?

For example, when we don’t specify any abort conditions, Move Prover allows all possible aborts by default. And in the simple snippet above, we tell the Prover with the indicator aborts_if_is_strict :

I want this function to be strictly checked for possible aborts. Please report errors if any abort that is not listed by the programmer occurs.

Enter the BasicBalance directory, and run the command sui move prove -t balance.move ( If the dependencies installation fails, please check if the terminal needs to be configured with a proxy.), the -t in the command represents the object file that needs to be specified for verification, the balance.move is the file to be verified.

sui move prove -t balance.move

This command invokes Move Prover to check the code of the current module, and you can also use the command sui move prove to check the code of all modules in the directory. After running the command, we can see that Prover reported the following error message:

error: abort not covered by any of the `aborts_if` clauses
   ┌─ ./sources/balance.move:51:5
   │
46 │           assert!(value < (18446744073709551615u64 - self.value), EOverflow);
   │           ------------------------------------------------------------------ abort happened here with code 0x1
   ·
51 │ ╭     spec increase_supply {
52 │ │         pragma aborts_if_is_strict;
53 │ │     }
   │ ╰─────^
   │
   =     at ./sources/balance.move:45: increase_supply
   =         self = &balance.Supply{value = 18446744073709551615}
   =         value = 18467
   =     at ./sources/balance.move:46: increase_supply
   =         ABORTED

exiting with verification errors

The Prover’s output tells us that it found a situation where function increase_supply would abort, but we don’t failed to explicitly indicate the possibility of this abort. Looking at the code that triggers the abort, we can find that the exception is caused by an assertion inside the function, which shows that the parameter value must be less than
(18446744073709551615u64 - self.value). According to the prompt of the error message, we can add the following aborts_if condition:

spec increase_supply {
    pragma aborts_if_is_strict;
    aborts_if value >= (MAX_U64 - self.value);
}

After adding this condition, try to call Prover again, and there are no more verification errors. Now we can confirm with confidence: the function increase_supply would abort if and only if value >= (18446744073709551615u64 - self.value).

Verify the function decrease_supply

The function decrease_supply is to subtract the value of the second parameter balance from the value of the first input parameter self and return the subtracted value.

public fun decrease_supply<T>(self: &mut Supply<T>, balance: Balance<T>): u64 {
    let Balance { value } = balance;
    assert!(self.value >= value, EOverflow);
    self.value = self.value - value;
    value
}

Specify the termination condition of decrease_supply

The decrease_supply has a possibility of aborting:

  • Self.value is less than balance.value

So we can define the termination condition according to the previous example of increase_supply：

spec decrease_supply {
    let value = balance.value;
    aborts_if self.value < value;
}

As you can see, a spec block can use let to define an expression to a name and can be used repeatedly.

If the function has multiple aborts_if conditions, these conditions will be connected with logical OR. Let’s look at the following function, this function does not exist in file balance.move, it is just an example:

public fun mul_div(x: u64, y: u64, z: u64): u64 {
    let r = x * y / z;
    r
}

This function is very simple, first multiply and then divide, and return the final result.
It is easy to observe two conditions where the program would abort:

  • The divisor z cannot be equal to 0

  • x * ycannot be greater than the upper limit of u64
    So its termination condition should be like this:

    spec mul_div {
    aborts_if z == 0;
    aborts_if x * y > MAX_U64;
}

    The MAX_u64 is a built-in variable in the Move Specification Language (MSL), representing the maximum upper limit of u64, and also includes MAX_U128. One thing worth noting: For example, the expression a + b > MAX_U64 is problematic in the Move program. Because the addition on the left may cause an overflow exception. If we want to write a similar check in the Move program, we should use an expression like a > MAX_U64 - b to avoid the overflow problem.

However, this expression is perfectly fine in Move Specification Language (MSL). Since the spec block uses the MSL language, its type system is different from Move. In MSL, all integers are of type num, which is an integer in the mathematical sense. That is, it is signed and has no size limit. When referencing data of a Move program in MSL, all built-in integer types ( u8，u64 ) are automatically converted to the num type. A more detailed description of the type of system can be found in the MSL documentation.

As mentioned earlier, if we don’t specify any abort conditions, Prover will not impose any restrictions on aborts.

But once we give any abort condition, Prover defaults that we want to strictly check all possible aborts, so we need to list all possible conditions, which is equivalent to implicitly adding the instruction pragma aborts_if_is_strict. If only some of the conditions for abnormal exit are listed, Prover will report a verification error. However, if pragma aborts_if_is_partial is defined in the spec block, it is equivalent to telling the Prover:

‘ I just want to list some of the conditions that will cause an abort, please just verify if it will abort under these conditions. ’

If you are interested, you can do such a set of experiments to verify:

  • When any one of the above two conditions aborts_if is deleted, Prover will report an error;

  • When all conditions aborts_if are deleted at the same time, Prover will not report an error;

  • When pragma aborts_if_is_partial is added, no matter how many conditions aborts_if are kept, Prover will not report an error (Of course! the conditions themselves must be correct).

For a more detailed understanding, you can refer to the MSL documentation for more information.

Specifies the functional nature of decrease_supply

Next, we define functional properties. The below two statements ensures in the spec block gives us the functional expectation of decrease_supply :

spec decrease_supply {
    let value = balance.value;
    aborts_if self.value < value with EOverflow;

    let old_value = self.value;
    let post new_value = self.value;
    ensures new_value == old_value - value;
    ensures result == balance.value;
}

In this code, firstly using let post to define new_value as value of self after executing the function, which should be equal to self.value minus balance.value before function execution. Then, result is a special name and represents the return value, that is balance.value .

The above spec block can also be replaced with the following:

spec decrease_supply {
    let value = balance.value;
    aborts_if self.value < value with EOverflow;

    ensures self.value == old(self.value) - value;
    ensures result == balance.value;
}

It can be seen that we have deleted the definitions of the two variables old_value and new_value, because ensures means that the function has been executed, so self.value which is after ensures means that the value has been subtracted from balance.value, old() Represents the value before the function is executed, so self.value is equivalent to the above new_value, and old(self.value) is equivalent to the above old_value.

Use Schema to Simplify Redundant Specifications

Congratulations! So far, we have completed the termination conditions and property verification of some functions step by step. But there is a problem. Take function mul_div as an example. If another function calls function mul_div, how should the spec of this function be written? For example, the following function foo, the function foo , and mul_div both do not exist in balance.move, just a simple example is written for ease of illustration:

public fun mul_div(x: u64, y: u64, z: u64): u64 {
    let r = x * y / z;
    r
}

public fun foo(a: u64, b: u64, c: u64): u64 {
    let r = mul_div(a,b,c);
    r
}

First of all, it is certain that the function foo will also have the termination condition and properties of the function mul_div. If you want to write the spec of foo, it is actually simple, just write the spec of mul_div in foo one more time, for example:

spec mul_div {
    aborts_if z == 0;
    aborts_if x * y > MAX_U64;
}

spec foo {
    aborts_if c == 0;
    aborts_if a * b > MAX_U64;
}

The verification logic of the above two functions is basically the same, but it will be very cumbersome to write them separately, especially since many modules in the project will call each other, and the same function may be called by multiple functions of different modules, which is obviously not a reasonable way to write all of this function specs. We hope to make them more concise so that the file structure will be clearer.

Schema is a means of building specifications by grouping attributes. Semantically, they are also syntactic sugar and used in spec blocks which is equivalent to expanding the conditions they contain to functions, structs, or modules.

As the most obvious example, the spec blocks of mul_div and foo are slightly different except for the variable names, the overall structure can be said to be exactly the same. To simplify them, let’s create a Schema:

spec schema MulDivSchema {
    x: u64;
    y: u64;
    z: u64;

    aborts_if z == 0;
    aborts_if x * y > MAX_U64;
}

This Schema declares three types of variables and some conditions that these variables should meet. When you want to use this Schema in other places, you need to use include MulDivSchema{x: XX, y: YY, z: ZZ}; to import it. Among them, XX , YY , and ZZ are respectively the three parameters passed into the Schema. If the expression is exactly the same as the corresponding variable name, you can write the variable name, or omit it directly, but there is one thing to note: the function parameters in the move code can be directly passed to the Schema as parameters, but the variables defined in the function cannot be passed in directly.

With the above Schema definition, we can now simplify the previous spec:

spec mul_div {
    include MulDivSchema;
}

spec foo {
    include MulDivSchema{x: a, y: b, z: c};
}

Practice

  1. In addition to the above example, find another spec block (such as decrease_supply ), and split it into a Schema declaration and a spec block that uses the corresponding Schema. As an exercise, the Schema you create may not be available in this code, It seems like there is no any benefit. But it will be more convenient if other functions call decrease_supply in later development.

  2. We have submitted the specs of the functions increase_supply and decrease_supply in the above example to the PR list of the Sui Official Codebase ( https://github.com/MystenLabs/sui/pull/7440 ), and there are still relatively few specs in the Sui-Framework official codebase. We also call on everyone to find some functions in Sui-Framework and try to write specs by themselves. If they can run successfully, you can submit them to the PR list of the Sui Official Codebase. We believe this will make you feel more fulfilled.

Conclusion

So far, we have introduced in detail how to use the Move Prover for Formal Verification to provide protection for the security of smart contracts, and we have also initially realized the power of Move Prover.

More and more developers are developing Move applications and deploying Move contracts on the Move ecosystem. We strongly recommend using Move Prover and other contract auditing tools to audit the application before launching the Move DApp. If you need help with the Move contract audit, please contact us (https://www.movebit.xyz/) !

MoveBit

MoveBit is a blockchain security company focused on the Move Ecosystem. The team consists of security professionals from academia and enterprise with 10 years of security experience. they were one of the earliest contributors to the Move ecosystem, working with Move developers to set the standard for secure Move applications and make the Move ecosystem the most secure Web3 destination.

MoveBit Social Media Platforms:

Official Website: https://www.movebit.xyz/

Twitter: https://twitter.com/MoveBit_

GitHub: https://github.com/movebit

Discord: https://discord.com/invite/7wM8VU9Gyj

OLDER > < NEWER
Copyright © MoveBit 2022