Quantitative Verification of Cyber-Physical Systems by Integrating Statistical and Formal Approaches
| 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の形式仕様を記述する手法を開発するために、統計的認識論理を導入し、機械学習モデルの統計的性質を論理式で形式化する手法を初めて提案した。
|
Report
(4 results)
Research Products
(34 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Journal Article] Leakage and Protocol Composition in a Game-Theoretic Perspective2018
Author(s)
Mario S. Alvim, Konstantinos Chatzikokolakis, Yusuke Kawamoto, and Catuscia Palamidessi
-
Journal Title
Proc. of the 7th International Conference on Principles of Security and Trust (POST 2018), Lecture Notes in Computer Science
Volume: 10804
Pages: 134-159
DOI
ISBN
9783319897219, 9783319897226
Related Report
Peer Reviewed / Int'l Joint Research
-
-
[Journal Article] HyLeak: Hybrid Analysis Tool for Information Leakage2017
Author(s)
Fabrizio Biondi, Yusuke Kawamoto, Axel Legay, and Louis-Marie Traonouez
-
Journal Title
Proc. of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017), Lecture Notes in Computer Science
Volume: 10482
Pages: 156-163
DOI
ISBN
9783319681665, 9783319681672
Related Report
Peer Reviewed / Int'l Joint Research
-
[Journal Article] Information Leakage Games2017
Author(s)
Mario S. Alvim, Konstantinos Chatzikokolakis, Yusuke Kawamoto, and Catuscia Palamidessi
-
Journal Title
Proc. of the 8th International Conference on Decision and Game Theory for Security (GameSec 2017), Lecture Notes in Computer Science
Volume: 10575
Pages: 437-457
DOI
ISBN
9783319687100, 9783319687117
Related Report
Peer Reviewed / Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] Information Leakage Games2017
Author(s)
Mario S. Alvim, Konstantinos Chatzikokolakis, Yusuke Kawamoto, and Catuscia Palamidessi
Organizer
8th International Conference on Decision and Game Theory for Security (GameSec 2017)
Related Report
Int'l Joint Research
-
-
