Loading...
シリーズ： 形式検証シリーズ · 全3回中の第2回 対象読者： 初心者。第1回では形式検証を紹介しました。今回は、それがなぜ急務になったのかを示す実際のバグを取り上げます。必要なことはすべて基礎から説明します。 この記事で得られること： 暗号学的証明システムに健全性の穴が生じる仕組み、2026年のZcash「Orchard」バグの正体、この種のバグが何年も隠れ得る理由、そして過去にも起きた理由について、直感的かつ正確に理解できます。
第1回では、テストはバグの存在を示せても不在を証明することはできず、最も危険なバグはシステムの仕様、すなわちその基礎となる数学に潜むと述べました。この記事はその事例研究です。2026年、ZcashのOrchardシールドプールに、攻撃者が無制限の偽造資金を人知れず作り出せてしまう可能性がある欠陥が見つかりました。それは4年間にわたり、繰り返し行われた監査もすり抜けていました。この事例とその前例を理解することは、システムの正しさを証明する必要性をこれ以上なく明確に示します。
Zcashは、プライベートモードを備えた暗号資産です。そのシールドプールでは、トランザクションの金額、送信者、受信者が隠されます。このプライバシーは、ゼロ知識証明、つまりトランザクションの内容を明かさずに、すべてのルールに従っていることを証明する暗号学的証明によって実現されています。
この設計には両面があります。Bitcoinのような透明な台帳では、誰かが無からコインを生み出せば、水増しされた数値は誰にでも見え、ネットワークはそれを検知して巻き戻せます。シールドプールでは、数値は設計上隠されています。したがって、証明システム自体に無効なトランザクションを有効に見せかける欠陥があった場合、その偽造は検知不能になります。台帳は意図的に不透明であるため、台帳を調べても見つけられません。
それがまさにOrchardで現実化したリスクです。それを理解するには、ゼロ知識証明が実際に何を確認しているのかを見ていく必要があります。
書類を直接見ずに旅行者を承認しなければならない国境審査官を想像してください。旅行者はそれぞれチェックリストに記入し、審査官はすべての項目にチェックが入っている人を承認します。このチェックリストは、正当な旅行者だけがすべての項目にチェックを入れられるように設計されています。
では、そのチェックリストに「パスポートの有効期限が切れていない」という重要な項目が1つ欠けているとします。ほとんどの人は依然として正直に記入するため、何も問題がないように見えます。しかし、有効期限切れのパスポートを持つ人も、残りの項目すべてにチェックを入れて通過できます。日常的な利用ではシステムは正常に見えます。この穴が意味を持つのは、それを探そうとする人に対してだけです。
ゼロ知識証明は、そのチェックリストのように機能します。プライベートな詳細を明かすのではなく、それらが固定された一連の条件を満たすことを確認します。そして、必要な条件が1つでも誤って抜け落ちれば、無効な入力であっても通過できる一方で、他のすべては正常に見え続けます。
「条件のチェックリスト」を正確に説明しましょう。まさにそこにバグがありました。
内部では、「このトランザクションは有効である」という主張は回路として符号化されます。これは、数値に対する方程式として書かれた、制約と呼ばれる固定された算術条件の集まりです。有効な証明を作るには、証明者はすべての制約を満たす秘密の値、すなわち証人を提供しなければなりません。証明は、そのような証人が存在することを検証者に納得させますが、証人自体は明かしません。
このシステムに必要な性質には名前があります。
健全性： 偽の主張に対して有効な証明を作ることは不可能でなければなりません。すべての制約を満たす証人を持てるのは、真の主張だけであるべきです。
健全性は偽造防止の保証です。健全性が保たれていれば、有効な証明は本当に「実在し、ルールに従ったトランザクションが行われた」ことを意味します。健全性に穴があれば、有効な証明は何も意味しないかもしれません。
制約ではしばしば、値が単純なものであることを強制する必要があります。よくある例は、値bを0または1のどちらか一方である単一のビットに制限することです。これを行う標準的な方法は、次の1つの制約です。
b × (b − 1) = 0
なぜ機能するのでしょうか？積がゼロになるのは、その因子の一方がゼロである場合だけです。したがって、b × (b − 1) = 0はb = 0またはb = 1を強制し、それ以外を許しません。17で折り返す算術において0から16までのすべての値を確認すると、これを満たすのは0と1だけです。✓
ここで、その行が回路から誤って抜け落ちたと想像してください。するとbは制約を受けなくなります。不正な証明者はbを5や9、あるいは任意の値に設定しても、残りの制約を満たせます。この1行の欠落が健全性の穴です。偽の主張にも、制約を満たす証人が存在するようになります。
これは仮定の話ではありません。まさにこの種のboolean制約の欠落が、開発中にZcashの最初のシールド設計であるSproutに見つかり、リリース前に修正されました。制約不足は、これらの回路を構築する際に生じる最も一般的で危険な誤りの一つです。
これが小さな規模で見たOrchardバグの全体像です。では本題に進みましょう。
Zcashのシールド証明は、楕円曲線に基づいています。楕円曲線は、その上の点を組み合わせたり、数値で「乗算」したりできる数学的対象であり、回路はこれらの演算を制約によって強制しなければなりません。回路には、楕円曲線乗算を実行し、それが正しく行われたことを確認するガジェットが含まれます。
Shielded Labsと研究者Taylor Hornbyによる開示によれば、Orchardの欠陥はまさに次のものでした。
Orchard回路の制約不足要素により、楕円曲線乗算に任意の偽の入力を与えても、乗算チェックを通過できることが可能になっていました。
平たく言えば、回路のチェックリストには、その乗算を確定させるべき項目が欠けていました。この穴により、十分に専門性の高い攻撃者は、トランザクションが無から価値を生み出しているにもかかわらず、システムが受け入れるトランザクション証明を構築できました。これは偽造であり、シールドプール内の金額は隠されているため、台帳からは検知不能でした。Tachyonチームは後に、同じ欠陥をコードレベルで、基礎となる方程式を密かに崩す回路内の欠落行として説明しました。
チェックリストの話との類似は完全に一致します。
| チェックリストの話 | Orchardバグ |
|---|---|
| 「パスポートの有効期限が切れていない」という項目の欠落 | 楕円曲線乗算に関する制約の欠落 |
| 有効期限切れのパスポートを持つ旅行者が通過する | 任意の偽の入力が乗算チェックを通過する |
| 他の全員は影響を受けないため、異常に見えない | 通常のトランザクションは完全に機能し、欠陥を隠していた |
| 穴を探している人だけが見つける | 回路の数学を意図的に調査した専門家が発見するまでかかった |
この問題がどれほど深刻だったかを明確にすると、研究者はAIの支援を受けて完全に動作するエクスプロイトを書き、ローカルのテストネットワークで、無制限かつ検知不能な偽造コインを生成できることを確認しました。これは理論的な懸念ではなく、実際に悪用可能な欠陥でした。
このバグは、2022年5月の有効化から2026年6月の緊急修正まで、Orchardに存在していました。その間、世界最高峰の暗号学者たちによる専門的な監査が繰り返し行われました。なぜでしょうか？
第1回で警告した通り、テストは事例を抽出するにすぎず、この欠陥は誰も抽出しなかった事例に存在していたからです。通常のトランザクションでは欠けていた制約が使われなかったため、すべてのテストは通り、日々の通常運用も完璧に見えました。この欠陥に到達するには、穴を正確に狙った特殊な証人を意図的に構築する必要がありました。最終的にこれはテストの実行ではなく、回路の数学についての推論によって発見されました。
発見そのものが、セキュリティが向かう先を示しています。2026年4月、Shielded Labsは、まさにこの種の欠陥を探すためにセキュリティ研究者Taylor Hornbyを起用しました。2026年5月下旬に新しい最先端AIモデル（AnthropicのClaude Opus 4.8）がリリースされた直後、Hornbyはカスタム分析ハーネスと従来の手法を組み合わせ、Orchard回路を対象に絞ったレビューにこのモデルを使いました。2026年5月29日、このレビューで脆弱性が見つかりました。
開示には、冷静に明示すべき2つの事実があります。
Orchardバグは繰り返し発生する系統に属しており、その系統を見ることで、形式検証は任意の選択肢ではなく必然であると感じられます。偽造につながる欠陥は、常に3つの原因のいずれかにさかのぼります（第1回で示した分類法です）。すなわち、仕様（数学そのもの）、実装（正しい数学にコードが従わないこと）、または破られた前提です。そして重要なのは、偽造バグが検知不能になるのは、それが仕様に存在する場合だけだということです。実装バグは永続的な公開証拠を残します。すべてのブロックには各トランザクションの完全な内容が記録されているため、修正済みソフトウェアで履歴を再実行すれば、バグのあるコードが誤って受け入れたトランザクションが明らかになるからです。
Zcash自身の歴史は、このパターンを示しています。
| バグ（年） | 原因 | 検知可能？ |
|---|---|---|
| Zerocashのコミットメント欠陥（2016年、リリース前） | 仕様（切り詰められたハッシュがバインディング性を損なった） | 検知不能 |
| 信頼できるセットアップの健全性欠陥（2018年） | 仕様（基礎となるzk-SNARK論文の誤り） | 検知不能 |
| 証明システムのクエリ衝突（2025年） | 仕様（証明システム内のチェックの欠落） | 検知可能 |
| 曲線部分群検証バグ（2016年） | 実装（部分群チェックの欠落） | 検知可能 |
| Orchardの制約不足乗算（2026年） | 仕様（回路） | 検知不能 |
一貫した流れは明白です。永遠に隠れ得る欠陥は、数学にある欠陥です。これは、仕様の機械検証済み証明が一度にすべてのケースを対象として排除できる、まさにその種類です。テストと監査は標本を調べます。数学を証明することだけが、すべての入力をカバーします。
Zcashの開発者は迅速かつ段階的に対応しました。
この第2段階で形式検証が物語に登場します。それは第3回の主題です。チームが実行に移した認識は、このシリーズ全体を結びつけるものなので、あらかじめ紹介する価値があります。
検知不能な偽造の欠陥は、プロトコルの仕様にしか存在し得ません。したがって、仕様が偽造を許さないことを証明できれば、ここで4年間隠れていたバグのクラス全体を排除できます。
これはまさに第1回の第1の柱となる考え方です。仕様を検証すれば、テストでは決して閉じられなかった穴を閉じられます。
意図的に単純化しています。実際の回路には数百の領域と数千の制約があり、実際の欠陥は単一のビットチェックの欠落より技術的に複雑です。ビットチェックを使ったのは、制約不足の回路の形を正確に示せるためであり、またその正確な誤りがZcashの歴史に実在するためです。公式開示にある通り、正確なOrchardの欠陥は制約不足の楕円曲線乗算でした。また、開示と対策の時系列も簡略化しています。権威ある技術的説明については、Shielded Labsの開示およびProject Tachyonの解説を参照してください。
b(b−1)=0はbを0または1に強制しますが、これを外すとbは任意の値にできます。この正確な種類のバグはZcashの歴史に実在します。）| 用語 | 平易な意味 |
|---|---|
| シールドプール | 金額と当事者が隠されるZcashのプライベートモード |
| ゼロ知識証明 | 隠された主張が有効であることを証明し、それ以外は何も明かさない証明 |
| 回路 | 有効なトランザクションが満たさなければならない、固定された算術条件の集合 |
| 制約 | 回路内の1つの条件（方程式） |
| 証人 | 制約を満たす秘密の値 |
| 健全性 | 真の主張だけが有効な証明を生成できるという保証 |
| 健全性の穴 | 偽の主張を通過させる、欠けた制約 |
| 制約不足 | 必要な条件が欠けた回路であり、Orchardバグの根本原因 |
| 検知可能／検知不能 | 悪用が公開台帳に証拠を残すかどうか |
偽造されたZcashは実際に作られたのでしょうか？ 悪用の証拠は見つかっておらず、チームはその可能性を低いと考えています。しかし、この欠陥は台帳から検知不能だったため、台帳だけでは一度も起きなかったことを完全には証明できません。だからこそ、対応は非常に徹底したものとなりました。
金額を隠すことは、なぜバグをより深刻にするのでしょうか？ 透明なチェーンでは、発行されたコインは見えるため、発見して取り消せます。プライバシーのために金額が隠されている場合、偽造バグは目に見える異常を生じさせず、気づかれないまま残り得ます。
なぜ何年もの監査で発見されなかったのでしょうか？ 監査とテストは主に、現実的なケースでの挙動を調べます。この欠陥は、数学的なエッジケースを狙った意図的に細工された特殊な入力でのみ現れ、通常のレビューでは実行されませんでした。テストではなく、回路についての標的を絞った推論によって発見されました。
制約が1つ欠けるだけで本当に十分なのでしょうか？ はい。証明システムの強さは、その完全な制約集合に依存します。必要な条件が1つ抜けるだけで、無効な主張を通過させるには十分です。
AIはどのような役割を果たしたのでしょうか？ 研究者は、カスタムハーネスと従来の手法とともに最先端AIモデルを使い、回路の数学をレビューして欠陥を発見しました。AIはセキュリティの攻防の両側でますます利用されており、それもまた、今やシステムの正しさを証明することが非常に重要である理由の一部です。
シールドトランザクションが「入る資金と出る資金は等しい」ことを証明するはずなのに、回路が1つの出力値を制約するのを忘れたとします。不正な証明者は何ができ、公開台帳はなぜ完全に正常に見えるのでしょうか？ (答えは以下です。)
その出力が制約されていなければ、証明者は実際の入力で許される額より大きく設定し、無から価値、すなわち偽造品を作り出せます。唯一その不均衡を検出できたはずの制約が欠けているため、証明は依然として検証に通ります。そしてシールドプールは金額を隠すため、台帳には「有効なトランザクションが発生した」とだけ表示され、警告を発するような目に見える不均衡はありません。偽造は本物ですが見えません。これこそ回路の健全性が非常に重要であり、テストではなく証明されなければならない理由です。
第3回・Ironwood： 修正は単なるパッチではありませんでした。Zcashのエンジニアは新しいシールドプールを構築し、Lean証明支援系で記述された2,700以上の定理からなる機械検証済み数学的証明を添えました。これにより、定められた前提のもとで偽造資金を作り出せないことが示されています。「残高整合性」と「知識健全性」が何を意味するのか、この証明が正確に何を対象とし何を対象外とするのか、そして旧プールがどのように安全に廃止されたのかを見ていきます。
ZecHubのための Formal Verification シリーズの一部です。