IoT システムのための形式検証手法の深化

• Project/Area Number: 19H04084
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Kyoto University
• Principal Investigator: 末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
• Co-Investigator(Kenkyū-buntansha): 五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456) ; 海野 広志 筑波大学, システム情報系, 准教授 (80569575) ; 池渕 未来 京都大学, 情報学研究科, 助教 (70961796)
• Project Period (FY): 2019-04-01 – 2024-03-31
• Project Status: Completed (Fiscal Year 2023)
• Budget Amount: ¥17,030,000 (Direct Cost: ¥13,100,000、Indirect Cost: ¥3,930,000); Fiscal Year 2023: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2022: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2021: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000); Fiscal Year 2020: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2019: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
• Keywords: モデル検査 / PDR / IoT / プログラム検証 / 形式検証 / 強化学習 / 機械学習 / ハイブリッドシステム / 形式手法

Outline of Research at the Start

IoT システムの安全性保証は，IoT の普及とその safety-critical な場面での利用が進むにつれ，大きな社会的課題となりつつある．この課題の解決のために大規模な IoT システムの非自明な安全性を保証するための形式検証手法を提案する．具体的には，ソフトウェア検証の分野で成功を収めている検証手法を拡張し，人間が援助することによって自動検証プロセスをガイドするための手法を目指す．

Outline of Annual Research Achievements

IoTシステムのための形式検証手法として，以下の手法について研究を行った．
確率的な挙動を行い，かつ内部動作がブラックボックスであるようなIoTシステムを，モデル検査と動的検査を組み合わせて検証する手法を研究した．この手法では，ブラックボックスシステムに対してシステマティックに生成された入力を与え，その挙動に関するデータを得ることで，この挙動を模倣するMDPを得る．その上で，得られたMDPに対して確率的モデル検査を適用し，仕様の充足可能性を最大化するようなスケジューラを得る．このスケジューラをブラックボックスシステムに対して適用し，実際に動作させたうえで，同じ確率で仕様が充足されるかどうかを判断する．もし異なる確率が得られた場合には，再度MDPの学習を進め，より正確なMDPを得ることで，ブラックボックスシステムの検査を継続する．この手法により，確率的挙動を示すブラックボックスシステムの仕様の充足確率を，従来手法より高速かつ正確に見積もれることを実験的に確認した．
また，IoTシステムの重要な構成要素であるハイブリッドシステムについて，ブラックボックスなハイブリッドシステムからその挙動を模倣するハイブリッドオートマトンを得る手法を提案した．この手法では，ハイブリッドシステムに対して様々な入力を与え，得られた出力からハイブリッドオートマトンを構成する．上記の手法と同様に，ブラックボックス検査への応用が期待される．

Research Progress Status

令和5年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

令和5年度が最終年度であるため、記入しない。

Research Products

• [Journal Article] Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs (2024)
  • Author(s): Kawamoto Yusuke、Sato Tetsuya、Suenaga Kohei
  • Journal Title: Artificial Intelligence Volume: 326 Pages: 104045-104045
  • DOI: 10.1016/j.artint.2023.104045
  • Peer Reviewed / Open Access
• [Journal Article] HEIR: A Unified Representation for Cross-Scheme Compilation of Fully Homomorphic Computation (2024)
  • Author(s): Bian Song、Zhao Zian、Zhang Zhou、Mao Ran、Suenaga Kohei、Jin Yier、Guan Zhenyu、Liu Jianwei
  • Journal Title: Proceedings of NDSS 2022 Volume: －
  • DOI: 10.14722/ndss.2024.23067
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] Formalizing Statistical Causality via Modal Logic (2023)
  • Author(s): Kawamoto Yusuke、Sato Tetsuya、Suenaga Kohei
  • Journal Title: Logics in Artificial Intelligence: 18th European Conference, JELIA 2023, Dresden, Germany, September 20-22, 2023, Proceedings Volume: - Pages: 681-696
  • DOI: 10.1007/978-3-031-43619-2_46
  • ISBN: 9783031436185, 9783031436192
  • Peer Reviewed / Open Access
• [Journal Article] Probabilistic Black-Box Checking via Active MDP Learning (2023)
  • Author(s): Shijubo Junya、Waga Masaki、Suenaga Kohei
  • Journal Title: ACM Transactions on Embedded Computing Systems Volume: 22 Issue: 5s Pages: 1-26
  • DOI: 10.1145/3609127
  • Peer Reviewed / Open Access
• [Journal Article] Learning Nonlinear Hybrid Automata from?Input?Output Time-Series Data (2023)
  • Author(s): Gurung Amit、Waga Masaki、Suenaga Kohei
  • Journal Title: Automated Technology for Verification and Analysis. ATVA 2023 Volume: 14215 Pages: 33-52
  • DOI: 10.1007/978-3-031-45329-8_2
  • ISBN: 9783031453281, 9783031453298
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] BOREx: Bayesian-Optimization-Based Refinement of?Saliency Map for Image- and Video-Classification Models (2023)
  • Author(s): Kikuchi Atsushi、Uchida Kotaro、Waga Masaki、Suenaga Kohei
  • Journal Title: Proceedings of ACCV 2022 Volume: 13847 Pages: 274-290
  • DOI: 10.1007/978-3-031-26293-7_17
  • ISBN: 9783031262920, 9783031262937
  • Peer Reviewed / Open Access
• [Journal Article] Goal-Aware RSS for Complex Scenarios Via Program Logic (2022)
  • Author(s): Hasuo Ichiro、Eberhart Clovis、Haydon James、Dubut Jeremy、Bohrer Rose、Kobayashi Tsutomu、Pruekprasert Sasinee、Zhang Xiao-Yi、Pallas Erik Andre、Yamada Akihisa、Suenaga Kohei、Ishikawa Fuyuki、Kamijo Kenji、Shinya Yoshiyuki、Suetomi Takamasa
  • Journal Title: IEEE Transactions on Intelligent Vehicles Volume: (to appear) Issue: 4 Pages: 1-33
  • DOI: 10.1109/tiv.2022.3169762
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (2022)
  • Author(s): Banno Ryotaro、Matsuoka Kotaro、Matsumoto Naoki、Bian Song、Waga Masaki、Suenaga Kohei
  • Journal Title: 34th International Conference on Computer-Aided Verification Volume: 13371 Pages: 447-468
  • DOI: 10.1007/978-3-031-13185-1_22
  • ISBN: 9783031131844, 9783031131851
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] The Lattice-Theoretic Essence of?Property Directed Reachability Analysis (2022)
  • Author(s): Kori Mayuko、Urabe Natsuki、Katsumata Shin-ya、Suenaga Kohei、Hasuo Ichiro
  • Journal Title: Computer Aided Verification. CAV 2022. Lecture Notes in Computer Science. Volume: vol 13371 Pages: 235-256
  • DOI: 10.1007/978-3-031-13185-1_12
  • ISBN: 9783031131844, 9783031131851
  • Peer Reviewed / Open Access
• [Journal Article] Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types. (2022)
  • Author(s): Yuki Nishida, Hiromasa Saito, Chen Ran, Akira Kawata, Jun Furuse, Kouhei Suenaga and Atsushi Igarashi
  • Journal Title: New Generation Computing Volume: 40 Issue: 2 Pages: 507-540
  • DOI: 10.1007/s00354-022-00167-1
  • Peer Reviewed / Open Access
• [Journal Article] Efficient Black-Box Checking via Model Checking with Strengthened Specifications (2021)
  • Author(s): Shijubo Junya、Waga Masaki、Suenaga Kohei
  • Journal Title: Lecture Notes in Computer Science book series Volume: 12974 Pages: 100-120
  • DOI: 10.1007/978-3-030-88494-9_6
  • ISBN: 9783030884932, 9783030884949
  • Peer Reviewed
• [Journal Article] Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic (2021)
  • Author(s): Kawamoto Yusuke、Sato Tetsuya、Suenaga Kohei
  • Journal Title: Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning Volume: － Pages: 411-421
  • DOI: 10.24963/kr.2021/39
  • Peer Reviewed / Open Access
• [Journal Article] Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types (2021)
  • Author(s): Nishida Yuki、Saito Hiromasa、Chen Ran、Kawata Akira、Furuse Jun、Suenaga Kohei、Igarashi Atsushi
  • Journal Title: Proceedings of TACAS 2021, Springer LNCS Volume: 12652 Pages: 262-280
  • DOI: 10.1007/978-3-030-72013-1_14
  • ISBN: 9783030720124, 9783030720131
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs (2021)
  • Author(s): Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho 0002,
  • Journal Title: arXiv Volume: -
  • Open Access / Int'l Joint Research
• [Journal Article] Visualizing Color-Wise Saliency of Black-Box Image Classification Models (2021)
  • Author(s): Hatakeyama Yuhki、Sakuma Hiroki、Konishi Yoshinori、Suenaga Kohei
  • Journal Title: ACCV 2020 Volume: 12624 Pages: 189-205
  • DOI: 10.1007/978-3-030-69535-4_12
  • ISBN: 9783030695347, 9783030695354
  • Peer Reviewed / Open Access
• [Journal Article] ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs (2020)
  • Author(s): Toman John、Siqi Ren、Suenaga Kohei、Igarashi Atsushi、Kobayashi Naoki
  • Journal Title: Proceedings of ESOP 2020, Springer LNCS Volume: 12075 Pages: 684-714
  • DOI: 10.1007/978-3-030-44914-8_25
  • NAID: 120006879514
  • ISBN: 9783030449131, 9783030449148
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] Generalized Property-Directed Reachability for Hybrid Systems (2020)
  • Author(s): Suenaga Kohei、Ishizawa Takuya
  • Journal Title: VMCAI 2020 Volume: 11990 Pages: 293-313
  • DOI: 10.1007/978-3-030-39322-9_14
  • ISBN: 9783030393212, 9783030393229
  • Peer Reviewed / Open Access
• [Presentation] Oblivious Online Monitoring for?Safety LTL Specification via?Fully Homomorphic Encryption (2022)
  • Author(s): Banno Ryotaro、Matsuoka Kotaro、Matsumoto Naoki、Bian Song、Waga Masaki、Suenaga Kohei
  • Organizer: CAV 2022
  • Int'l Joint Research
• [Presentation] The Lattice-Theoretic Essence of?Property Directed Reachability Analysis (2022)
  • Author(s): Kori Mayuko、Urabe Natsuki、Katsumata Shin-ya、Suenaga Kohei、Hasuo Ichiro
  • Organizer: CAV 2022
  • Int'l Joint Research
• [Presentation] BOREx: Bayesian-Optimization-Based Refinement of?Saliency Map for Image- and Video-Classification Models (2022)
  • Author(s): Kikuchi Atsushi、Uchida Kotaro、Waga Masaki、Suenaga Kohei
  • Organizer: ACCV 2023
  • Int'l Joint Research
• [Presentation] HEIR: A Unified Representation for Cross-Scheme Compilation of Fully Homomorphic Computation (2022)
  • Author(s): Bian Song、Zhao Zian、Zhang Zhou、Mao Ran、Suenaga Kohei、Jin Yier、Guan Zhenyu、Liu Jianwei
  • Organizer: NDSS 2023
  • Int'l Joint Research
• [Presentation] スマートコントラクト検証器Helmholtzのためのエラー原因提示手法 (2022)
  • Author(s): 小野 雄登 , 西田 雄気 , 古瀬 淳 , 末永 幸平 , 五十嵐 淳
  • Organizer: 日本ソフトウェア科学会 第39回大会
• [Presentation] SCameleer: スマートコントラクト記述言語SCamlのための自動検証器 (2022)
  • Author(s): 服部 佑哉 , 西田 雄気 , 古瀬 淳 , 末永 幸平 , 五十嵐 淳
  • Organizer: 日本ソフトウェア科学会 第39回大会
• [Presentation] The Lattice-Theoretic Essence of Property Directed Reachability Analysis (2022)
  • Author(s): Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga, Ichiro Hasuo
  • Organizer: CAV 2022
  • Int'l Joint Research
• [Presentation] Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (2022)
  • Author(s): Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga, Kohei Suenaga
  • Organizer: CAV 2022
  • Int'l Joint Research
• [Presentation] 完全準同型暗号を用いた秘匿LTLオンラインモニタリング (2021)
  • Author(s): 伴野 良太郎 , 松岡 航太郎 , 松本 直樹 , Bian Song , 和賀 正樹 , 末永 幸平
  • Organizer: コンピュータセキュリティシンポジウム 2021 (CSS 2021)
• [Presentation] Efficient Black-Box Checking via Model Checking with Strengthened Specifications (2021)
  • Author(s): Junya Shijubo, Masaki Waga, Kohei Suenaga
  • Organizer: RV 2021
  • Int'l Joint Research
• [Presentation] Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic. (2021)
  • Author(s): Yusuke Kawamoto, Tetsuya Sato, Kohei Suenaga
  • Organizer: KR 2021
  • Int'l Joint Research
• [Presentation] Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types. (2021)
  • Author(s): Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, Atsushi Igarashi
  • Organizer: TACAS 2021
  • Int'l Joint Research
• [Presentation] 暗号通貨向けストレージシステムにおけるデータ永続化処理の形式検証 (2021)
  • Author(s): 伴野良太郎, 佐藤聡太, 古瀬淳, 末永幸平, 五十嵐淳
  • Organizer: PPL 2021
• [Presentation] 物理情報システムに対するブラックボックス検査の構文的仕様強化による最適化 (2021)
  • Author(s): 四十坊純也, 和賀正樹, 末永幸平
  • Organizer: PPL 2021
• [Presentation] ブラックボックス画像分類モデルの否定的判断根拠と色情報根拠の可視化 (2020)
  • Author(s): 畠山雄気, 佐久間宏樹, 小西嘉典, 末永幸平
  • Organizer: MIRU 2020
• [Presentation] F*を用いたMerkle Patricia Treeライブラリの形式検証 (2020)
  • Author(s): 佐藤 聡太, 古瀬 淳, 末永 幸平, 五十嵐 淳
  • Organizer: PPL 2020
• [Presentation] スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証 (2020)
  • Author(s): 齋藤 大聖, 西田 雄気, 五十嵐 淳, 末永 幸平
  • Organizer: PPL 2020
• [Book] プログラミング言語の形式的意味論入門 (2023)
  • Author(s): G.ウィンスケル (著), 末永 幸平 (監修, 翻訳), 勝股 審也 (翻訳), 中澤 巧爾 (翻訳)
  • Total Pages: 301
  • Publisher: 丸善出版
• [Book] 理論計算機科学事典（8.3節「型に基づくプログラム検証」） (2022)
  • Author(s): 徳山 豪、小林 直樹
  • Total Pages: 800
  • Publisher: 朝倉書店
  • ISBN: 9784254122633