Formally Verifying Noir Zero Knowledge Programs with NAVe

技術要約：NAVeによるNoirゼロ知識プログラムの形式検証

問題提起
ゼロ知識（ZK）証明システムは、プライベートな入力 $W$ が関係式 $R(X, W)$ を満たすことを、 $W$ を明かすことなく検証するための算術回路（有限体上の多項式方程式の集合）に依存しています。Noirのような高レベルドメイン固有言語（DSL）は、コードをACIR（Abstract Circuit Intermediate Representation）と呼ばれる中間表現にコンパイルすることで、これらの回路の作成を簡素化します。しかし、この抽象化は微妙な脆弱性を導入します。具体的には、Noirは、プロバー（証明者）への複雑な計算のオフロードを通じて証明の効率を向上させるために設計された「制約なしコード」（unconstrained 関数や unsafe ブロックを介したもの）をサポートしています。開発者が、制約なしコードの結果に対して対応する制約（例：assert 文によるもの）を手動で追加し忘れた場合、生成される算術回路が意図した関係を正確に捉えられない可能性があります。この「制約不足（under-constrained）」のバグは、プロバーが偽のステートメントに対して有効な証明を生成することを許してしまうような、深刻なセキュリティ脆弱性につながる可能性があります。既存の形式検証ツールは、主にCircomのような低レベルの回路DSLを対象としているか、あるいは対話的な定理証明を必要とするため、メモリ操作やブラックボックス関数といった特徴を持つ高レベルなNoirプログラムに対する自動化されたスケーラブルな検証機能が欠けています。

手法
著者らは、高レベルのNoirソースコードではなく、ACIR中間表現上で動作するオープンソースの形式検証フレームワークであるNAVe（Noir Acir Verifier）を提案しています。この選択は、言語の進化に対する安定性を確保し、ACIRをターゲットとする他の言語をツールがサポートできる可能性を高めるためのものです。

1. SMT-LIBによる定式化: NAVeの核となるのは、ACIRのサブセットを充足可能性モジュロ理論（SMT）公式へと定式化することです。著者らは2つの異なるエンコーディングを実装しています。

   • 有限体エンコーディング: cvc5 ソルバーに実装された、非標準的な素数次有限体の理論を利用します。このアプローチでは、フィールド演算を直接モデル化するために、ff.add、ff.mul、ff.bitsum といった特定のオペレータを使用します。
   • 整数演算エンコーディング: SMT-LIBの標準的な整数理論を活用します。これは、素数次有限体 $p$ と整数 $\text{mod } p$ の間の同型性を利用し、フィールド演算をモジュロ整数演算（例：(mod (+ ...) p)）としてエンコードします。

2. オペコードのセマンティクス: 定式化は主要なACIRオペコードをカバーしています。

   • AssertZero: ゼロに等しい多項式方程式の制約としてエンコードされます。
   • BlackBoxFuncCall: 特に Range チェック・オペコードのために定式化されています。有限体エンコーディングでは、これはバイナリ分解（bitsum）を使用してモデル化され、ビットが0または1であることを保証する制約を用います。整数エンコーディングでは、標準的な整数の順序制約（$x < 2^n$）を使用してモデル化されます。
   • MemoryOp および MemoryInit: インデックスから証拠値（witness values）へのマップを使用して、配列の変異を追跡するように定式化されており、読み取り操作と書き込み操作の両方を逐次的に処理します。
   • BrilligCall: 制約なしコードを表します。これらは、常に充足される制約 true （または無視）として翻訳されます。これは、検証者の目的が制約なしブロックの外部にある制約をチェックすることだからです。

3. 検証ワークフロー:

   • 本ツールは、NoirのパッケージマネージャーであるNargoと統合され、formal-verify コマンドとして機能します。
   • 開発者は、Noirプログラムに verify_assert(b: bool) ステートメントを付与します。標準的な assert 文が回路制約を生成するのに対し、verify_assert は証明義務（proof obligation）を作成します。
   • NAVeはNoirプログラムをACIRにコンパイルし、ACIRオペコードをSMT公式に翻訳し、検証式 $F = \text{ACIR}_{\text{constraints}} \land \neg \text{verify\_assert}_{\text{condition}}$ を構築します。
   • cvc5 ソルバーが $F$ の充足可能性をチェックします。もし $F$ が**充足不能（unsatisfiable）であれば、検証条件は成立しています（プログラムは正しく制約されています）。もし $F$ が充足可能（satisfiable）**であれば、ソルバーは条件を違反する証拠の割り当てを示すモデル（反例）を返し、デバッグを支援します。

主な貢献

• ACIRの定式化: メモリ操作、範囲チェック、および制約付きコードと制約なしコードの区別といった複雑な特徴をカバーする、SMT-LIBを用いたACIR言語のサブセットにおける初の定式化。
• デュアルエンコーディング戦略: 異なるソルバーの能力を活用するための、補完的な2つのエンコーディング（有限体理論と整数演算）の提案。
• NAVeツール: 対話的な定理証明を必要とせずに、開発者がアクセス可能なように設計された、Noirエコシステム（Nargo）に統合されたオープンソースの自動形式検証ツール。
• 実証的評価: さまざバックエンドや制約タイプ、ソルバー構成におけるパフォーマンスを分析するために、一連のNoirテストプログラムを用いてNAVeを包括的に評価。

結果
著者らは、cvc5 ソルバーを使用して、4つの異なるNoirプログラムのセット（検証済み条件、偽造された条件、および範囲チェックの有無を含む）に対してNAVeを評価しました。

• ソルバーのパフォーマンス: 単一のバックエンド（整数エンコーディング、有限体 --ff=gb、または有限体 --ff=split）が、一貫して他を圧倒することはありませんでした。この結果は、エンコーディングが補完的であることを示しています。あるプログラムはあるエンコーディングによって高速に解かれ、別のプログラムはその同じエンコーディングではタイムアウトするものの、別のエンコーディングでは成功するという現象が見られました。
• 範囲チェックの影響: Range チェック（BlackBoxFuncCall オペコード）を含むプログラムは、検証時間を大幅に増加させました。デフォルトの --ff=gb 設定と比較して、有限体理論を近似する --ff=split 設定は、大規模な範囲チェックを伴うプログラムにおいて優れたパフォーマンスを示しましたが、複雑なケースでは依然としてタイムアウトが発生しました。
• 反例の生成: 本ツールは、偽造された条件に対して反例の生成に成功し、制約不足のロジックを特定する上での有用性を実証しました。

意義と主張
本論文は、NAVeが、現実世界の脆弱性を引き起こしてきたエラーのクラスである「制約不足のバグ」に対して、高レベルのZKプログラムを検証するための自動化されたスケーラブルな手法を提供することで、ZKエコシステムの重要なギャップを埋めるものであると主張しています。ACIRをターゲットにすることで、ツールは高レベルのNoir構文の変化に対して堅牢であり、同じ中間表現をターゲットとする他の言語にも適用できる可能性があります。

著者らは、自らの研究をより広範な検証能力への一歩として控えめに位置づけています。現在の定式化はACIRのサブセット（再帰的な Call オペコードや、Range を除くほとんどの BlackBoxFuncCall を除く）のみをカバーしていることを認めています。また、範囲チェックの検証コストが高いことを主要な制限事項として特定しており、将来の研究は、これらの複雑な制約を効率的に扱うための抽象化や近似の開発に焦点を当てる必要があると示唆しています。論文は、NAVeをすべてのZK検証ニーズに対する完全な解決策としてではなく、高レベルのNoirプログラムの自動形式検証の実現可能性を示し、複雑なビットレベルの制約に対するソルバーのハンドリングを改善するための道筋を示す、実用的かつ統合されたツールとして位置づけています。