Quantitative Verification of Cyber-Physical Systems by Integrating Statistical and Formal Approaches

2019 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

情報セキュリティ

Academic Significance and Societal Importance of the Research Achievements

サイバーフィジカルシステム(CPS)の確率的な振る舞いをモデル化・解析・検証する上で、形式的アプローチと統計的アプローチの融合が有用であるということを様々な観点において明らかにした。具体的には、プログラム解析と統計手法の融合により、システムからの情報漏洩量の推定を高速化できることを示した。また、ゲーム理論と情報理論を組み合わせることで、適応的な攻撃者と防御者の下での情報漏洩のモデル化・解析を実現した。また、機械学習モデルを部品として用いるCPSの形式仕様を記述する手法を開発するために、統計的認識論理を導入し、機械学習モデルの統計的性質を論理式で形式化する手法を初めて提案した。