SMTCheckerと形式検証

形式検証は、ソースコードがある形式的な仕様を満たしていることを、自動的に数学的に証明することを可能にします。 仕様はソースコードと同様に形式的なものですが、通常はよりシンプルなものになります。

形式検証は、「何をしたか（仕様）」と「どのようにしたか（実際の実装）」の違いを理解するためのものでしかないことに注意してください。 仕様が望んだものになっているかどうか、意図しない挙動を見逃していないかどうかをチェックする必要は依然としてあります。

Solidityでは、 SMT (Satisfiability Modulo Theories) と Horn の解法に基づいた形式的な検証アプローチを実装しています。 SMTCheckerモジュールは、 require 文と assert 文で与えられた仕様をコードが満たしていることを自動的に証明しようとします。 つまり、 require 文を仮定とみなし、 assert 文の中の条件が常に真であることを証明しようとします。 アサーションの失敗が発見された場合、アサーションがどのように破られるかを示す反例がユーザーに与えられます。 SMTCheckerがあるプロパティに対して警告を出さない場合、そのプロパティは安全であることを意味します。

SMTCheckerがコンパイル時にチェックするその他の検証対象は以下の通りです。

• 算術演算のアンダーフローとオーバーフロー。

• ゼロによる除算。

• トリビアルな条件と到達不可能なコード。

• 空の配列に対するポップ。

• 範囲外のインデックスアクセス。

• 送金に必要な資金の不足。

上記のターゲットは、Solidity >=0.8.7のunderflowとoverflowを除き、すべてのエンジンが有効な場合、デフォルトで自動的にチェックされます。

SMTCheckerが報告する潜在的な警告は次のとおりです。

• <failing  property> happens here これは、SMTCheckerがあるプロパティが失敗することを証明したことを意味します。 反例が示されることもありますが、複雑な状況では反例が示されないこともあります。 この結果は、SMTエンコーディングが、表現が困難または不可能なSolidityコードの抽象化を追加する場合、特定のケースでは誤検出となることもあります。

• <failing property> might happen here これは、ソルバーが与えられたタイムアウト内にどちらのケースも証明できなかったことを意味します。 結果は不明なので、SMTCheckerは健全性のために潜在的な失敗を報告します。 これは、クエリのタイムアウトを増やすことで解決できるかもしれませんが、問題が単にエンジンにとって難しすぎるだけかもしれません。

SMTCheckerを有効にするには、デフォルトではエンジンなしとなっている 実行するエンジン を選択する必要があります。 エンジンを選択すると、すべてのファイルでSMTCheckerが有効になります。

注釈

Solidity 0.8.4以前では、SMTCheckerを有効にするデフォルトの方法は pragma experimental SMTChecker; を介したもので、プラグマを含むコントラクトのみが分析されました。 このプラグマは非推奨となっており、後方互換性のためにSMTCheckerを有効にしていますが、Solidity 0.9.0では削除されます。 また、1つのファイルでもプラグマを使用すると、すべてのファイルでSMTCheckerが有効になることに注意してください。

注釈

検証対象に対して警告が出ないということは、SMTCheckerや基盤となるソルバーにバグがないことを前提とした、議論の余地のない正しさの数学的証明を意味します。 これらの問題は、一般的なケースで自動的に解決することは 非常に難しく 、時には 不可能 であることに留意してください。 したがって、いくつかの特性は解決できないかもしれませんし、大規模なコントラクトでは誤検出につながるかもしれません。 すべての証明されたプロパティは重要な成果であると考えるべきです。 上級者向けには、 SMTChecker Tuning を参照して、より複雑なプロパティを証明するのに役立ついくつかのオプションを学んでください。

チュートリアル

オーバーフロー

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Overflow {
    uint immutable x;
    uint immutable y;

    function add(uint x_, uint y_) internal pure returns (uint) {
        return x_ + y_;
    }

    constructor(uint x_, uint y_) {
        (x, y) = (x_, y_);
    }

    function stateAdd() public view returns (uint) {
        return add(x, y);
    }
}

上のコントラクトではオーバーフローチェックの例を示しています。 SMTCheckerはSolidity >=0.8.7ではデフォルトでアンダーフローとオーバーフローをチェックしないので、コマンドラインオプション --model-checker-targets "underflow,overflow" またはJSONオプション settings.modelChecker.targets = ["underflow", "overflow"] を使用する必要があります。 this section for targets configuration を参照してください。 ここでは、以下のように報告しています。

Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
x = 1, y = 115792089237316195423570985008687907853269984665640564039457584007913129639935
 = 0

Transaction trace:
Overflow.constructor(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
State: x = 1, y = 115792089237316195423570985008687907853269984665640564039457584007913129639935
Overflow.stateAdd()
    Overflow.add(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call
 --> o.sol:9:20:
  |
9 |             return x_ + y_;
  |                    ^^^^^^^

オーバーフローのケースをフィルタリングする require 文を追加すると、SMTCheckerはオーバーフローに到達しないことを（警告を報告しないことで）証明します。

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Overflow {
    uint immutable x;
    uint immutable y;

    function add(uint x_, uint y_) internal pure returns (uint) {
        return x_ + y_;
    }

    constructor(uint x_, uint y_) {
        (x, y) = (x_, y_);
    }

    function stateAdd() public view returns (uint) {
        require(x < type(uint128).max);
        require(y < type(uint128).max);
        return add(x, y);
    }
}

アサート

アサーションとは、コードの不変性を表すもので、すべての入力値と保存値を含むすべてのトランザクションに対して*真でなければならないプロパティで、そうでなければバグがあることになります。

以下のコードでは、オーバーフローしないことを保証する関数 f を定義しています。 関数 inv は、 f が単調増加であるという仕様を定義しています: すべての可能なペア (a, b) に対して、もし b > a ならば f(b) > f(a) です。 f は確かに単調増加なので、SMTCheckerは我々の特性が正しいことを証明します。 この性質と関数の定義を使って、どんな結果が出るか試してみてください。

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Monotonic {
    function f(uint x) internal pure returns (uint) {
        require(x < type(uint128).max);
        return x * 42;
    }

    function inv(uint a, uint b) public pure {
        require(b > a);
        assert(f(b) > f(a));
    }
}

また、ループの中にアサーションを追加して、より複雑なプロパティを検証することもできます。 次のコードでは、制限のない数値の配列の最大要素を検索し、検索された要素は配列のすべての要素と同じかそれ以上でなければならないというプロパティをアサートしています。

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Max {
    function max(uint[] memory a) public pure returns (uint) {
        uint m = 0;
        for (uint i = 0; i < a.length; ++i)
            if (a[i] > m)
                m = a[i];

        for (uint i = 0; i < a.length; ++i)
            assert(m >= a[i]);

        return m;
    }
}

この例では、SMTCheckerは自動的に3つのプロパティを証明しようとすることに注意してください。

1. 最初のループの ++i はオーバーフローしません。

2. 2つ目のループの ++i はオーバーフローしません。

3. アサーションは常に真です。

注釈

プロパティにはループが含まれているため、これまでの例よりも*はるかに*難しくなっていますので、ループにご注意ください。

すべてのプロパティの安全性が正しく証明されています。 プロパティを変更したり、配列に制限を加えることで、異なる結果を得ることができます。 例えば、コードを次のように変更すると

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Max {
    function max(uint[] memory a) public pure returns (uint) {
        require(a.length >= 5);
        uint m = 0;
        for (uint i = 0; i < a.length; ++i)
            if (a[i] > m)
                m = a[i];

        for (uint i = 0; i < a.length; ++i)
            assert(m > a[i]);

        return m;
    }
}

が与えてくれます。

Warning: CHC: Assertion violation happens here.
Counterexample:

a = [0, 0, 0, 0, 0]
 = 0

Transaction trace:
Test.constructor()
Test.max([0, 0, 0, 0, 0])
  --> max.sol:14:4:
   |
14 |            assert(m > a[i]);

ステートのプロパティ

これまでの例では、特定の操作やアルゴリズムに関するプロパティを証明する、純粋なコードに対するSMTCheckerの使用方法を示しただけでした。 スマートコントラクトにおける一般的なプロパティの種類は、コントラクトの状態に関わるプロパティです。 このようなプロパティについてアサーションを失敗させるには、複数のトランザクションが必要になる場合があります。

例として、両軸の座標が(-2^128, 2^128 - 1)の範囲にある2Dグリッドを考えてみましょう。 ここで、ロボットを(0, 0)の位置に置きます。 ロボットは対角線上に1歩ずつしか移動できず、グリッドの外には出られません。 このロボットのステートマシンは、以下のスマートコントラクトで表すことができます。

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Robot {
    int x = 0;
    int y = 0;

    modifier wall {
        require(x > type(int128).min && x < type(int128).max);
        require(y > type(int128).min && y < type(int128).max);
        _;
    }

    function moveLeftUp() wall public {
        --x;
        ++y;
    }

    function moveLeftDown() wall public {
        --x;
        --y;
    }

    function moveRightUp() wall public {
        ++x;
        ++y;
    }

    function moveRightDown() wall public {
        ++x;
        --y;
    }

    function inv() public view {
        assert((x + y) % 2 == 0);
    }
}

関数 inv は、 x + y が偶数でなければならないというステートマシンの不変量を表しています。 SMTCheckerは、ロボットにどんなに多くの命令を与えても、たとえ無限に与えても、不変量は*絶対に*失敗しないことを証明できます。 興味のある方は、手動でこの事実を証明することもできます。 ヒント: この不変量は帰納的なものです。

また、SMTCheckerを騙して、到達可能と思われるある位置までのパスを教えてもらうこともできます。 次のような関数を追加することで、(2, 4)は*not* reachableであるという性質を追加できます。

open in Remix

function reach_2_4() public view {
    assert(!(x == 2 && y == 4));
}

この性質は偽であり、SMTCheckerはこの性質が偽であることを証明しながら、(2, 4)に到達する方法を正確に*教えてくれます。

Warning: CHC: Assertion violation happens here.
Counterexample:
x = 2, y = 4

Transaction trace:
Robot.constructor()
State: x = 0, y = 0
Robot.moveLeftUp()
State: x = (- 1), y = 1
Robot.moveRightUp()
State: x = 0, y = 2
Robot.moveRightUp()
State: x = 1, y = 3
Robot.moveRightUp()
State: x = 2, y = 4
Robot.reach_2_4()
  --> r.sol:35:4:
   |
35 |            assert(!(x == 2 && y == 4));
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^

なお、上の経路は必ずしも決定論的ではなく、(2, 4)に到達する経路は他にもあるので注意が必要です。 どの経路を表示するかは、使用するソルバーやそのバージョンによって変わるかもしれませんし、ランダムに表示されるかもしれません。

外部呼び出しとReentrancy

すべての外部呼び出しは、SMTCheckerによって未知のコードへの呼び出しとして扱われます。 その理由は、たとえ呼び出されたコントラクトのコードがコンパイル時に利用可能であったとしても、デプロイされたコントラクトが実際にコンパイル時にインターフェースの元となったコントラクトと同じであるという保証はないからです。

場合によっては、外部から呼び出されたコードが呼び出し元のコントラクトを再入力するなど、何をしても真である状態変数のプロパティを自動的に推論することも可能です。

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

interface Unknown {
    function run() external;
}

contract Mutex {
    uint x;
    bool lock;

    Unknown immutable unknown;

    constructor(Unknown u) {
        require(address(u) != address(0));
        unknown = u;
    }

    modifier mutex {
        require(!lock);
        lock = true;
        _;
        lock = false;
    }

    function set(uint x_) mutex public {
        x = x_;
    }

    function run() mutex public {
        uint xPre = x;
        unknown.run();
        assert(xPre == x);
    }
}

上の例では、ミューテックスフラグを使用して再入を禁止したコントラクトを示しています。 ソルバーは、 unknown.run() が呼び出されたとき、コントラクトはすでに「ロック」されているので、未知の呼び出されたコードが何をしようと、 x の値を変更できないだろうと推測できます。

関数 set に mutex モディファイアを使うことを「忘れた」場合、SMTCheckerは外部から呼び出されたコードの振る舞いを合成し、アサーションが失敗するようにします。

Warning: CHC: Assertion violation happens here.
Counterexample:
x = 1, lock = true, unknown = 1

Transaction trace:
Mutex.constructor(1)
State: x = 0, lock = false, unknown = 1
Mutex.run()
    unknown.run() -- untrusted external call, synthesized as:
        Mutex.set(1) -- reentrant call
  --> m.sol:32:3:
   |
32 |                assert(xPre == x);
   |                ^^^^^^^^^^^^^^^^^

SMTCheckerのオプションとチューニング

タイムアウト

SMTCheckerでは、ソルバーごとに選択されたハードコードされたリソース制限（ rlimit ）を使用していますが、これは時間とは正確には関係ありません。 rlimit オプションをデフォルトとして選択したのは、ソルバー内部の時間よりも決定性の保証が得られるからです。

このオプションを大まかに説明すると、1回のクエリにつき「数秒のタイムアウト」となります。 もちろん、多くのプロパティは非常に複雑で、決定論が問題にならないような解決に多くの時間を必要とします。 SMTCheckerがデフォルトの rlimit でコントラクトプロパティを解決できない場合、CLIオプション --model-checker-timeout <time> またはJSONオプション settings.modelChecker.timeout=<time> を介して、ミリ秒単位でタイムアウトを与えることができます。

検証ターゲット

SMTCheckerによって作成される検証ターゲットの種類は、CLIオプション --model-checker-target <targets> またはJSONオプション settings.modelChecker.targets=<targets> によってカスタマイズすることもできます。 CLIの場合、 <targets> は1つまたは複数の検証ターゲットのスペースなしコンマ区切りのリストで、JSON入力では1つまたは複数のターゲットを文字列として配列します。 ターゲットを表すキーワードは

• アサーション: assert 。

• 算術アンダーフロー: underflow 。

• 算術オーバーフロー: overflow 。

• ゼロによる除算: divByZero 。

• トリビアルな条件と到達不可能なコード: constantCondition 。

• 空の配列のポップ: popEmptyArray 。

• 境界を越えた配列/固定バイトのインデックスアクセス: outOfBounds 。

• 送金に必要な資金が不足しています: balance 。

• 上記の全てです: default （CLIのみ）。

ターゲットの一般的なサブセットは、例えば次のようなものです: --model-checker-targets assert,overflow 。

デフォルトではすべてのターゲットがチェックされますが、Solidity >=0.8.7ではアンダーフローとオーバーフローがチェックされます。

検証対象をいつ、どのように分割するかについての正確なヒューリスティックはありませんが、特に大規模なコントラクトを扱う場合には有効です。

証明されたターゲット

証明されたターゲットがある場合、SMTCheckerはエンジンごとに、証明されたターゲットの数を示す警告を1回発行します。 もしユーザーが証明されたターゲットをすべて見たい場合は、CLIオプション --model-checker-show-proved とJSONオプション settings.modelChecker.showProved = true を使用できます。

証明されていないターゲット

証明されていないターゲットがある場合、SMTCheckerは証明されていないターゲットの数を示す1つの警告を発行します。 ユーザーが特定の未処理のターゲットをすべて表示したい場合は、CLIオプション --model-checker-show-unproved およびJSONオプション settings.modelChecker.showUnproved = true を使用できます。

未サポートの言語機能

SMTCheckerが適用するSMTエンコーディングでは、Solidity 言語の一部の機能が完全にサポートされていません（例えば、アセンブリブロック）。 サポートされていない構成は、健全性を保つために過近接によって抽象化されます。 つまり、この機能がサポートされていなくても、安全と報告されたプロパティは安全です。 しかし、このような抽象化は、対象となるプロパティがサポートされていない機能の正確な動作に依存している場合、誤検出を引き起こす可能性があります。 エンコーダがこのようなケースに遭遇した場合、デフォルトでは、サポートされていない機能をいくつ見たかを示す一般的な警告を報告することになります。 もしユーザーがサポートされていない機能をすべて見たい場合は、CLIオプション --model-checker-show-unsupported とJSONオプション settings.modelChecker.showUnsupported = true を使用できます（デフォルト値は false です）。

検証されたコントラクト

デフォルトでは、指定されたソース内のすべてのデプロイ可能なコントラクトが、デプロイされるものとして個別に分析されます。 これは、コントラクトが多くの直接および間接的な継承親を持つ場合、最も派生したものだけがブロックチェーン上で直接アクセスされるにもかかわらず、それらすべてが単独で分析されることを意味します。 これは、SMTCheckerとソルバーに不必要な負担をかけることになります。 このようなケースを支援するために、ユーザーはどのコントラクトをデプロイされたものとして分析すべきかを指定できます。 親コントラクトはもちろんまだ分析されますが、最も派生したコントラクトのコンテキストでのみ分析され、エンコーディングと生成されたクエリの複雑さが軽減されます。 抽象コントラクトはデフォルトではSMTCheckerによって最も派生したものとして分析されないことに注意してください。

選択されたコントラクトは、CLI: --model-checker-contracts "<source1.sol:contract1>,<source2.sol:contract2>,<source2.sol:contract3>" では<source>: <contract>のペアのコンマ区切りリスト（空白は許されない）を介して、 JSON input ではオブジェクト settings.modelChecker.contracts を介して、次のような形式で与えられます。

"contracts": {
    "source1.sol": ["contract1"],
    "source2.sol": ["contract2", "contract3"]
}

信頼した外部呼び出し

デフォルトでは、SMTCheckerは、コンパイル時に利用可能なコードと外部呼び出しの実行時コードが同じであることを想定していません。 次のコントラクトを例にとります:

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Ext {
    uint public x;
    function setX(uint _x) public { x = _x; }
}
contract MyContract {
    function callExt(Ext _e) public {
        _e.setX(42);
        assert(_e.x() == 42);
    }
}

MyContract.callExt が呼び出されると、引数としてアドレスが与えられます。 デプロイ時には、アドレス _e が実際にコントラクト Ext のデプロイメントを含んでいるかどうかを確実に知ることはできません。 したがって、SMTChecker は、 _e に Ext 以外のコントラクトが含まれている場合、上記のアサーションに違反する可能性があることを警告します（これは真です）。

しかし、例えば、あるインターフェースの異なる実装が同じプロパティに適合しているかどうかをテストするために、これらの外部呼び出しを信頼できるものとして扱うことが有用な場合があります。 これは、アドレス _e が本当にコントラクト Ext としてデプロイされたと仮定することを意味します。 このモードはCLIオプション --model-checker-ext-calls=trusted またはJSONフィールド settings.modelChecker.extCalls: "trusted" で有効にできます。

このモードを有効にすると、SMTCheckerの解析に計算コストがかかることに注意してください。

このモードの重要な点は、コントラクトタイプとコントラクトへの高レベルの外部呼び出しに適用され、 call や delegatecall などの低レベルの呼び出しには適用されないという点です。 アドレスの保存はコントラクトタイプごとに行われ、SMTCheckerは外部から呼び出されたコントラクトは呼び出し元の式のタイプを持つと仮定しています。 したがって、 address やコントラクトを異なるコントラクト型にキャストすると、異なるストレージ値が得られ、以下の例のように仮定が矛盾している場合、健全でない結果を与えることがあります:

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract D {
    constructor(uint _x) { x = _x; }
    uint public x;
    function setX(uint _x) public { x = _x; }
}

contract E {
    constructor() { x = 2; }
    uint public x;
    function setX(uint _x) public { x = _x; }
}

contract C {
    function f() public {
        address d = address(new D(42));

        // `d` was deployed as `D`, so its `x` should be 42 now.
        assert(D(d).x() == 42); // should hold
        assert(D(d).x() == 43); // should fail

        // E and D have the same interface, so the following
        // call would also work at runtime.
        // However, the change to `E(d)` is not reflected in `D(d)`.
        E(d).setX(1024);

        // Reading from `D(d)` now will show old values.
        // The assertion below should fail at runtime,
        // but succeeds in this mode's analysis (unsound).
        assert(D(d).x() == 42);
        // The assertion below should succeed at runtime,
        // but fails in this mode's analysis (false positive).
        assert(D(d).x() == 1024);
    }
}

以上のことから、 address 型や contract 型の特定の変数に対する信頼できる外部呼び出しは、常に同じ呼び出し元の式の型を持つようにします。

また、継承の場合には、呼び出されたコントラクトの変数を最も派生した型の型としてキャストすることが有効です。

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

interface Token {
    function balanceOf(address _a) external view returns (uint);
    function transfer(address _to, uint _amt) external;
}

contract TokenCorrect is Token {
    mapping (address => uint) balance;
    constructor(address _a, uint _b) {
        balance[_a] = _b;
    }
    function balanceOf(address _a) public view override returns (uint) {
        return balance[_a];
    }
    function transfer(address _to, uint _amt) public override {
        require(balance[msg.sender] >= _amt);
        balance[msg.sender] -= _amt;
        balance[_to] += _amt;
    }
}

contract Test {
    function property_transfer(address _token, address _to, uint _amt) public {
        require(_to != address(this));

        TokenCorrect t = TokenCorrect(_token);

        uint xPre = t.balanceOf(address(this));
        require(xPre >= _amt);
        uint yPre = t.balanceOf(_to);

        t.transfer(_to, _amt);
        uint xPost = t.balanceOf(address(this));
        uint yPost = t.balanceOf(_to);

        assert(xPost == xPre - _amt);
        assert(yPost == yPre + _amt);
    }
}

関数 property_transfer では、外部呼び出しは変数 t に対して行われることに注意してください。

このモードのもう一つの注意点は、解析されたコントラクト以外のコントラクトタイプの状態変数への呼び出しです。 以下のコードでは、 B が A をデプロイしているにもかかわらず、 B.a に格納されているアドレスが、 B 自身へのトランザクションの合間に、 B 以外の誰かによって呼び出される可能性もあります。 B.a に起こりうる変更を反映するために、エンコーディングは外部から B.a を無制限に呼び出すことができるようにします。 エンコーディングは B.a のストレージを追跡するので、アサーション(2)が成立するはずです。 しかし、現在のエンコーディングでは、このような呼び出しは概念的に B から行うことができるので、アサーション(3)は失敗します。 エンコーディングを論理的に強くすることは、トラステッドモードの拡張であり、現在開発中です。 もし B.a が address 型を持つ場合、エンコーディングは B へのトランザクションの間にそのストレージが変更されないと仮定します。

open in Remix

pragma solidity >=0.8.0;

contract A {
    uint public x;
    address immutable public owner;
    constructor() {
        owner = msg.sender;
    }
    function setX(uint _x) public {
        require(msg.sender == owner);
        x = _x;
    }
}

contract B {
    A a;
    constructor() {
        a = new A();
        assert(a.x() == 0); // (1) should hold
    }
    function g() public view {
        assert(a.owner() == address(this)); // (2) should hold
        assert(a.x() == 0); // (3) should hold, but fails due to a false positive
    }
}

報告された推論された帰納的な不変量

CHCエンジンで安全性が証明された性質については、SMTCheckerは証明の一部としてHornソルバーによって推論された帰納的不変量を取得できます。 現在、2種類のみの不変量をユーザに報告できます。

• コントラクト不変量: コントラクトの状態変数に関するプロパティで、コントラクトが実行する可能性のあるすべてのトランザクションの前後で真となるものです。 例えば、 x と y がコントラクトの状態変数である場合、 x >= y となります。

• 再帰性プロパティ: 未知のコードへの外部呼び出しがある場合のコントラクトの動作を表します。 これらのプロパティは、外部呼び出しの前と後の状態変数の値の間の関係を表現できます。 外部呼び出しは、分析されたコントラクトへのリエントラントな呼び出しを行うことを含め、何でも自由に行うことができます。 プライム化された変数は、前記外部呼び出し後の状態変数の値を表します。 例: lock -> x = x' 。

ユーザーは、CLIオプション --model-checker-invariants "contract,reentrancy" を使用して、または JSON input のフィールド settings.modelChecker.invariants で配列として報告される不変量の型を選択できます。 デフォルトでは、SMTCheckerはインバリアントを報告しません。

スラック変数を使った除算とモジュロ

SMTCheckerで使用されているデフォルトのHornソルバーであるSpacerは、Hornルール内の除算やモジュロ演算を嫌うことがあります。 そのため、デフォルトではSolidityの除算とモジュロ演算は a = b * d + m where d = a / b and m = a % b という制約を用いてエンコードされています。 しかし、Eldaricaのような他のソルバーは、構文的に正確な演算を好みます。 コマンドラインフラグ --model-checker-div-mod-no-slacks とJSONオプション settings.modelChecker.divModNoSlacks を使って、使用するソルバーの好みに応じてエンコーディングを切り替えることができます。

Natspec Function Abstraction

pow や sqrt などの一般的な数学手法を含む特定の関数は、完全に自動化された方法で分析するには複雑すぎる場合があります。 このような関数には、Natspecタグで注釈を付けることができます。 Natspecタグは、SMTCheckerに対して、これらの関数が抽象化されるべきであることを示します。 これは、関数の本体は使用されず、関数が呼び出されたときに

• 非決定論的な値を返し、抽象化された関数がview/pureであれば状態変数を変更せずに、そうでなければ状態変数を非決定論的な値に設定します。 これは、アノテーション /// @custom:smtchecker abstract-function-nondet を介して使用できます。

• 解釈されない関数として動作します。 これは、（ボディで与えられた）関数のセマンティクスが無視され、この関数が持つ唯一の特性は、同じ入力が与えられれば同じ出力が保証されるということです。 この関数は現在開発中で、アノテーション /// @custom:smtchecker abstract-function-uf から利用できるようになる予定です。

モデルチェックエンジン

SMTCheckerモジュールは、BMC（Bounded Model Checker）とCHC（Constrained Horn Clauses）という2種類の推論エンジンを実装しています。 両エンジンは現在開発中であり、それぞれ異なる特徴を持っています。 これらのエンジンは独立しており、すべてのプロパティの警告は、それがどのエンジンから来たかを示しています。 なお、上記の反例のある例はすべて、より強力なエンジンであるCHCから報告されています。

デフォルトでは、両方のエンジンが使用され、CHCが最初に実行され、証明されなかったすべてのプロパティがBMCに渡されます。 特定のエンジンを選択するには、CLIオプション --model-checker-engine {all,bmc,chc,none} またはJSONオプション settings.modelChecker.engine={all,bmc,chc,none} を使用します。

Bounded Model Checker (BMC)

BMCエンジンは、関数を単独で解析します。 つまり、各関数を解析する際に、複数のトランザクションにわたるコントラクトの全体的な動作を考慮しません。 ループも現時点ではこのエンジンでは無視されます。 内部の関数呼び出しは、直接的または間接的に再帰的でない限りインライン化されます。 外部関数呼び出しは可能な限りインライン化されます。 再帰性の影響を受ける可能性のある知識は消去されます。

上記のような特性から、BMCは誤検出を報告する傾向がありますが、軽量であるため、小さなローカルバグを素早く発見できるはずです。

Constrained Horn Clauses (CHC)

コントラクトのコントロールフローグラフ（CFG）は、Horn節のシステムとしてモデル化されており、コントラクトのライフサイクルは、すべてのpublic/external関数を非決定的に訪れることができるループで表現されています。 このようにして、任意の関数を解析する際には、無制限の数のトランザクションにおけるコントラクト全体の動作が考慮されます。 ループはこのエンジンで完全にサポートされています。 internal関数の呼び出しはサポートされており、external関数の呼び出しは、呼び出されたコードが未知であり、何でもできると仮定します。

CHCエンジンは、BMCよりも証明できる内容がはるかに多く、より多くの計算資源を必要とする可能性があります。

SMTソルバーとHornソルバー

上記の2つのエンジンは、自動定理証明器を論理的バックエンドとして使用しています。 BMCはSMTソルバーを使用し、CHCはHornソルバーを使用しています。 SMTソルバーを主とし、 Spacer をHornソルバーとして利用可能な z3 や、両方の機能を持つ Eldarica のように、同じツールが両方の役割を果たすこともよくあります。

ユーザーは、使用可能な場合、どのソルバーを使用するかを、CLIオプション --model-checker-solvers {all,cvc4,eld,smtlib2,z3} またはJSONオプション settings.modelChecker.solvers=[smtlib2,z3] で選択できます。

• cvc4 は、 solc のバイナリがコンパイルされている場合にのみ使用できます。 cvc4 を使うのはBMCだけです。

• eld は、システムにインストールされている必要があるバイナリを介して使用されます。 CHCだけが eld を使用し、 z3 が有効でない場合にのみ使用します。

• smtlib2 はSMT/Hornのクエリを smtlib2 形式で出力します。 これをコンパイラの コールバックメカニズム と併用することで、システム内の任意のソルバーバイナリを採用して、クエリの結果をコンパイラに同期して返すことができます。 これは、どのソルバーを呼び出すかによって、BMCとCHCの両方で使用できます。

• 以下の場合 z3 が使えます。

  • solc がz3とともにコンパイルされている場合。

  • Linuxシステムにバージョン>=4.8.xの動的 z3 ライブラリがインストールされている場合（Solidity 0.7.6以降）。

  • soljson.js （Solidity 0.6.9 以降）では静的に、つまりコンパイラのJavaScriptバイナリを使用しています。

注釈

z3バージョン4.8.16は、以前のバージョンとのABI互換性を壊し、solc <=0.8.13で使用できません。 もしz3 >=4.8.16を使用しているならば、solc>=0.8.14を使用してください。 逆に、古いz3は古いsolcリリースとしか使用できません。 また、SMTCheckerも最新のz3リリースを使用することをお勧めします。

BMCもCHCも z3 を採用しており、 z3 はブラウザを含めてより多様な環境で利用できるため、ほとんどのユーザーはこのオプションを気にする必要はないでしょう。 上級者であれば、より複雑な問題に対して別のソルバーを試すためにこのオプションを適用するかもしれません。

なお、選択したエンジンとソルバーの組み合わせによっては、SMTCheckerが何もしない場合があります。 例えば、CHCと cvc4 を選択した場合などです。

抽象化と偽陽性

SMTCheckerは、抽象化を不完全かつ健全な方法で実装しています。 バグが報告された場合、それは抽象化によってもたらされた誤検出である可能性があります（知識を消去したり、正確でない型を使用したため）。 検証対象が安全であると判断された場合、それは確かに安全であり、つまり（SMTCheckerにバグがない限り）偽陰性は存在しないのです。

ターゲットが証明できない場合は、前のセクションのチューニングオプションを使ってソルバーを助けることができます。 誤検出が確実な場合は、より多くの情報を含む require 文をコードに追加することで、ソルバーにさらなる力を与えることもできます。

SMTエンコーディングと型

SMTCheckerのエンコーディングは可能な限り正確を期しており、Solidityの型や表現を下の表のように最も近い SMT-LIB 表現にマッピングしています。

Solidityの型	SMT sort	Theories
Boolean	Bool	Bool
intN, uintN, address, bytesN, enum, contract	Integer	LIA, NIA
array, mapping, bytes, string	Tuple (Array elements, Integer length)	Datatypes, Arrays, LIA
struct	Tuple	Datatypes
他の型	Integer	LIA

まだサポートされていない型は、1つの256ビットの符号なし整数で抽象化され、サポートされていない操作は無視されます。

SMTエンコーディングの内部動作の詳細については、論文 SMT-based Verification of Solidity Smart Contracts を参照してください。

関数呼び出し

BMCエンジンでは、同じコントラクト（またはベースコントラクト）の関数呼び出しは、可能な場合、つまりその実装が利用可能な場合にインライン化されます。 他のコントラクトの関数の呼び出しは、そのコードが利用可能であってもインライン化されません。 これは、実際にデプロイされたコードが同じであることを保証できないからです。

CHCエンジンは、内部関数の呼び出しをサポートするために、呼び出された関数のサマリーを使用する非線形Horn句を作成します。 外部関数呼び出しは、リエントラント呼び出しの可能性も含め、未知のコードへの呼び出しとして扱われます。

複雑な純関数は、引数上の解釈されない関数（UF）によって抽象化されます。

関数	BMC/CHCの挙動
assert	Verification target.
require	仮定
internalコール	BMC: Inline function call. CHC: Function summaries.
既知のコードへのexternalコール	BMC: Inline function call or erase knowledge about state variables and local storage references. CHC: Assume called code is unknown. Try to infer invariants that hold after the call returns.
Storage array push/pop	Supported precisely. Checks whether it is popping an empty array.
ABI関数	Abstracted with UF.
addmod, mulmod	Supported precisely.
gasleft, blockhash, keccak256, ecrecover ripemd160	Abstracted with UF.
pure functions without implementation (external or complex)	Abstracted with UF
external functions without implementation	BMC: Erase state knowledge and assume result is nondeterminisc. CHC: Nondeterministic summary. Try to infer invariants that hold after the call returns.
transfer	BMC: Checks whether the contract's balance is sufficient. CHC: does not yet perform the check.
others	現在は未サポート

抽象化することは、正確な知識を失うことを意味しますが、多くの場合、証明力を失うことを意味しません。

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Recover
{
    function f(
        bytes32 hash,
        uint8 v1, uint8 v2,
        bytes32 r1, bytes32 r2,
        bytes32 s1, bytes32 s2
    ) public pure returns (address) {
        address a1 = ecrecover(hash, v1, r1, s1);
        require(v1 == v2);
        require(r1 == r2);
        require(s1 == s2);
        address a2 = ecrecover(hash, v2, r2, s2);
        assert(a1 == a2);
        return a1;
    }
}

上の例では、SMTCheckerは実際に ecrecover を計算するほどの表現力はありませんが、関数呼び出しを解釈されない関数としてモデル化することで、同等のパラメータで呼び出された場合に戻り値が同じであることがわかります。 このことは、上記の主張が常に真であることを証明するのに十分です。

関数呼び出しをUFで抽象化することは、決定論的であることが知られている関数に対しては可能であり、純粋な関数に対しても簡単に行うことができます。 しかし、一般の外部関数では、状態変数に依存する可能性があるため、これを行うことは困難です。

参照型とエイリアス

Solidityでは、同じ データロケーション を持つ参照型に対してエイリアスを実装しています。 つまり、ある変数が同じデータ領域への参照を通じて変更される可能性があるということです。 SMTCheckerは、どの参照が同じデータを参照しているかを追跡しません。 これは、参照型のローカル参照または状態変数が割り当てられるたびに、同じ型およびデータロケーションの変数に関するすべての知識が消去されることを意味します。 型が入れ子になっている場合、知識の消去には、すべての前置基底型も含まれます。

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Aliasing
{
    uint[] array1;
    uint[][] array2;
    function f(
        uint[] memory a,
        uint[] memory b,
        uint[][] memory c,
        uint[] storage d
    ) internal {
        array1[0] = 42;
        a[0] = 2;
        c[0][0] = 2;
        b[0] = 1;
        // Erasing knowledge about memory references should not
        // erase knowledge about state variables.
        assert(array1[0] == 42);
        // However, an assignment to a storage reference will erase
        // storage knowledge accordingly.
        d[0] = 2;
        // Fails as false positive because of the assignment above.
        assert(array1[0] == 42);
        // Fails because `a == b` is possible.
        assert(a[0] == 2);
        // Fails because `c[i] == b` is possible.
        assert(c[0][0] == 2);
        assert(d[0] == 2);
        assert(b[0] == 1);
    }
    function g(
        uint[] memory a,
        uint[] memory b,
        uint[][] memory c,
        uint x
    ) public {
        f(a, b, c, array2[x]);
    }
}

b[0] に割り当てられた後、 a については型（ uint[] ）とデータの場所（メモリ）が同じであるため、知識を消去する必要があります。 また、 c の基本型もメモリ上の uint[] であるため、 c に関する知識も消去する必要があります。 これは、ある c[i] が b や a と同じデータを参照する可能性があることを意味します。

array と d は、型が uint[] であっても、ストレージに配置されているため、知識を消去しないことに注意してください。 しかし、もし d が割り当てられていたら、 array に関する知識をクリアする必要があり、その逆もまた然りです。

コントラクト残高

コントラクトは、デプロイトランザクションにおいて msg.value > 0 であれば、資金を送ってデプロイされるかもしれません。 しかし、コントラクトのアドレスは、デプロイ前にすでに資金を持っている可能性があり、それはコントラクトによって保持されます。 そのため、SMTCheckerはEVMルールとの整合性を取るために、コンストラクタで address(this).balance >= msg.value を想定しています。 また、コントラクトの残高は、以下の場合、コントラクトへの呼び出しをトリガすることなく増加することがあります。

• selfdestruct は、分析されたコントラクトを残金の対象として、別のコントラクトで実行されます。

• コントラクトは、あるブロックのコインベース（＝ block.coinbase ）です。

これを適切にモデル化するために、SMTCheckerは、新しいトランザクションのたびに コントラクトの残高が少なくとも msg.value だけ増える可能性があると仮定しています。

実世界の仮定

SolidityやEVMでは表現できますが、実際には発生しないと思われるシナリオもあります。 そのようなケースの1つが、プッシュ時に動的ストレージの配列の長さがオーバーフローすることです。 push 操作が長さ2^256 - 1の配列に適用された場合、その長さは静かにオーバーフローします。 しかし、実際にはこのようなことは起こり得ません。 なぜなら、配列をそこまで成長させるために必要な演算を実行するには、何十億年もかかるからです。 SMTCheckerのもう一つの類似した仮定は、アドレスの残高がオーバーフローすることはないというものです。

同じようなアイデアが EIP-1985 でも紹介されていました。