【入門編】スマートコントラクトの形式検証(Formal Verification)の導入 – IoT・OT（制御システム） & ブロックチェーンセキュリティ防御ガイド

こんにちは！スマートコントラクトの開発現場やセキュリティの最前線に飛び込んだばかりの頃は、見慣れない専門用語の壁にぶつかって圧倒されてしまいますよね。「本当に自分の書いたコード、ハッキングされないだろうか…」と夜も眠れなくなる気持ち、痛いほどよく分かります。

今回は、Web3の世界における最強の盾の一つである「スマートコントラクトの形式検証（Formal Verification）」について、一歩ずつ優しく紐解いていきましょう！

—

1. 身近な防犯で例える「形式検証」ってなに？

いきなり「形式検証」や「数学的証明」なんて言われると、大学の数学の授業を思い出して逃げ出したくなりますよね。でも、安心してください。身近な「家の鍵」に例えてみると、とってもシンプルに理解できます。

テスト（従来のやり方）と形式検証の違い

通常のテスト（ユニットテスト）：

「家族全員の鍵で開くか？」「泥棒が適当な針金で開けようとした時に開かないか？」を何パターンも試してみるテストです。これはこれで大事ですが、「100万通りある鍵穴の組み合わせのうち、運良く（あるいは悪く）開いてしまう1通り」を見落とすリスクが残ります。

形式検証（今回の主役）：

鍵そのものを物理的なものではなく、「完全に解読不可能な数式」としてコンピュータに証明させるアプローチです。「この家には、地球上のいかなる鍵やピッキングを使っても、絶対に窓やドアを突破することはできない」ということを、数学の論理でパズルのように完璧に証明しちゃうイメージですね。

つまり、テストが「いくつかの意地悪を試すチェック」なのだとしたら、形式検証は「あらゆる可能性（無限のパターン）を数式でねじ伏せる完全無欠の証明」なのです。

—

2. なぜ形式検証が必要なの？ブロックチェーンの怖さ

スマートコントラクトが一度ブロックチェーン上にデプロイ（公開）されてしまうと、後から「あ、バグがあった！」と言って修正パッチを当てるのは、原則として不可能（あるいは非常に困難）です。銀行の金庫が、通りすがりの誰でも触れる野外にむき出しで置かれているようなものだと思ってください。

実務の現場では、CertoraやK-Frameworkといったツールを使って、この数学的証明を行います。「もしこの関数が実行されたら、絶対に預金残高がマイナスになってはいけない」というルール（これをプロパティ、あるいは不変条件と呼びます）をコードとして定義し、ツールに全パターンを網羅的に検証してもらうのです。

—

3. 実践！Certora風のプロパティ記述を書いてみよう

百聞は一見に如かず。実際に、簡単なスマートコントラクトに対して「どんなルール（証明すべき性質）を書くのか」を見てみましょう。

ここでは、誰もがお世話になるシンプルな「お財布（Vault）コントラクト」を例にします。

サンプルコード：お財布コントラクト（Solidity）

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

contract SimpleVault {
    // ユーザーごとの預金残高を管理するマッピング
    mapping(address => uint256) public balances;

    // 預金機能：ETHを受け取って残高を増やす
    function deposit() external payable {
        require(msg.value > 0, "0以上の金額を送金してください");
        balances[msg.sender] += msg.value;
    }

    // 引き出し機能：自分の残高分だけ引き出せる
    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount, "残高が足りません");
        balances[msg.sender] -= amount;
        
        // 実際の送金処理（簡略化のためLow-level callを使用）
        (bool success, ) = msg.sender.call{value: amount}("");
        require(success, "送金に失敗しました");
    }
}

このコントラクトに対して、「いかなる操作を行っても、コントラクト全体が持つETHの総額は、全ユーザーの残高の合計と常に一致しなければならない」という絶対的なルール（不変条件）を、形式検証用言語（Certoraなら CVL など）で定義します。

形式検証ルールのイメージ（CVLの例）

// Vault.spec ファイルのイメージ
methods {
    function balances(address) external returns (uint256) envfree;
    function deposit() external payable;
    function withdraw(uint256) external;
}

// 常に満たされるべきルール：コントラクトの残高 >= 全ユーザーの残高の総和
rule invariant_solvency() {
    // コントラクトが持つ実際のETH残高
    mathint totalEthInContract = currentContract.balance;
    
    // 数学的にバグがないか、あらゆるトランザクションの組み合わせを探索して証明する
    assert totalEthInContract >= 0, "破綻エラー：ETHの残高がマイナスになりました！";
}

このように、開発者は「こういう状態になってはいけない」「このルールは絶対に破られてはならない」という条件をコード（ルール）として書き起こし、検証ツールに読み込ませます。

—

4. 形式検証の限界と「盲点」

「なんだ、じゃあ形式検証ツールを導入すれば、もうハッキングされる心配はゼロだね！」と安心したくなるかもしれませんが、ここにサイバー攻撃者が狙う最大の盲点があります。

それは、「人間が書いたルール（仕様）自体にバグや抜け穴があったら、ツールはそれを検知できない」という点です。

よくある現場の失敗：

「すべてのユーザーの残高がマイナスにならないこと」というルールを完璧に証明できたとします。しかし、開発者が「そもそも管理者が勝手に全額を引き出せるバックドアの存在」をルール書きに含め忘れていた場合、ツールは「このルール内においては完璧です」とお墨付きを与えてしまいます。

例えるなら：

「正面玄関の鍵は100%ピッキング不可能です」と数学的に証明された金庫であっても、設計図の段階で「裏口の窓に鍵がついていない」という仕様の抜け穴があれば、泥棒は裏口からスルスルと侵入してしまいますよね。

形式検証は「コードが意図したルール通りに動いているか」を証明する最強の矛ですが、「その意図（ルール）自体が正しかったのか」を判断するのは、依然として人間の仕事なのです。

—

まとめ：一歩ずつ、確実に安全なコードへ

今回はスマートコントラクトの形式検証について、身近な防犯に例えながら解説しました。

1. 形式検証とは、従来の「いくつかのテストを試す」やり方を超え、数式と論理であらゆるパターンを網羅的に証明する強力なアプローチである。
2. Certoraなどのツールを使い、破られてはならない不変条件をルールとして定義する。
3. ただし、「ルール（仕様）自体の書き忘れや抜け穴」を見つけることはできないため、人間による設計レビューや従来のテストと組み合わせて使うことが極めて重要である。

セキュリティの世界は広大で、最初は圧倒されることばかりだと思います。でも、こうした強力なツールと正しいアプローチを一つずつ知っていけば、確実にスマートコントラクトの安全性は高まります。

焦らず、一歩ずつ、一緒にセキュリティの階段を登っていきましょう！