Project/Area Number |
17K12667
|
Research Category |
Grant-in-Aid for Young Scientists (B)
|
Allocation Type | Multi-year Fund |
Research Field |
Software
|
Research Institution | National Institute of Advanced Industrial Science and Technology |
Principal Investigator |
Kawamoto Yusuke 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (60760006)
|
Project Period (FY) |
2017-04-01 – 2020-03-31
|
Project Status |
Completed (Fiscal Year 2019)
|
Budget Amount *help |
¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2019: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2018: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
Keywords | 情報セキュリティ / プライバシ / システム検証 / 形式手法 / 定量的情報流解析 / 差分プライバシ / 情報理論 / 様相論理 / 形式仕様 / 認識論理 / 確率分布 / 最適輸送理論 / 機械学習 / ゲーム理論 / プログラム検証 / 統計手法 |
Outline of Final Research Achievements |
We studied theories and techniques for modeling, analyzing, and verifying quantitative properties of cyber-physical systems (CPSs). First, we developed HyLeak, a tool for estimating information leakage in programs by combining program analysis with statistical analysis. Second, we investigated quantitative models for privacy leakage in CPSs, proposed privacy protection mechanisms based on game theory and differential privacy, and demonstrated that the proposed mechanisms are effective for location-based services. Third, we introduced StatEL (statistical epistemic logic), a modal logic for describing statistical knowledge, and showed how this logic can be used to formalize the statistical specification of machine learning models used inside CPSs.
|
Academic Significance and Societal Importance of the Research Achievements |
サイバーフィジカルシステム(CPS)の確率的な振る舞いをモデル化・解析・検証する上で、形式的アプローチと統計的アプローチの融合が有用であるということを様々な観点において明らかにした。具体的には、プログラム解析と統計手法の融合により、システムからの情報漏洩量の推定を高速化できることを示した。また、ゲーム理論と情報理論を組み合わせることで、適応的な攻撃者と防御者の下での情報漏洩のモデル化・解析を実現した。また、機械学習モデルを部品として用いるCPSの形式仕様を記述する手法を開発するために、統計的認識論理を導入し、機械学習モデルの統計的性質を論理式で形式化する手法を初めて提案した。
|