概要
- 新しい形のコンピューティング。ゼロ知識証明により、ワークロードを実行し、結果とともに、プログラムが正しく実行されたことを示す短い証明を受け取ることができる。誰でも証明をミリ秒単位で検証でき、プログラムの再実行も、実行者を信頼することも、プログラムが実行されたデータを必要とすることもない。
- 広範な採用の妨げとなってきた3つの大きな課題がある。証明を十分な速さで生成できるようにすること、暗号の専門知識なしに通常のプログラムで証明を利用できるようにすること、そして数十年後にも信頼され続ける暗号の上に証明を築くことである。
- Magnetarは、この3つの課題すべてにおいて大きな進歩を遂げた。 Rust、Go、またはCで書かれたプログラムを証明でき、以前の最速の同等システムと比べて平均で10倍から39倍高速に実行でき、そのセキュリティは標準的なハッシュ関数のみに依存している。これは、ゼロ知識証明を実用的にするためのMicrosoft Researchにおける10年以上の研究による最新の成果である。
新しい形のコンピューティング
コンピューターが生成するすべての結果には、暗黙の問いが伴う。プログラムは主張どおりに実行され、正しい出力を生成したのか?今日、この問いに答えるには、多くの場合、検証とともに一定の信頼が必要となる。私たちは運用者、ベンダー、取引相手、エージェントを信頼し、契約、監査、ログによってその信頼を確立している。
ゼロ知識証明は、信頼を確立するための根本的に異なるアプローチを提供する。プログラムが実行されると、出力とともに短い証明、すなわち「このプログラムが、これらの入力に対して、この出力を生成した」ことを示す暗号学的証明書が生成される。証明は小さく、検証も高速である。受け取った者は、プログラムを再実行することなくミリ秒単位で結果を確認でき、同じ保証を必要とする他の誰にでもその証明を渡すことができる。ゼロ知識性により、証明はプライベートであるべき入力について何も明かさない。
これにより、現実の世界における「正しさ」の意味が変わる。結果は、誰が生成したかによって信頼されるのではなく、それに伴うものによって検証可能になる。誰かの代理として動作するAIエージェントは、各アクションが与えられたポリシーに準拠していたことを示す証明を添付できる。規制対象の金融機関は、取引を公開することなく、取引が正しく処理されたことを証明できる。これらは、証明の生成がプログラムの実行と同じくらい日常的になったときに可能となる。
3つの大きな課題
ゼロ知識証明は1980年代に発明され、プログラムの実行を証明するという考え方はほぼ同じくらい前から存在してきた。これらが一般的なツールにならなかった原因は、同時に解決が困難だった3つの課題である。
効率性。証明の生成には、歴史的に、プログラム自体の実行に比べて数百万倍もの計算量が必要だった。長年の研究によってこのオーバーヘッドは削減されてきたが、最速のシステムは他の面で妥協することによって速度を達成していた。
汎用性とユーザビリティ 多くの証明システムでは、開発者がプログラムを暗号回路(その計算そのものの固定された算術的記述)として手作業で書き直す必要がある。これには数か月を要する。アプリケーションを変更するたびに新しい回路が必要となり、その変換自体がセキュリティバグの頻出原因となっている。汎用的な代替手法は、通常のプロセッサの実行を証明することであり、これによりコンパイルされた任意のプログラムを、書かれたとおりに証明できる。しかしこれまで、その汎用性は速度またはセキュリティにおいて大きな代償を伴っていた。
セキュリティ 証明は、その基盤となる暗号と同じくらいの強度しか持たない。多くの証明システムは楕円曲線に基づいており、これは十分に強力な量子コンピューターによって破られる可能性がある。MicrosoftはQuantum Safe Programでこの問題に取り組んでおり、自社の製品とサービスを耐量子暗号へ移行する予定で、その目標は recently accelerated to 2029。耐量子の証明システムはすでに存在するが、一部は格子問題の仮定に基づいており、大半は証明コストを削減するために新たに考案された暗号関数に基づいている。これらの新しい暗号関数は、今日のインターネットを保護する暗号に与えられてきた数十年に及ぶ精査を経験していないものもあり、証明されていない誤り訂正符号に関する数学的推測に基づくものもある。それらは強い仮定と引き換えに速度を獲得してきた。
PODCAST SERIES
The Shape of Things to Come
MicrosoftのDoug Burgerとゲストが、AIの根本的な真実と、それが未来をどう形づくるかについて掘り下げます。
今すぐ聴く10年以上にわたる研究の成果
10年以上にわたり、Microsoft Researchはゼロ知識証明と検証可能計算を実用的なものにする研究に取り組んできました。初期の研究は2つのアプローチに沿って進められましたが、どちらも小規模なプログラムにしか実用的ではありませんでした。 最初のもの(新しいタブで開く) (新しいタブで開く)は、サムチェックと呼ばれる手法を用いて、証明者との短い対話を通じて検証者が長大な計算をチェックすることを可能にしましたが、 サムチェックプロトコル(新しいタブで開く)これは特定の階層構造を持つ計算にしか適用できませんでした。 2つ目のもの(新しいタブで開く) (新しいタブで開く)は、楕円曲線暗号を用いて、ほぼあらゆる計算に対して非常に小さな証明を作成しました。しかし、これには秘密情報を含む一度限りの信頼されたセットアップ(trusted setup)が必要であり、その秘密情報が漏洩すれば誰もが証明を偽造できてしまいます。このアプローチは量子コンピュータに対しても脆弱です。
2019年、 Spartan と呼ばれる新しいゼロ知識証明システムが、サムチェックのアプローチに立ち返り、信頼されたセットアップなしで汎用プログラムに対応させることに成功しました。Spartanは、異なる暗号学的構成要素でインスタンス化することもできます。この柔軟性こそが、後に証明システムをハッシュ関数のみで構築することを可能にしました。その後、一連の研究成果が残りの部分を埋めていきました:
- Phalanx(新しいタブで開く)は2021年、プロセッサが毎ステップで同じ命令サイクルを実行するといった反復を利用する方法を示し、Spartanより一桁速く計算を証明できるようにしました。Magnetarのプロセッサ記述はこの考えに基づいています。
- Nova(新しいタブで開く), HyperNova(新しいタブで開く), NeutronNova(新しいタブで開く), NeoとSuperNeo(新しいタブで開く) は、Spartanの証明を途中で停止し、部分的な結果を折り畳み(folding)することで、あらゆる規模の計算をはるかに低コストで現実的に証明できることを示しました。
- Brakedown(新しいタブで開く)は2021年、高速なハッシュベースのコミットメント方式を導入し、それをSpartanと組み合わせることで、セキュリティが標準的なハッシュ関数に基づく初めてのSpartan派生系を実現しました。
- Spice(新しいタブで開く), Lasso(新しいタブで開く), Nebula(新しいタブで開く)、そして TwistとShout(新しいタブで開く) は、汎用プロセッサの中核をなすメモリ操作の証明コストを低減し、 Jolt(新しいタブで開く) はこれらをSpartanと組み合わせることで、プロセッサ全体の実行を効率的に証明できることを示しました。
- 今年初めには、 Vega(新しいタブで開く) がこの研究の系譜をデジタルIDに応用し、政府発行のクレデンシャルからの事実を証明しました。 0.1秒未満で.
- より最近では、 BinarySpartan (opens in new tab) が、プロセッサの論理や標準的なハッシュ関数を効率的に表現できる2進体の分野にSpartanをもたらしました。BinarySpartanはまた、 Ligerito (opens in new tab)（証明がはるかに短いBrakedown型のコミットメント方式）と、 ring switching (opens in new tab)（ビットベクトルへのコミットを効率的にする手法）にも依存しています。
これらのそれぞれが問題の一部を解決しました。Magnetarは、その断片が一つにまとまる場所です。
Magnetar
Magnetar はゼロ知識仮想マシン（zkVM）であり、3つの課題すべてに対して同時に大きな進歩をもたらします。
それは汎用です。 Magnetarは、あらゆる主流言語向けの成熟したコンパイラを持つオープンなプロセッサアーキテクチャであるRISC-Vの実行を証明します。開発者はRust、Go、またはCでプログラムを書き、通常どおりコンパイルすれば、Magnetarは書かれたとおりのものを証明します。これが実務で何を意味するか考えてみてください。ビジネスポリシー、データパイプライン、あるいはEthereum Virtual Machine(EVM)のインタープリタは、単なるプログラムにすぎず、すでにそれを保守しているエンジニアが、書かれたとおりの実行をそのまま証明できます。その結果、証明は専門家だけの活動ではなくなるのです。
同じクラスの従来システムよりも高速です。 Magnetarはラップトップ上で毎秒7.2〜8.7百万のプロセッサ命令を証明できることを実証しました。暗号ハッシュから小型のEVMインタプリタ内でのトークン転送に至るまでの15のベンチマークプログラムにおいて、同一マシン上の既存の最速のzkVMと比べて平均10〜39倍高速であり、トークン転送ベンチマークでは他の2つに対して300倍以上高速です。最適化されたMagnetarは毎秒9.5〜12.8百万サイクルを証明でき、これにより本稿で報告する各高速化倍率が約1.3倍に向上します。その証明は約12ミリ秒で検証されます。
そのセキュリティは標準的な暗号技術に依存しています。 Magnetarは、すでにすべての組織のシステムを保護しているSHA-256やSHA-3といった標準的なハッシュ関数に依存しています。楕円曲線も格子も、特殊用途のハッシュ関数も、トラステッドセットアップも、誤り訂正符号に関する未証明の推測も必要としません。ハッシュ関数は暗号ツールキットの中で最も徹底的に研究されたプリミティブであり、NISTが独自の保守的な耐量子オプションとして標準化したステートレスなハッシュベース署名の基盤でもあります。何十年先もなお信頼できなければならないシステムにとって、標準ハッシュ関数のみに依存することは、ロードマップから暗号の移行作業を取り除くことを意味します。
同じ設計上の判断は、2つ目の利益をもたらします。Magnetarの証明の検証は、主に標準的なハッシュ関数と二進体演算の評価で構成されており、これらはまさにMagnetarが効率的に証明できる操作です。したがって、証明の検証はMagnetarにとって通常のワークロードです。これにより、Magnetarは計算を断片に分けて証明し、その断片を結合することで、任意のサイズの計算を証明できるのです。また、これによりMagnetarは台帳やブロックチェーンのような長時間実行されるシステムの証明も可能になります。
その 技術論文 設計全体、安全性の分析、および測定結果を示しています。
今後の展望
Magnetarは、ゼロ知識証明と検証可能計算を、組織がすでに信頼する暗号技術の上に、実用に耐える速度で、エンジニアが通常のコードを書くだけで構築できる段階へと進歩させます。Magnetarは、暗号学的証明が計算の日常的な出力となる未来を可能にします。私たちは、技術リーダーたちがもはや問わなくなるだろうと考えています 実行の証明が実用的かどうか 「その代わりに焦点を当てるのは」 その結果 〜だろう 彼らは鵜呑みにするのではなく、自ら検証することを好む.
ゼロ知識証明があなたのユースケースにどのように役立つかを検討されたい方は、ぜひ ご意見をお聞かせください(新しいタブで開きます).