パスワードや銀行の残高といった秘密そのものを決して明かすことなく、自分がその秘密を知っていることを証明できる世界を想像してみてください。これは**ゼロ知識証明（ZKP）**の魔法です。それは、魔法使いがコインをウサギに変える手品を見せるようなものです。あなたは、どのようにしてその手品を行ったのか、あるいは変身前のウサギがどのような姿だったのかを、決して見ることはありません。これらの証明は、数十億ドルのデジタル通貨を保護し、私たちの最も敏感な個人データを守る、インターネットの未来のバックボーンになりつつあります。しかし、ここには落とし穴があります。これらの「デジタルの手品」を構築するのは、信じられないほど困難なのです。もし魔法使いが呪文の本（スペルブック）でほんの少しでもミスをすれば、手品全体が失敗し、詐欺師が証明を偽造して、お金を盗んだり身分を偽ったりすることを許してしまうかもしれません。リスクが非常に高いため、研究者たちは、公開前にこれらのスペルブックのエラーをスキャンするために設計されたソフトウェアプログラムである、一連の「セキュリティ・ガード（警備員）」のツールボックスを構築してきました。

しかし、果たしてこれらのセキュリティ・ガードは本当に役に立っているのでしょうか？ これが、この論文が投げかける大きな問いです。著者であるトップ機関の研究チームは、これらのツールをテストすることにしました。彼らは単にツールのマーケティング資料を見るだけでなく、実際のプロジェクトで見つかった70個の現実世界のバグを大量に集め、それらのツールがどれだけ多くのバグを検知できるかを検証しました。また、これらのシステムを構築・監査している48人の専門家にインタビューを行い、彼らが実際にどう考えているかを探りました。彼らが語る物語は、希望と厳しい現実認識が入り混じったものです。ツールは有用ではあるものの、決して完璧ではなく、業界はいまだに重労働を人間の脳に大きく依存しているという現実です。

景観：ハンマーが詰まったツールボックス

研究者たちはまず、現在の「セキュリティ・ランドスケープ（景観）」を調査しました。全員が特定の種類の鍵を直そうとしているワークショップを想像してみてください。彼らは、ほとんどすべてのセキュリティツールが、「Circom」と呼ばれる一種の鍵の言語に対してのみ機能するように設計されていることを見出しました。それは、世界中でネジやボルト、接着剤が使われ始めているのに、ワークショップにはハンマーしか揃っていないような状態です。Circomは普及していますが、より新しい言語やシステム（zkVMsと呼ばれます）へのサポートはほとんどありません。

これらのツールの多くは、「アンダーコンストレインド（制約不足）」と呼ばれる特定のエラーを探しています。例え話を使うなら、あなたが橋を建設していると想像してください。アンダーコンストレンドな橋とは、設計図に「この橋は車を支えなければならない」とは書いてあるものの、「この橋は車だけを支えなければならない」という指示を忘れているようなものです。賢い泥棒がタンクを走らせても、橋は依然として「はい、これは有効な車です！」と答えてしまうでしょう。ツールはこうした「足りないルール」を見つけることには長けていますが、より複雑なロジックエラーや、橋が道路の他の部分とどのように接続されるかといった間違いについては苦戦します。

テストドライブ：本当の性能は？

次に、チームはこれら6つのツールを厳格なテストドライブにかけました。彼らは、実際に発見された70個の現実世界のバグをツールに読み込ませました。結果は、まるでジェットコースターのようでした。

ツールがバグを単独で見たとき（例えば、機械から一つの壊れた歯車を取り出して、それ単体でテストする場合）、彼らは問題の約**45.7%を検知しました。これは有望に聞こえます！ しかし、研究者がツールをフルセットの、混沌とした現実世界のコードベース（機械全体）に対してテストしたところ、その有効性はわずか19.6%**へと急落しました。

なぜ低下したのでしょうか？ 論文は、現実世界のコードは乱雑であることを示唆しています。ツールは複雑な依存関係によって混乱したり、計算が速すぎて解けないためにクラッシュしたり、タイムアウトしたりすることがよくあります。それは、一文であれば素晴らしい校正を行うが、小説を丸ごと貼り付けるとフリーズしてしまうスペルチェッカーのようなものです。著者らは、ツールは進化しているものの、人間の助けなしに大規模なプロジェクトを自動的に保護できるような「ボタン一つで解決できる」ソリューションにはまだなっていないと指摘しています。

魔法の鏡：形式検証

論文はさらに、**形式検証（Formal Verification）**と呼ばれる、より高度な手法についても考察しています。もしセキュリティツールがスペルチェッカーだとすれば、形式検証は、どんなことがあってもその呪文が失敗しないことを数学的に証明しようとする試みです。これは安全性のゴールドスタンダード（最高基準）です。

研究者たちは、進展は見られるものの、それは主に孤立した領域で行われていることを発見しました。専門家たちは、システムの特定のパーツ（「制約」、つまり橋のルール）が健全であることを証明することには成功しています。しかし、システム全体はどうでしょうか？ そうではありません。「ウィットネス・ジェネレーター」（実際に証明を構築する部分）や「プルーフ・システム」（秘密を隠す魔法の部分）は、依然として未検証のままであることが多いのです。それは、橋が強いことは証明したが、土台がしっかりしているか、あるいは建設作業員が計画に従ったかどうかを確認し忘れているようなものです。論文は、これらの証明がしばしば「信頼された仮定」に依存していること、つまり、証明を書くために使用されたツールがミスをしていないことを信じるしかない、という点に触れています。

人間の要素：専門家の声

最後に、チームは実際にこれらのシステムを構築・監査している48人の実務家に対して調査を行いました。結果は非常に興味深いものでした。AIや大規模言語モデル（LLM）の台頭にもかかわらず、その作業は依然として人間主導です。開発者の約85%、監査人の約**83%**がLLMを補助として利用していますが、彼らはそれらを代替品としてではなく、アシスタントとして使用しています。

専門家たちは研究者に対し、最大の問題は単にバグを見つけることではなく、ツールが使いにくいことであると語りました。ツールは手動でのセットアップを多く必要とし、新しい言語に対応しておらず、報告書の内容も分かりにくいことが多いのです。実務家たちは、より簡単に統合でき、異なる言語間で動作し、明確で信頼できる答えを出してくれるツールを求めています。彼らは特に「セマンティック・エラー（意味論的エラー）」、つまり、コードがプログラマーの指示通りに正確に動作しているものの、プログラマーが意図した通りには動いていないというミスを非常に懸念しています。現在のツールは、こうしたエラーを見つけるのが極めて苦手です。

結論

この論文は明確な絵を描き出しています。ゼロ知識証明は強力ですが、それを保護することは依然として進行中の課題です。現在ある自動化ツールは、特定の言語における単純なミスを捉えるには役立ちますが、現実世界のプロジェクトの複雑さに直面すると力不足となります。業界は現在、自動スキャニングと重厚な人間によるレビューが混在しており、AIをヒーローとしてではなく、ヘルパーとして活用する傾向が強まっています。

著者らは、断片的なパーツだけでなく、システム全体を扱えるより優れたツールが必要であると結論付けています。私たちは、コードの構文（シンタックス）だけでなく、その「意味（セマンティクス）」を理解するツールを必要としており、形式検証を日常の開発においてより使いやすくする必要があります。それまでは、私たちのデジタルな秘密の安全性は、いくつかの便利なロボットが明らかなタイポ（打ち間違い）を捕まえる傍らで、人間の魔法使いのチームが呪文をダブルチェックすることに依存しているのです。