高階確率的プログラムにおける差分プライバシーの形式的検証

高阶概率程序中差分隐私的形式化验证

基本信息

批准号：
20K19775
负责人：
佐藤哲也
金额：
$ 1.33万
依托单位：
Tokyo Institute of Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Early-Career Scientists
财政年份：
2020
资助国家：
日本
起止时间：
2020-04-01 至 2024-03-31
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20K19775/
关键词：
差分プライバシープログラミング言語理論圏論証明支援系確率的プログラムソフトウェア検証二項関係持ち上げ次数付きホーア論理形式的検証意味論プログラム検証確率的プログラミング言語高階プログラミング言語

项目摘要

本研究プロジェクトは（A）連続型の確率分布を含む高階確率的プログラムとして与えられるデータベースの差分プライバシーを検証するためのプログラム論理を構築する（B）左記のプログラム論理を定理証明支援系の上で実装し、ソフトウェア上でのプログラム検証の実現を目指す、の２段階に分かれている。本年度は以下のように研究を進めた。（A）については、前年度で構成した連続型の確率分布を含む高階確率的プログラムの差分プライバシーを検証する次数付きプログラム論理(勝股審也氏との共同研究、国際誌Mathematical Structures in Computer Scienceの特集号に投稿済・査読中)において、データベースの入力に依存するような差分プライバシーの特徴づけであるlocal sensiyivity/smooth sensitivityといった性質を検証することが困難であることを発見し、その解決策の一つとして項を次数にもつプログラム論理の構成を進め、その一般論の開発を行う途上である。（B）については、平田路和氏・南出靖彦氏との共同研究で構成したIsabelle/HOLによる高階確率的プログラムの検証ライブラリ(国際会議ITP2023採択決定済)において、形式化に適するような、s-有限測度モナドの構成と証明を与えた。このライブラリに差分プライバシーを測る基準となる統計的ダイバージェンスを組み込めば、(A)で触れたlocal sensiyivity/smooth sensitivityを含めた検証が可能となる。ただし当該統計的ダイバージェンス自身のIsabelle/HOL上による形式化を行う必要があるが、昨年度から、作業は難航している。特にRenyiダイバージェンスについての単純な形式化を得る必要がある。

该研究项目包括 (A) 构建一个程序逻辑来验证作为包含连续概率分布的高阶概率程序给出的数据库的差分隐私；以及 (B) 开发左侧描述的定理证明程序逻辑；支撑系统分为两个阶段：实现阶段和软件上实现程序验证的目的。今年，我们的研究进展如下。关于（A），我们开发了一定程度的程序逻辑，以验证包括前一年构建的连续概率分布在内的高阶概率程序的差分隐私（与 Shinya Katsumata 联合研究，发表在国际期刊 Mathematical Structures in Computer Science 上）。局部敏感性/平滑是依赖于数据库输入的差异隐私的表征，已提交至特刊，目前正在审查中。我们发现验证灵敏度等属性很困难，作为解决该问题的一种方法，我们正在着手构建以项为顺序的程序逻辑，目前正在开发其一般理论。关于（B），我们通过Isabelle/HOL创建了一个高阶概率程序的验证库（在国际会议ITP2023上通过），该验证库是通过与Michikazu Hirata和Yasuhiko Minamide的联合研究构建的，适合形式化。给出了s-有限测度单子的构造和证明。通过将统计差异（测量差异隐私的标准）纳入该库，可以验证（A）中提到的局部敏感度/平滑敏感度。然而，有必要使用 Isabelle/HOL 将统计散度本身形式化，但这项工作自去年以来一直很困难。特别是，我们需要获得 Renyi 散度的简单形式化。