ジーキャッシュ、『Ironwood』の偽造バグを数学的に排除へ

この記事のポイント

タキオン、Ironwoodの偽造バグを数学的に排除
創業者ウィルコックス氏が証明完成を間近と表明

Ironwoodの形式検証へ

プライバシー特化型仮想通貨ジーキャッシュ（ZEC）のアップグレードを手がけるプロジェクト・タキオンは7日、次世代シールドプール『Ironwood』の形式検証に関する技術解説を公式ブログで公開した。

ジーキャッシュ創業者のゾーコ・ウィルコックス氏は「最新のジーキャッシュ・シールドプールに検知不可能な偽造バグが存在しないことを示す数学的証明の完成が間近だ」と述べた。

同ブログが示した数学的根拠は次のとおりだ。プロジェクト・タキオンによれば、「検知不可能な偽造バグ」は仕様上の誤りからのみ生まれるため、仕様を形式検証することでその種のバグを網羅的に排除できるという。一方、ソフトウェア実装上の誤りはチェーン履歴に痕跡を残すため、事後の検証で必ず検知可能になるとした。形式検証とは、暗号プロトコルの仕様が定めた安全性を数学的に証明する手法で、コードではなく仕様の代数的構造を直接解析する。

6月に発覚したOrchardプールの脆弱性は、ゼロ知識証明回路の「健全性バグ」が原因だった。悪用されれば、Orchardプール内で不正なZECの無制限発行が検知されないまま行われる恐れがあった。

開発者らは悪用の証拠はないとしたが、Orchardのプライバシー設計上、偽造が行われなかったことを暗号学的に証明する手段がなかった。

ジーキャッシュ開発組織シールデッドラボの事務局長が、IronwoodアップグレードとZ3スタック移行の同時完了は困難との見解を示し、延期を含む3つのリスク低減策を検討する価値があると提言。

AI活用で数週間に短縮

プロジェクト・タキオンは定理証明支援ツール「Lean」を用い、Ironwoodの仕様が「知識健全性」と呼ばれる暗号特性を満たすことを機械的に確認する。同ブログは、大規模言語モデル（LLM）を人間が誘導して活用することで、かつて数年を要した証明生成作業を数週間に短縮できるようになったと説明した。

同作業には、プロジェクト・タキオンのタル・デレイ氏、セキュリティ研究機関zkセキュリティ（zkSecurity）から契約参加するグレゴル・ミチャ＝バウデ氏、ジーキャッシュ・オープン・デベロップメント・ラボ（ZODL）のダイラ＝エマ・ホップウッド氏が当たっている。

Ironwoodの開発自体も前進している。ジーキャッシュ財団・プロジェクト・タキオン・バラー・グループ・ZODL・シールデッドラボの各チームが手がけるコンセンサスルール変更については、テストネットでの有効化が近日中に行われる見通しだ。

一方、シールデッドラボの事務局長ジェイソン・マクギー氏は3日、IronwoodネットワークアップグレードとZ3スタックへの移行という2つの大規模作業を現行スケジュールで同時完了することへの懸念をジーキャッシュコミュニティフォーラムで示した。マクギー氏は、有効化の延期・独立した第三者によるセキュリティ監査の先行実施・IronwoodとZ3移行の切り離しという3つのリスク低減策をコミュニティに提示した。

CoinPostの特集記事