Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs

技術要約：Elton: 敵対的な確率プログラムに関する推論のためのurnリソース

問題提起
確率的プログラムの形式検証は、ランダム化アルゴリズム、機械学習、差分プライバシー、および暗号学的安全性において極めて重要である。特定の課題は、暗号学的安全性において発生する。そこでは、未知の任意の敵対的なコードが存在する場合でも成立する性質を確立しなければならない。高階分離論理（higher-order separation logics）は、非確率的な設定において敵対的な相互作用をモデル化することに成功してきたが、これを確率的プログラムへと拡張することは困難である。核心的な困難は、未知の敵対者の振る舞いが存在する状況下で、確率的選択、高階関数、およびローカル状態の組み合わせについて推論することにある。

既存の検証技術は、以下の「トリレンマ」に直面している：

1. 分布論理（Distributional Logics）: 述語が状態の分布を記述することを可能にする（「値は一様分布である」といった不変量を記述するのに有用）。しかし、複雑な敵対的相互作用をモデル化するために必要な表現力（高階関数や一般的な参照など）に欠けることが多い。
2. リフティングベースの論理（Lifting-Based Logics）: 標準的な状態ベースの述語を保持し、それらを分布へとリフトアップする（高階の特徴を拡張しやすい）。しかし、分布的な不変量（例えば、敵対者がランダムビットに偏りを与えることができないことを証明するために必要なもの）を表現することに苦慮する。
3. 敵対的推論（Adversarial Reasoning）: 既存のアプローチは、未知のコード、高階状態、および分布的不変量の同時的な組み合わせを扱うことに失敗することが多い。例えば、標準的な「予言変数（prophecy variables）」や「プリサンプリング・テープ（presampling tapes）」（Clutchのような論理で使用される）は、未知の敵対者のコードの出力を健全に予測することはできず、また、ランダムサンプリングと敵対的な呼び出しの順序が入れ替わった場合を容易に扱うこともできない。

手法
著者らは、未知の敵対的コードが存在する状況下での確率的プログラムの堅牢な安全性を推論するために設計された、高階分離論理であるEltonを提示する。Eltonは、「混合」アプローチを採用しており、リフティングベースの論理（Irisフレームワーク上に構築されたもの）の構造的な利点と、分布的特性を捉えるための新しいメカニズムを組み合わせている。

この手法は、主に2つの拡張に基づいている：

1. 遅延サンプリング（演算意味論）:
   Eltonは、drandプリミティブを備えた言語（RandML）のバリアントを導入する。標準的なランダムサンプリング（rand）とは異なり、drandは即座に値へと解決されない。代わりに、それは記号的な「urn（壺）」（可能な値の集合）を作成し、「urnラベル」を返す。これらのラベルを含む計算は、「遅延された値（delayed values）」（記号的な式）を生成する。これにより、論理が敵対者がシステムと相互作用した後に、ランダム性の解決を遅延させることが可能になる。演算意味論は、これらの遅延された計算が、標準的なコールバイバリューの確率的意味論へと健全に消去（erase）可能であることを保証する。

2. urnリソース（論理的機能）:
   論理レベルにおいて、Eltonはurnリソース（$\iota \sim s$と表記）を導入する。これは、遅延されたサンプル変数 $\iota$ が集合 $s$ 上で一様分布であることを主張するものである。これにより、論理は分離論理の表現力を放棄することなく、状態の分布について推論することが可能となる。
   urnリソースの証明プロセスは、以下の3段階のライフサイクルに従う：

• 生成（Creation）: drandプリミティブがurnリソースを作成する。
• 解決（Resolution）: 論理は、urnリソースを（例えば、敵対者が推測した特定の値を避けるように）部分集合へと分割し、それに応じて「エラークレジット（誤差の境界）」を分配することができる。これはht-resolve-partialのような規則によって制御される。
• 昇格（Promotion）: 敵対者の相互作用が完了し、分布的特性が確立された後、「遅延された値」は、現在のurnリ訳の下で意味的等価性を主張するpromote update述語（$v \mapsto [R] w$）を用いて、具体的な値へと昇格される。

Eltonは、その前身であるErisから「エラークレジット」メカニズムを継承して誤差確率を制限し、型に基づいた未知の、ウェルタイピングされた敵対者の仕様を導出するために**論理関係（logical relations）**を利用する。

主な貢献
本論文は、以下の貢献を主張している：

• 初の確率的高階分離論理: Eltonは、未知の敵対的コード、高階ローカル状態、および分布的不変量を同時に扱うことができる初の論理である。
• 新しい演算意味論: 遅延サンプリングと停止された値の記号的実行をサポートする意味論を導入し、標準的なコールバイバリューの確率的意味論への消去を通じて健全性を証明した。
• urnリソース: 遅延サンプリングから生じる状態の分布を推論するための新しい分離論理リソース。
• 健全性と妥当性: 遅延サンプリングの意味論と標準的な意味論を接続する形式的な健全性証明を提供し、遅延版での証明が標準版における誤差境界を意味することを保証する。
• 機械化されたケーススタディ: すべての結果は、IrisフレームワークとCoquelicotライブラリを用いて、Rocq証明助手（旧Coq）内で機械化されている。論文では、以下の複雑な例を通じてEltonの表現力を実証している：
  • インタラクティブな推測: 秘密を推測する試行回数が未知である敵対者に対する誤差境界の証明。
  • 複雑なコイン投げ（Complicated Flip）: 敵対者がクロージャを通じて状態を操作できる場合でも、直接状態を読み取ることができない限り、プログラムが一様分布のビットを返すことを検証する。
  • 原像耐性（Preimage Resistance）: インタラクティブな敵対者に対するランダムオラクルハッシュモデルの原像耐性の定式化。
  • 非連結性（Unlinkability）: Basic Hashプロトコルの非連結性の検証。
  • 離散対数問題: ジェネリックグループモデルにおけるジェネリックアルゴリズムに対する誤差境界の、初の機械化された形式的証明の提供。

結果
著者らは、Eltonが、既存の手法では範囲外であった幅広いセキュリティ事例の誤差境界を証明できることを示している。具体的には：

• Eltonは、ランダムサンプリングと敵対的呼び出しの順序が入れ替わったシナリオ（例：guess2）を正常に処理できる（これは標準的なErisの規則が失敗するケースである）。
• 動的に割り当てられたローカル状態や複雑な確率的推論を含む特性（例：Basic Hashプロトコルの非連結性）を検証できる。
• ジェネリックグループモデルにおける離散対数問題に関する形式的証明を提供し、これはShoupによって確立された誤差境界と一致するが、インタラクティブなプログラムに対する精密な演算意味論の範囲内で行われる。

意義
本論文は、Eltonを暗号プロトコルの形式検証における重要な進歩として位置づけている。リフティングベースの論理（複雑な言語的特徴を扱う）と分布論理（確率的不変量を扱う）の間の溝を埋めることで、Eltonは、簡略化されたモデルやアドホックな構文的制限に頼ることなく、未知の敵対者の存在下でのセキュリティ特性の検証を可能にする。著者らは、現在のアプローチは一様分布に限定されており、より複雑な分布（非一様または無限分布など）をサポートするには大幅な修正が必要であるが、リフティングベースの論理フレームワーク内で分布的特性を表現するための有望な基礎を築いていると述べている。本研究は完全に機械化されており、導出されたセキュリティ保証に対して高い信頼性を提供している。