Foundations of formalization of differential privacy for formal verification

• Project/Area Number: 24K14893
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: 佐藤 哲也 東京工業大学, 情報理工学院, 助教 (40761797)
• Project Period (FY): 2024-04-01 – 2028-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2027: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2026: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2025: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2024: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
• Keywords: 差分プライバシー / 定理証明支援系 / プログラム検証 / 確率的プログラム / プログラミング言語理論

Outline of Research at the Start

機械学習によるデータ処理が普及し、データベースが大規模化しつつある今日の社会的状況において、個人情報を保護するプライバシー技術の重要性はますます高まりを見せている。本研究では、数学的なプライバシーの基準である差分プライバシーについて、定理証明支援系による検証の有効性を明らかにすべく、定理証明支援系上で形式化を与え、差分プライバシーの検証を行うための基盤となるライブラリを整備し、具体的なメカニズムの差分プライバシーの検証する。