新シールドプール「Ironwood」で再発防止へ
プライバシーコイン「ジーキャッシュ（Zcash）」の研究プロジェクト「タキオン（Tachyon）」が進める形式検証が最終段階に入り、最新のシールドプールに「検出不能な偽造バグ」が存在しないことを示す数学的証明の完成が近づいているようだ。これを受けてかZECは7月7日、24時間で12%超上昇し、6月上旬以来となる500ドル台に一時回復した。なおシールドプールとは、Zcashで送金額や送受信者を秘匿したままZECを管理・移転するための領域を指す。暗号技術のゼロ知識証明（ZKP）が活用されている。
6月4日、Zcashの現行シールドプール「オーチャード（Orchard）」の偽造バグが公表された。これは攻撃者が検出されないままZECを偽造できる可能性がある脆弱性で、開発チームは公表前の6月1日に緊急修正を導入し、6月2日までに対応を完了していた。
開発側は、この脆弱性が実際に悪用された可能性は低いとの見方を示している。一方で、Zcashは取引額を秘匿する設計であるため、過去に悪用がなかったことを暗号学的に完全に証明することはできないという構造的な課題も明らかになった。
この脆弱性の公表を受け、ZECは2日間で40%超下落する場面もあった。
これを受け、Zcashコミュニティは、オーチャードをベースに脆弱性を修正した新たなシールドプール「アイアンウッド（Ironwood）」の導入を進めている。
アイアンウッドでは「ターンスタイル（Turnstile）」機構を活用し、旧オーチャードから資金が移動する際の入出金をオンチェーンで照合することで、オーチャード内で検出不能な偽造が発生していなかったことを間接的に確認できる設計となる。また、同アップグレードの有効化後は、旧オーチャードに新たな出力を作成する取引を無効化し、旧オーチャード内の資金はターンスタイルを通じてのみ移動できるようにすることで、流通するZECの上限を明確にする狙いもある。
タキオンが公開した技術ブログでは、今回の脆弱性を修正するだけでは十分ではないと説明。アイアンウッドについては大規模な監査やAIツールを用いた分析に加え、形式手法による検証を通じて、暗号学的前提が成り立つ範囲で「検出不能な偽造バグ」そのものを排除することを目指しているという。
また、Zcash創設者のズーコ・ウィルコックス（Zooko Wilcox）氏は7月8日のXで、「タキオンの形式検証プロジェクトは、最新のZcashシールドプールに検出不能な偽造バグが存在しないことを示す数学的証明の完成間近にある」と投稿した。さらに、この成果によって「マネーサプライの検証可能性とプライバシーという長年の二律背反が終わりを迎える」との見方を示したほか、暗号学的証明と形式検証を組み合わせることで、今後数年のうちにさまざまな計算の正しさを数学的に検証できるようになる可能性があるとの展望も語っている。
タキオンによると、こうした形式検証が現実的になった背景には、AIを活用した証明生成技術の進歩があるという。従来は数年かかることもあった作業が、人間の監督の下で大規模言語モデル（LLM）を活用することで、数週間程度まで短縮できるようになったとしている。
実務にはタキオンのタル・デレイ（Tal Derei）氏、セキュリティ企業zkSecurityのグレゴール・ミチャ＝バウデ（Gregor Mitscha-Baude）氏、Zcash Open Development Labのダイラ＝エマ・ホップウッド（Daira-Emma Hopwood）氏らが参加している。
同ブログでは、偽造バグを「仕様（プロトコルの数学的記述）の誤り」「実装（ソフトウェア）の誤り」「暗号学的前提の破綻」の3種類に分類している。
このうち実装上の不具合はブロックチェーン上に痕跡が残るため事後に検出可能だが、仕様レベルの誤りは検出不能な偽造を引き起こす可能性があるという。
実際、2016年に発見されたゼロキャッシュ（Zerocash）初期設計の欠陥や、2018年に公表された旧Sproutプロトコルのゼロ知識証明システムの健全性に関する欠陥はいずれも仕様レベルの問題だった。また今回のオーチャードの脆弱性についても、zk-SNARK（ZKP技術の一種）回路の健全性に関する不具合で、回路コードの記述漏れに起因する仕様上の誤りに近いものだったと説明している。
元NEAR Protocolコントリビューターのヴァディム・ザコディル（Vadim Zacodil）氏は、今回の問題を2010年に発生したビットコインのインフレバグ（約1840億BTCが不正生成された事案）になぞらえている。
ただし、ビットコインは取引金額が公開されているため、不正発行はすぐに検出され修正された。一方、Zcashのシールドプールは取引額を秘匿するゼロ知識証明に依存しているため、証明システムに欠陥があれば偽造コインが表面化しないまま生成される可能性がある点が大きく異なる。
タキオンは、アイアンウッドの仕様を形式検証によって証明できれば、残るリスクは実装上の不具合（発生すれば検出可能なもの）と暗号学的前提の破綻に限定できるとしている。なお、証明全体の構成や、検証対象となるモデルと実際に稼働するソフトウェアとの対応関係については、続編の記事で詳しく説明するとしている。
Tachyon’s Formal Verification project is on the verge of producing a mathematical proof that there are no undetectable counterfeiting bugs in the latest Zcash shielded pools. https://t.co/hFkULWYL9J
— zooko🛡🦓🦓🦓 ⓩ (@zooko) July 7, 2026
参考：Tachyon発表
画像：PIXTA