【入門編】 Echidnaを用いたプロパティベーステストによる不変条件の検証 – IoT・OT（制御システム） & ブロックチェーンセキュリティ防御ガイド

こんにちは！スマートコントラクトの開発に挑戦している皆さん、日々のコーディングお疲れ様です。「自分が書いたコードにバグはないはず！」と意気込んでデプロイした矢先、ハッカーにプール金の全額をきれいさっぱり抜き取られてしまった……そんな冷や汗が出るようなニュース、Web3の世界では後を絶ちませんよね。

従来のテスト（「この関数に 10 を入れたら 20 が返るはず」という単体テスト）だけでは、複雑に絡み合うコントラクトの状態遷移のすべてを網羅することは不可能です。泥棒は、私たちが思いもしない「斜め上の侵入経路」を探してきます。

そこで今回は、スマートコントラクトのセキュリティをガッチリ固めるための最先端アプローチ、「Echidna（エキドナ）」を用いたプロパティベーステストについて、身近な防犯のたとえを交えながら、一歩ずつ優しく紐解いていきましょう！

—

1. 家の鍵と泥棒に例える「不変条件（Invariant）」の考え方

セキュリティの世界でよく耳にする「不変条件（Invariant）」って、なんだか難しそうな言葉ですよね。でも、安心してくだい。考え方はとってもシンプルです。

例えば、あなたの家を想像してみてください。
泥棒対策として、どんな状況であっても「守られなければならない絶対的なルール（不変条件）」って何でしょうか？

  • 「玄関の鍵が閉まっている時は、窓の鍵も必ず閉まっていること」
  • 「金庫の中身は、どんなにお金を出し入れしても、常にマイナス（借金状態）になっていないこと」

スマートコントラクトの世界でも同じです。例えば、銀行のような預金コントラクトを作ったとします。ここで絶対に破られてはならないルール（不変条件）は、「コントラクトが持つ実際のETH残高（Weiの総額）は、ユーザー全員の預金残高の合計値以上でなければならない」ということですよね。

もし、このルールが破られるような状態（＝バグや脆弱性）が存在するなら、それは泥棒が侵入できる「勝手に開く裏口」があるのと同じです。

—

2. Echidna（エキドナ）とは？ 自動で家の弱点を探す「優秀な警備ロボット」

人間が手作業で「この関数を呼び出したあとに、あっちの関数を呼んで……」とテストケースを考えるのは限界があります。そこで登場するのが、スマートコントラクト専用のファザー（自動テストツール）である Echidna です。

Echidnaは、いわば「あなたの書いたコントラクトのあらゆる隙を突こうとする、超優秀かつ執念深い警備ロボット」です。
ランダムにあらゆる関数の組み合わせや数値をぶつけまくり、「おいおい、この手順を踏んだら金庫のルールが破綻してマイナスになったぞ！」という穴（脆弱性）を全自動で見つけ出してくれます。

—

3. 実践！Echidnaで不変条件をテストしてみよう

それでは、実際にEchidnaを使って、コントラクトの不変条件をテストするコードを見ていきましょう！
今回は、簡単な「お小遣い預金コントラクト」を用意しました。ここに隠された「絶対に破られてはならないルール」をEchidnaに監視させます。

脆弱性を含んだサンプルコントラクト

以下のコードを見てください。一見すると普通の預金コントラクトですが、実は大きな落とし穴が隠されています。

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract SimpleVault {
    // ユーザーごとの預金残高を管理するマッピング
    mapping(address => uint256) public balances;
    
    // コントラクト全体の総預金額
    uint256 public totalDeposits;

    // 預金関数
    function deposit() public payable {
        require(msg.value > 0, "0以上の金額を送金してください");
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }

    // 引き出し関数（ここにバグが潜んでいます！）
    function withdraw(uint256 _amount) public {
        require(balances[msg.sender] >= _amount, "残高が足りません");
        
        // ざんねん！送金処理の前に状態を更新し忘れている（Reentrancyや計算ミスにつながる典型例）
        (bool success, ) = msg.sender.call{value: _amount}("");
        require(success, "送金に失敗しました");

        balances[msg.sender] -= _amount;
        // totalDeposits の減算を書き忘れてしまいました！
    }
}

お気づきでしょうか？ withdraw 関数の中で、ユーザーの残高 (balances[msg.sender]) は減らしているものの、全体管理用の totalDeposits を減らし忘れています。これにより、実際のコントラクト残高と、記録上の totalDeposits が乖離してしまう致命的なバグ（不変条件の崩壊）が発生します。

Echidna用のテストコントラクトを書こう

このバグをEchidnaに発見させるために、テスト用のコントラクトを同じファイル、または別ファイルとして作成します。Echidnaは、関数名が echidna_ で始まるブール値（true / false）を返す関数を自動的に探してチェックします。

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import "./SimpleVault.sol";

contract EchidnaVaultTest is SimpleVault {
    
    // Echidnaが常に「true」であることを検証する不変条件（Invariant）
    // ルール：「コントラクトが持つ実際のETH残高は、記録上の totalDeposits 以上であるべき」
    function echidna_test_solidity_balance() public view returns (bool) {
        // address(this).balance はこのコントラクトが実際に持っているETHの量
        // これが totalDeposits を下回ったら、どこかで計算がおかしくなっている証拠
        return address(this).balance >= totalDeposits;
    }
}

Echidnaを実行してみよう！

ターミナルを開き、Echidnaのコマンドを実行します。

# Echidnaを使ってテストコントラクトを実行するコマンド
echidna-test EchidnaVaultTest.sol

しばらくすると、Echidnaが猛烈なスピードでランダムなトランザクションを生成し、次のようなエラー結果を吐き出します。

Failing assertion:
  echidna_test_solidity_balance() returned false
Call sequence:
  deposit(100 wei)
  withdraw(50 wei)

「おめでとうございます！（と言っていいのか分かりませんが）」、Echidnaは一瞬でバグを見つけ出しました。
deposit で 100 wei 預け、withdraw で 50 wei 引き出した結果、totalDeposits の辻褄が合わなくなり、私たちが設定した不変条件（echidna_test_solidity_balance）が false になったことを教えてくれています。

—

4. 現場で役立つ！Echidnaの運用とパラメーター設定のコツ

実務の現場でEchidnaを導入する際は、デフォルトのままだとテストが途中で終わってしまったり、効率が悪かったりします。プロジェクトの規模や目的に合わせて、設定ファイル（echidna.yaml）を調整するのがプロの技です。

以下に、現場でよく使われる実用的な設定ファイルのサンプルをご紹介します。

# echidna.yaml の設定サンプル
testMode: "assertion"       # テストモード（assertion または property）
corpusDir: "corpus"         # 成功したトランザクションの順序を保存するディレクトリ
maxGas: 10000000            # 1回のトランザクションで使用する最大ガスリミット
seqLen: 100                 # 1つのテストシナリオで実行するトランザクションの最大数（長いほど複雑なバグを見つけやすい）
testLimit: 50000            # ファジングを試行する回数（多いほど網羅性が上がります）
initialBalance: 1000000000000000000 # テストコントラクトに最初から持たせるETH残高（1 ETH）

この設定ファイルをプロジェクトのルートディレクトリに置いておけば、コマンド一発で最適化されたファジングテストを実行できるようになります。

—

まとめ：セキュリティは「疑うこと」から始まる

今回は、Echidnaを使ったプロパティベーステストの基本と、不変条件の重要性について解説しました。

  • 不変条件（Invariant）とは、システム全体で「絶対に破られてはならないルール」のこと。
  • Echidnaは、そのルールが破られるような複雑な操作手順を全自動で見つけ出してくれる優秀な相棒。
  • テストコードは echidna_ で始まる関数名で定義し、常に true になるべき条件を記述する。

「自分のコードは大丈夫」という思い込みを捨て、優秀な警備ロボットであるEchidnaにガンガン攻撃を試してもらう。このアプローチを取り入れるだけで、スマートコントラクトの安全性は劇的に跳ね上がります。

一歩ずつ、確実にセキュアなコードを書けるエンジニアになっていきましょう！次回の解説もお楽しみに！

スポンサーリンク

コメント

タイトルとURLをコピーしました