• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 17K12667
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeMulti-year Fund
Research Field Software
Research InstitutionNational 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)
  • 2019 Annual Research Report   Final Research Report ( PDF )
  • 2018 Research-status Report
  • 2017 Research-status Report
  • Research Products

    (34 results)

All 2019 2018 2017 Other

All Int'l Joint Research (5 results) Journal Article (12 results) (of which Int'l Joint Research: 6 results,  Peer Reviewed: 12 results,  Open Access: 3 results) Presentation (15 results) (of which Int'l Joint Research: 13 results,  Invited: 1 results) Remarks (1 results) Patent(Industrial Property Rights) (1 results)

  • [Int'l Joint Research] Inria Saclay(フランス)

    • Related Report
      2019 Annual Research Report
  • [Int'l Joint Research] Inria Saclay(フランス)

    • Related Report
      2018 Research-status Report
  • [Int'l Joint Research] Federal University of Minas Gerais(ブラジル)

    • Related Report
      2018 Research-status Report
  • [Int'l Joint Research] Inria Saclay/Inria Rennes(France)

    • Related Report
      2017 Research-status Report
  • [Int'l Joint Research] Federal University of Minas Gerais(Brazil)

    • Related Report
      2017 Research-status Report
  • [Journal Article] Utility-Optimized Local Differential Privacy Mechanisms for Distribution Estimation2019

    • Author(s)
      Takao Murakami and Yusuke Kawamoto
    • Journal Title

      Proc. of the 28th USENIX Security Symposium (USENIX Security 2019)

      Volume: - Pages: 1877-1894

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Local Obfuscation Mechanisms for Hiding Probability Distributions2019

    • Author(s)
      Yusuke Kawamoto and Takao Murakami
    • Journal Title

      Proc. of the 24th European Symposium on Research in Computer Security (ESORICS 2019), Part I, Lecture Notes in Computer Science

      Volume: 11735 Pages: 128-148

    • DOI

      10.1007/978-3-030-29959-0_7

    • ISBN
      9783030299583, 9783030299590
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Local Distribution Obfuscation via Probability Coupling2019

    • Author(s)
      Yusuke Kawamoto and Takao Murakami
    • Journal Title

      Proc. of the 57th Annual Allerton Conference on Communication, Control, and Computing (Allerton 2019)

      Volume: - Pages: 718-725

    • DOI

      10.1109/allerton.2019.8919803

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Towards Logical Specification of Statistical Machine Learning2019

    • Author(s)
      Yusuke Kawamoto
    • Journal Title

      Proc. of the 17th International Conference on Software Engineering and Formal Methods (SEFM 2019), Lecture Notes in Computer Science

      Volume: 11724 Pages: 293-311

    • DOI

      10.1007/978-3-030-30446-1_16

    • ISBN
      9783030304454, 9783030304461
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [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

      10.1007/978-3-030-31175-9_20

    • ISBN
      9783030311742, 9783030311759
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Hybrid Statistical Estimation of Mutual Information and its Application to Information Flow2019

    • Author(s)
      Fabrizio Biondi, Yusuke Kawamoto, Axel Legay, and Louis-Marie Traonouez
    • Journal Title

      Formal Aspects of Computing

      Volume: 31(2) Issue: 2 Pages: 165-206

    • DOI

      10.1007/s00165-018-0469-z

    • Related Report
      2018 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] A Game-Theoretic Approach to Information-Flow Control via Protocol Composition2018

    • Author(s)
      Mario S. Alvim, Konstantinos Chatzikokolakis, Yusuke Kawamoto, and Catuscia Palamidessi
    • Journal Title

      Entropy

      Volume: 20(5:382) Issue: 5 Pages: 1-43

    • DOI

      10.3390/e20050382

    • Related Report
      2018 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] On the Anonymization of Differentially Private Location Obfuscation2018

    • Author(s)
      Yusuke Kawamoto and Takao Murakami
    • Journal Title

      Proc. of the 2018 International Symposium on Information Theory and Its Applications (ISITA 2018)

      Volume: - Pages: 159-163

    • DOI

      10.23919/isita.2018.8664351

    • Related Report
      2018 Research-status Report
    • Peer Reviewed
  • [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

      10.1007/978-3-319-89722-6_6

    • ISBN
      9783319897219, 9783319897226
    • Related Report
      2017 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] On the Compositionality of Quantitative Information Flow2017

    • Author(s)
      Yusuke Kawamoto, Konstantinos Chatzikokolakis, and Catuscia Palamidessi
    • Journal Title

      Logical Methods in Computer Science

      Volume: 13 Pages: 1-31

    • DOI

      10.23638/LMCS-13(3:11)2017

    • Related Report
      2017 Research-status Report
    • Peer Reviewed / Open Access / 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

      10.1007/978-3-319-68167-2_11

    • ISBN
      9783319681665, 9783319681672
    • Related Report
      2017 Research-status 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

      10.1007/978-3-319-68711-7_23

    • ISBN
      9783319687100, 9783319687117
    • Related Report
      2017 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] Utility-Optimized Local Differential Privacy Mechanisms for Distribution Estimation2019

    • Author(s)
      Takao Murakami
    • Organizer
      28th USENIX Security Symposium (USENIX Security 2019)
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Local Obfuscation Mechanisms for Hiding Probability Distributions2019

    • Author(s)
      Yusuke Kawamoto
    • Organizer
      24th European Symposium on Research in Computer Security (ESORICS 2019)
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Local Distribution Obfuscation via Probability Coupling2019

    • Author(s)
      Yusuke Kawamoto
    • Organizer
      57th Annual Allerton Conference on Communication, Control, and Computing (Allerton 2019)
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Towards Logical Specification of Statistical Machine Learning2019

    • Author(s)
      Yusuke Kawamoto
    • Organizer
      17th International Conference on Software Engineering and Formal Methods (SEFM 2019)
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Statistical Epistemic Logic2019

    • Author(s)
      Yusuke Kawamoto
    • Organizer
      The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Epistemic logic for expressing the statistical security of machine learning2019

    • Author(s)
      Yusuke Kawamoto
    • Organizer
      5th France-Japan Cybersecurity Workshop
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 情報量を利得とするゲームとプライバシー定量化への応用2019

    • Author(s)
      川本裕輔
    • Organizer
      ゲーム理論ワークショップ2019
    • Related Report
      2018 Research-status Report
  • [Presentation] Obfuscation Mechanisms with Distribution Privacy2018

    • Author(s)
      Yusuke Kawamoto
    • Organizer
      4th Franco-Japanese Cybersecurity Workshop
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] On the Anonymization of Differentially Private Location Obfuscation2018

    • Author(s)
      Yusuke Kawamoto and Takao Murakami
    • Organizer
      2018 International Symposium on Information Theory and Its Applications (ISITA 2018)
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] Extension of Differential Privacy to Distribution Obfuscation2018

    • Author(s)
      Yusuke Kawamoto
    • Organizer
      NII Shonan Meeting Seminar 116
    • Related Report
      2017 Research-status Report
    • Int'l Joint Research
  • [Presentation] Leakage and Protocol Composition in a Game-Theoretic Perspective2018

    • Author(s)
      Mario S. Alvim, Konstantinos Chatzikokolakis, Yusuke Kawamoto, and Catuscia Palamidessi
    • Organizer
      7th International Conference on Principles of Security and Trust (POST 2018)
    • Related Report
      2017 Research-status Report
    • Int'l Joint Research
  • [Presentation] Modeling and Analysis of Information Leakage2017

    • Author(s)
      Yusuke Kawamoto
    • Organizer
      Third French Japanese Meeting on Cybersecurity
    • Related Report
      2017 Research-status Report
    • Int'l Joint Research
  • [Presentation] プライバシの定量的モデルと保護メカニズム2017

    • Author(s)
      川本裕輔
    • Organizer
      日本応用数理学会2017年度年会 「数理的技法による情報セキュリティ」研究部会
    • Related Report
      2017 Research-status Report
    • Invited
  • [Presentation] HyLeak: Hybrid Analysis Tool for Information Leakage2017

    • Author(s)
      Fabrizio Biondi, Yusuke Kawamoto, Axel Legay, and Louis-Marie Traonouez
    • Organizer
      15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017)
    • Related Report
      2017 Research-status Report
    • 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
      2017 Research-status Report
    • Int'l Joint Research
  • [Remarks] Hybrid Analysis Tool for Information Leakage

    • URL

      https://project.inria.fr/hyleak/

    • Related Report
      2017 Research-status Report
  • [Patent(Industrial Property Rights)] タイミング攻撃に対抗するための情報処理方法、システム及びプログラム2018

    • Inventor(s)
      川本 裕輔,村上隆夫
    • Industrial Property Rights Holder
      産業技術総合研究所
    • Industrial Property Rights Type
      特許
    • Industrial Property Number
      2018-153830
    • Filing Date
      2018
    • Related Report
      2018 Research-status Report

URL: 

Published: 2017-04-28   Modified: 2021-02-19  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi