プライバシー特化型仮想通貨ジーキャッシュ（ZEC）の次世代シールドプール「Ironwood」の形式検証が、AI活用により数週間単位で完了目前に迫っている。
プロジェクト・タキオンは7日、Ironwoodの形式検証に関する技術解説を公式ブログで公開。ジーキャッシュ創業者のゾーコ・ウィルコックス氏は「最新のジーキャッシュ・シールドプールに検知不可能な偽造バグが存在しないことを示す数学的証明の完成が間近だ」と述べた。
形式検証で「検知不可能な偽造バグ」を排除
プロジェクト・タキオンによれば、「検知不可能な偽造バグ」は仕様上の誤りのみから生まれるため、仕様を形式検証することで網羅的に排除可能。一方、ソフトウェア実装上の誤りはチェーン履歴に痕跡を残すため、事後検証で必ず検知できるという。
形式検証は、暗号プロトコルの仕様が定めた安全性を数学的に証明する手法で、コードではなく仕様の代数的構造を直接解析する。
6月のOrchard脆弱性が背景に
6月に発覚したOrchardプールの脆弱性は、ゼロ知識証明回路の「健全性バグ」が原因。悪用されれば、Orchardプール内で不正なZECの無制限発行が検知されないまま行われる恐れがあった。開発者らは悪用の証拠はないとしたが、Orchardのプライバシー設計上、偽造が行われなかったことを暗号学的に証明する手段がなかった。
AI活用で証明生成を数週間に短縮
プロジェクト・タキオンは定理証明支援ツール「Lean」を用い、Ironwoodの仕様が「知識健全性」と呼ばれる暗号特性を満たすことを機械的に確認。大規模言語モデル（LLM）を人間が誘導して活用することで、かつて数年を要した証明生成作業を数週間に短縮できるようになった。
作業には、プロジェクト・タキオンのタル・デレイ氏、zkSecurityから契約参加するグレゴル・ミチャ＝バウデ氏、ZODLのダイラ＝エマ・ホップウッド氏が当たっている。
テストネット有効化目前も、スケジュール懸念浮上
Ironwoodのコンセンサスルール変更については、テストネットでの有効化が近日中に行われる見通し。一方、シールデッドラボの事務局長ジェイソン・マクギー氏は3日、IronwoodネットワークアップグレードとZ3スタックへの移行という2つの大規模作業を現行スケジュールで同時完了することへの懸念を示し、以下の3つのリスク低減策をコミュニティに提示した：
・IronwoodとZ3移行の切り離し
・有効化の延期
・独立した第三者によるセキュリティ監査の先行実施
 |  |