DPGen: Automated Program Synthesis for Differential Privacy
タイトル: DPGen: Automated Program Synthesis for Differential Privacy
著者: Yuxin Wang, Zeyu Ding, Yingtai Xiao, Daniel Kifer, Danfeng Zhang
CCS'21
TL;DR
non-privacyなコードに差分プライバシーを自動的に合成するツール
ノイズの候補となる場所を含むスケッチプログラムを自動的に生成し、スケッチプログラム上でプライバシー証明とノイズの規模を同時に最適化
DPGenはさまざまなプライバシーメカニズムからなる標準的なベンチマークで評価し、DPGenで合成したさまざまなメカニズムが𝜖-differential privacyを満たすことを証明
本文
背景
プライバシーメカニズムは,プライバシー保護を確実にするために非プライベートな計算にランダム性を入れる。しかし、このようなメカニズムを開発することは、いくつかの理由から困難な作業になっている。プライバシーの観点からは、どこにノイズを加えるかまたはどの程度のノイズを使用するかが、実用性の観点からは、non-privacyなプログラムをdifferential privacyなプログラムに変換する方法は数多くあり、そのようなオプションはそれぞれ大きく異なる有用性の特性を持つ可能性がある。SVTでは、ある特定の場所(閾値)にノイズを加えるすることでメカニズムが他の場所で使用するノイズを大幅に減らすことができる。ノイズの位置に関する様々な有効な選択とは別に、メカニズムはprivacy budgetを異なるコードフラグメントに割り当てる必要がある。その結果、privacy budgetの割合が大きいフラグメントほど、使用するノイズの量が少なくなるというトレードオフが生じる。ランダム性を追加し、privacy budgetを配分する最適な方法を選ぶことも、自明ではない作業である。
また、現在のほとんどのツールは、アルゴリズムのプライバシープロパティのチェックに重点を置いており、例えばプライバシーメカニズムが差分プライバシーを満たしていることを自動的に証明する検証ツールなどが多く開発されている。プライバシーメカニズムの正しさを保証するために非常に有用であるが、すべてのツールは、出発点として何かしらの差分プライベートアルゴリズムを必要とする。
DPGen
non-privacyなコードに差分プライバシーを自動的に合成するツール
ノイズの候補となる場所を含むスケッチプログラムを自動的に生成し、スケッチプログラム上でプライバシー証明とノイズの規模を同時に最適化
指定されたプライバシーバジェットを使い切るまでクエリを処理するようなメカニズムも合成可能
DPGenはさまざまなプライバシーメカニズムからなる標準的なベンチマークで評価し、DPGen合成したさまざまなメカニズムが𝜖-differential privacyを満たすことを証明
他のプログラムと比べてメカニズムの合成処理が速い
詳細
DPGenは2つのフェーズで合成作業を行う
https://gyazo.com/179a54d483d6483154a25c334ac4ad69
下記のコード(non-privacyなコード)をベースにフェーズ1、2を説明
https://gyazo.com/0b4f4b00ce2b3cc6fc5fda97ae8ed119
フェーズ1
ノイズの候補となる場所を含むスケッチメカニズムを生成。この段階では、必要以上のノイズ位置が含まれているが、不要なノイズ位置はフェーズ2で最適かされる
(1)ソースコードのどこでプライバシーが侵害されているかを特定
ソースコード内の違反を特定するためにstatic taint analysisを使用
(2)ランダム性を必要とする可能性のある変数のセットを推論
(3)特定された変数にノイズを注入するようにソースコードを修正
https://gyazo.com/8cec3ca6b48c44ed18d4e3b2cbffdc11
フェーズ2
メカニズム合成
スケールホール𝜆を含むスケールテンプレートSと、アライメントホール𝜃(合成すべきところ)を含む証明テンプレート(アラインメント(整列)の形式)Aの両方を持つ変換されたリレーショナルプログラムを生成
(1)各サンプリングコマンド(Lap(x))は、サンプルを読み取る非確率的対応物(non-probabilistic counterpart)($ \eta:=𝑠𝑎𝑚𝑝𝑙𝑒[𝑖𝑑𝑥];𝑖𝑑𝑥:=𝑖𝑑𝑥+ 1; )に置き換え
(2)各サンプリングコマンドに対してアライメントテンプレート(A)を生成
ランダム変数$ \eta_𝑖 に対する各アライメントテンプレート$ A_𝑖 は、(1)アサーションに登場し、(2)$ \eta_𝑖 に依存するプログラム変数の距離変数を含んでいる
(3)全体的なプライバシー・コストを追跡するために識別変数$ v_\epsilon を使用(さらに$ v_\epsilon =|A|/Sに更新される)
この更新は、ラプラス・ノイズをアライメントA とスケールSでラプラス・ノイズを整列させるというプライバシー・コストを適切に考慮している
(4)変換後のコードにアサーション(プライバシーを確保するためのアサーション)を挿入
アサーションは下記のプライバシーを保証する
スケッチ・メカニズムの2つの関連する実行が同じ制御フローに従うこと(例えば、14行目と18行目)
出力式の距離がゼロでなければならないこと(図7では、出力値が既にゼロ距離のリテラルであるため、存在しない)
プログラムの全体的なプライバシー・コストがプライバシー・バジェットを超えないこと(例えば、21行目)
https://gyazo.com/4fcf5df21fe36b4bc83f7b476c4148c5
メカニズム最適化
カスタマイズされたCounterexample-guided Inductive Synthesis (CEGIS)ループを用いてアライメントホール(𝜃)とスケールホール(𝜆)を見つける
https://gyazo.com/8290c08f3c2c48a88ec9d6d02f94e065
Counterexample Generationコンポーネント
メカニズム候補($ \theta_0=\vec0,\lambda_0=\vec1 のnullメカニズムで初期化)を用いて、𝑀′におけるアサーション違反になる入力𝑖𝑛𝑝を探す
Mechanism Generationコンポーネント
これまでに見出された反例のセットを用いて、以前に生成されたすべての反例を満足させつつ、utility objective function(本稿ではブラックボックス最適化手法としてParticle Swarm Optimization(PSO)を使用) を最適化することで、プライバシーメカニズムを合成
Note: 合成タスクでは、探索空間内の各メカニズム候補がPSOの粒子に相当し、スケッチ・メカニズムのインスタンスがその位置として機能する。各反復において,すべての候補は,現在のグローバルベスト候補(最高の効用を持つ),履歴上の自身のローカルベスト,および前の反復からの変更量に応じて,自身を少しずつ変化させながら探索空間を探索する。何回か繰り返した後に、最良解が返される
https://gyazo.com/d547bbc47a8e5274e0af90f581748df2
評価
異なる条件でのSVT,NumSVTやGapSVTなどのSVTの他の変形,Report Noisy Maxメカニズム,Partial SumやSmart Sumなどを用いて評価
合成されたランダム変数とそれに対応するアライメント証明・KOLAHALとの比較
https://gyazo.com/eff1c99788d0a52f07cd6e68bca37de1
参考
Sparse Vector Technique(SVT)
Particle Swarm Optimization(粒子群最適化)
自然界の鳥などの群れの行動にヒントを得たメタヒューリスティックな最適化アルゴリズム
探索空間に大量の解候補(「粒子」)を配置し,粒子が反復的に移動して最適な場所を探す。各粒子は、自分のローカルな最適位置、群の最適位置、前回の速度からなる数式に従って、反復ごとに位置と速度を更新する。この戦略を採用することで、群全体が最適なソリューションへと導かれる
The Sparse Vector Technique