差分プライバシーの検証の基盤となる形式化の構築

• 研究課題/領域番号: 24K14893
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60050:ソフトウェア関連
• 研究機関: 東京工業大学
• 研究代表者: 佐藤 哲也 東京工業大学, 情報理工学院, 助教 (40761797)
• 研究期間 (年度): 2024-04-01 – 2028-03-31
• 研究課題ステータス: 交付 (2024年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2027年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2026年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2025年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2024年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
• キーワード: 差分プライバシー / 定理証明支援系 / プログラム検証 / 確率的プログラム / プログラミング言語理論

研究開始時の研究の概要

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