Isabelle/HOLによる差分プライバシーの形式的検証についての進捗報告
TPP 2023
2023/10/31
佐藤哲也 (東京工業大学)(special thanks: 勝股審也・南出靖彦)

差分プライバシーの背景●

背景知識攻撃攻撃
内部データ

出力
データ集計処理–

内部データ自体は保護されていたとしても、十分な背景知識があると、データベースの出力を見て内部データを(統計的に)推測することが可能となる。

差分プライバシー●

ノイズ付加による匿名化技法

内部データ×

ノイズ付加

攻撃
出力

データ集計処理●–

ノイズを付加し、内部データの推測を困難にする。

–

背景知識攻撃(もっと言えば任意の統計的攻撃)に対して頑健。

差分プライバシー(Differential Privacy, DP)は、このような匿名化における、プライバシーの基準である

差分プライバシーの定義●

定義[Dwork+, TCC 2006]：–

ランダム化されたメカニズム M: X → Prob(Y) が(ε,δ)- 差分プライバシー (DP) を満たすとは、●“ 隣接する” 内部データ D1 ～ D2 について
（隣接関係、データ更新 D1 → D2 １ステップの差分）●

直観：確率 δ の場合を除き、確率比が ε で押さえられる((ε,δ)=(0,0) のとき、確率分布は一致する）

ラプラスメカニズム●

平均0分散 2ε^2 のラプラス分布からなるノイズを加算
これは(隣接関係を|x-y|≦1としたとき) (ε,0)-DPを満たす。

は平均 x 分散 2ε2 のラプラス分布

確率比(密度比)が一定以下

ガウシアンメカニズム●

平均０の正規分布を加算。(隣接関係を|x-y|≦1としたとき)適当なパラメータにおける(ε,δ)-DPを満たす。

は平均 x 分散 σ2 の正規分布
確率比は遠方で∞に発散、誤差δ>0分だけ端をカット
確率比に対応するεはδに依存して決まる

仮説検定的特徴づけ[Kariouz+, ICML 2015]●

ランダム化されたメカニズム M: X → Prob(Y) が(ε,δ)- 差分プライバシー (DP) を満たすことは以下と同値：–隣接する内部データ D1 ～ D2 についてRejection

Type I error

Sは、内部データがD1かD2かのどちらかを決定する手法と等価。
仮説検定の棄却域を検定統計量で引き戻した逆像。
どんな検定手法で内部データの弁別を試みても、誤りを一定以下にできない。

Type II error

privacy region差分プライバシーの合成性●

データベースの差分プライバシーは、処理ブロックごとに分割して評価することができる。
集計処理１

集計処理２

内部データ

出力
(ε1,δ1)-DP(ε2,δ2)-DP(ε1+ε2,δ1+δ2)-DP–

特に、決まった回数の繰り返しの差分プライバシーは、繰り返し回数とループ本体の差分プライバシーで求まる。

合成性に基づく形式的検証が厄介な例●

差分プライバシーを満たす勾配降下法[Lee & Kifer, KDD 2018]–

ノイズ持ち点 ρ を持っておく。
●

ρ がゼロになるまで以下を繰り返す：– ρから支払い、ノイズを付加した勾配ベクトルgtを取得●-gtが勾配を下る方向のときは-gtの方向に勾配降下。出力wをアップデートする。

●

そうでないときは、ρを払戻し、wをアップデートせず、若干大きなノイズを付加して方向ベクトルgtを取り直す。

●●

ρ は最終的には必ずゼロになり、必要なノイズが付加される。
持ち点 ρ のノイズを付加 ⇒ (ε,δ)-DPを保証。

なぜ厄介なのか●

分岐結果で付加するノイズ量やステップ数が動的に変化＋付加するノイズ量が多いとストッパーが働く
処理⇒ 実行パスを考慮した議論が必要
処理

処理

×処理
処理

理処理

処理

処理

処理
処理

×処理

処理
処理

×

着想
●

先ほどのような例の差分プライバシーを検証しようとすると、合成性を通した(保守的な)形式的検証はやりづらい。
–●●

実行パスを考慮した議論が上手く扱えるかがネック。

差分プライバシーの研究では様々な解析的手法が使われているが、それらについても厳密な検証もできるのではないか。
ラドン＝ニコディムの定理の形式化が様々な定理証明支援系で実装済。
–

過去の差分プライバシーの研究で、いかにこの定理に頼ってきたか。

–

連続的な確率分布に対応した形で差分プライバシーを形式化できそう。

差分プライバシーを直接形式化しよう！

Isabelle/HOLによるDPの形式化●●

Isabelle/HOLで差分プライバシーの形式化を進める。
–

測度論ライブラリがそろっている。

–

自動証明ツールsledgehammerが便利。

現在の進捗：差分プライバシーの議論のための部品の形式化を進行中：–

差分プライバシーに対応する統計的ダイバージェンス●–ラプラスメカニズム●–

定義・反射性・合成性など
ラプラス分布 (正規分布は標準ライブラリにある)

有限リストの可測空間(データセットの空間)●

位相的圏構造、直和可測空間、リスト操作の可測性

DPの統計的ダイバージェンスによる定式化[Barthe & Olmedo, ICALP 2013]●

M: X → Prob(Y) が(ε,δ)-DPを満たす⇔ 隣接する内部データD1～D2について⇔隣接する内部データD1～D2についてパラメータεのついたGiryモナド上のダイバージェンスとして解釈することができる(合成性・反射性)。

合成性の証明スケッチ

合成性の証明スケッチ
Giryモナドのbindを展開
共通の測度 π に関する
Radon-Nikodym 微分
積分の移項や変形をたくさん行う。

Bは前半の(...)が正になる
領域

２つの確率測度を比較する補題群(966行)
2つの確率測度をその和で微分したRadon-Nikodym微分の諸性質をまとめたlocaleを作る。

(中略、細かい補題たち。「MとNがL上の測度」とか)有限測度の、実数値のRadon-Nikodym微分をとる操作。
sigma_finite_measure.real_RN_deriv をもとにSOMEを使って構成。

(中略、Radon-Nikodym微分 dM, dNの非負性、可積分性、bindによる変形)１の分割をなす。

DP(のダイバージェンス)の形式化(597行)
計算上の都合で、ダイバージェンスの値の型を(定義)

ennreal=[0,∞]ではなくereal = [-∞,∞]でとる。

(非負性)(Giryモナド上のダイバージェンス[Sato&Katsumata,2023]の公理：単調性・反射性・合成性)

先ほどのlocaleを使う

合成性の形式的証明(主要部分外観)●

ほぼスケッチ通りの内容。

–

積分の移項が多いので非負積分でなく実関数の積分を採用。
(可積分性の証明の手間より、移項が楽になるほうが大きい)ラプラス分布・ラプラスメカニズムの形式化●

標準ライブラリ(HOL/Probability/Distributions)に正規分布の形式化があった(指数分布もあった、ラプラス分布はなかった)のでそれに倣った。
–

密度関数

–

累積分布関数●

同時に形式化する。密度関数と累積分布関数を用意して、微分積分学の基本定理(と広義積分)を適用する。
それから、合計が１になることを証明する。

–ｎ次モーメント●

一般形を先に与え、帰納法で証明する。
n+1のケースを部分積分法を使ってnのケースに帰着。

●

ラプラスメカニズムの構成と差分プライバシーの形式的証明は比較的安直にやれた。

ラプラス分布の形式化(864行)(密度関数と累積分布関数)(中略、可測性とか非負性とか)中心より右側の累積分布(左側も同様)[a,∞)型の広義積分の計算●

密度関数と累積分布関数に入っているif式を払うために、中心より右側と左側に分割して証明した。

ラプラス分布の形式化(n次のモーメント)

n次モーメントの中心より右側部分の計算

主に対称性からn次モーメントの計算をつくる。

ラプラスメカニズムの形式化(196行)(定義・基本的構造・可測性)(差分プライバシー)リスト可測空間の形式化(506+717+961行)●

構成はリスト準ボレル空間[Hirata+, ITP2023] を参考にした：
a)可算直積空間の形式化(標準ライブラリにある)b)可算直和空間の形式化(新しく作る)c) 直積と可算直和の分配律(新しく作る)d)同型写像で引き戻して●のσ代数を構成する(同型射にもなる)。

そのうえでリスト処理の可測性を形式的に証明する(進行中)：–

形式化済み：Cons, append, fold, foldr, foldl, rev, concat
ラムダ抽象や関数適用が一般に可測とは限らない。rec_listの可測性はうまく使えない。uncurryが随所に必要でかなりの手間が生じる。

「source」の形式化と直積●

可測空間
すべてのを備えた可測空間●と関数の族を考える
を可測ならしめる最も粗いσ代数
は、sourceと呼ばれる。

直積空間は射影引き戻したsourceに他ならない。

が可測になるようこれに限らず、Set上の任意の極限を可測空間化できる。
●。

Isablleにおける、sourceの定義と直積の定義の型は制限されている。
（依存型がないため）

標準ライブラリの直積空間と可測空間は一致。

「sink」の形式化●

可測空間
すべてのを備えた可測空間●

形式化と関数の族を考える
を可測ならしめる最も細かいσ代数
はsinkと呼ばれる。

。の型は制限されている。
（依存型がないため）

圏論的なsinkの定義を満足する：
(1)
は可測
(2)
が可測なら、圏論的なsinkの定義を満足するは可測※「最も細かい」ことも導ける。

直和可測空間の構成(245行)●

直和集合の余射影(埋め込み、coprojection)
で各を押し出したsinkは、直和空間に他ならない。
これに限らず、Set上の任意の余極限を可測空間化できる。

●

形式化(直和集合の構成は割愛)の可測性の可測性

（二項）直積と可算直和の分配律(266行)●

互いに可逆な可測関数を構成する(定義は省く)。とのσ代数の生成元を突き合わせる。

有限リストの可測空間の形式化(961行)●●

同型写像から作る(source/vimage)–

上記の2つのfunが実際に同型写像であることを示し、–sourceであることからそれらの可測性を証明する。

Cons(のuncurrying)が可測写像であること(補題含め合計150行ほど)–

可測性形式化済み：map, append, fold, foldr, foldl, rev, concat,

Future Work●

まずは簡単な差分プライバシーの検証例を構成する
実数のリストの全要素にラプラスメカニズムを適用

入力リストの隣接関係を定義し、差分プライバシーを示す。