介绍 Move 的形式化验证工具 Move Prover的基本用法。

形式化验证

Move 的形式化验证工具 Move Prover 可以对 Move 程序进行形式化验证。它可以自动证明 Move 智能合约是否符合其形式化规范，同时提供类似于类型检查器的用户体验。Move Prover的设计目标是使智能合约更具“可信赖性”：

• 保护由Starcoin区块链管理的大量资产免受智能合约漏洞的影响
• 有利于监管机构审查和合规要求
• 允许具有数学背景但不一定具有软件工程背景的领域专家了解智能合约的作用

安装

运行（在Starcoin根目录中）：

bash scripts/dev_setup.sh -t -y -p

目前仅支持在MacOS和Linux版本（如Ubuntu或CentOS）上运行。 -p 参数表示让 setup 脚本自动更新 .profile 文件，添加环境变量，也可以选择手动设置以下环境变量。

export DOTNET_ROOT=$HOME/.dotnet
export PATH=$HOME/.dotnet/tools:$PATH
export Z3_EXE=$HOME/bin/z3
export CVC4_EXE=$HOME/bin/cvc4
export BOOGIE_EXE=$HOME/.dotnet/tools/boogie

运行

通常是在 Starcoin源码环境中使用cargo run运行 Move Prover。 例如在当前目录中对arithm.move做形式化验证，需要告诉Move Prover在哪里 查找源文件的依赖（本例中 arithm.move 没有依赖）：

> cargo run --package move-prover -- --dependency . arithm.move

如果验证成功，Prover将打印一些统计信息，否则将打印错误诊断信息。 下面我们使用arithm.move来看一下如何对其进行形式化验证。首先，需要编写形式化规范。

/// arithm.move
module TestArithmetic {

    spec module {
        pragma verify = true;
        pragma aborts_if_is_strict = true;
    }

    fun arithmetic(x: u64, y: u64): u64 {
        (x + y) / x
    }
}

Move的形式化规范通常直接添加到源码里面。 pragma verify = true 用来告诉 Prover 需要验证 Module 中的所有方法。 pragma aborts_if_is_strict = true 告诉 Prover 必须严格检查所有退出条件。然后我们运行上面的命令就会输出如下错误信息：

abort happened here with execution failure

这说明有一些退出路径没有被规范覆盖到。可以通过添加下面的 aborts_if 退出条件来完善规范。规范添加完整后 Porver 将不再报错。

module TestArithmetic {

    spec module {
        pragma verify = true;
        pragma aborts_if_is_strict = true;
    }

    fun arithmetic(x: u64, y: u64): u64 {
        (x + y) / x
    }

    spec fun arithmetic {
        aborts_if x + y > max_u64();
        aborts_if x == 0;
    }
}

更多信息请参考下面的文档：

• Move智能合约的形式化验证工具
• Move Prover 用户指南
• Move 形式化规范语言