2019 Fiscal Year Annual Research Report
Quantitative Verification of Cyber-Physical Systems by Integrating Statistical and Formal Approaches
| Project/Area Number |
17K12667
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
川本 裕輔 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (60760006)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | 情報セキュリティ / 形式仕様 / 様相論理 / 認識論理 / 差分プライバシ / 確率分布 / 最適輸送理論 / 機械学習 |
|---|
| Outline of Annual Research Achievements |
本研究は、サイバーフィジカルシステムの量的性質、特に情報漏洩やプライバシの度合いをモデル化・解析・検証する手法を開発することを目的としている。
本年度は、形式的アプローチと統計的アプローチの融合による仕様記述の枠組みや、サイバーフィジカルシステムにおけるプライバシの定量的なモデル化・解析・検証技術、およびその基礎となる理論や関連技術について、以下の研究に取り組んだ。
(1) 形式的アプローチと統計的アプローチの融合により、論理的知識と統計的知識を記述できる様相論理StatELを提案し、分布間の距離に基づく可能世界意味論を与えた。また、統計的仮説検定や機械学習モデルの様々な統計的性質（精度、頑健性、公平性など）をStatELの論理式を用いて形式化した。研究成果を査読付き国際会議で発表した。
(2) プライバシの量的性質、特に確率分布についての情報漏洩の度合いをモデル化し解析する枠組みを提案した。具体的には、差分プライバシを確率分布に持ち上げた「分布プライバシ」を定義し、確率的ノイズやダミーデータの付加で実現できる分布プライバシを理論的に明らかにし、最適輸送問題との関連を示した。実験では、サイバーフィジカルシステムとして位置情報サービスを対象とし、ユーザの属性情報の保護メカニズムの分布プライバシと有用性を実証した。研究成果を査読付き国際会議ESORICS'19とAllerton'19で発表した。
(3) プライバシの量的性質、特に差分プライバシの変種について研究をおこなった。具体的には、機微な情報のみを保護するメカニズムを提案し、実現できるプライバシや有用性を理論的に明らかにした。また、サイバーフィジカルシステムとして位置情報サービスを対象とした実験により、提案メカニズムの有用性を実証した。研究成果を査読付き国際会議USENIX Security'19で発表した。
|
-
-
-
-
-
-
[Journal Article] Statistical Epistemic Logic2019
Author(s)
Yusuke Kawamoto
-
Journal Title
The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy, Lecture Notes in Computer Science
Volume: 11760
Pages: 344-362
DOI
Peer Reviewed
-
-
-
-
-
-
