形式検証とシステムソフトウェアの協働によるゼロトラストIoT

JST CREST研究領域：基礎理論とシステム基盤技術の融合によるSociety 5.0のための基盤ソフトウェアの創出 (S5基盤ソフト)

Topics

2023/11 SC23の展示会場で本ブロジェクトの展示発表を行いました． Link
2022/11/01 11/14-17にSC22の展示会場(Booth# 4205)で本ブロジェクトの展示発表を行います． PDF
2021/09/21 2021年度戦略的創造研究推進事業 (CREST)，研究領域「基礎理論とシステム基盤技術の融合によるSociety 5.0のための基盤ソフトウェアの創出 (S5基盤ソフト)」に採択されました．

研究概要

形式検証とシステムソフトウェアの融合により、ゼロトラスト(ZT)の概念を踏襲した安全なIoTシステムを実現します。理論研究では、IoTのトラストチェーンの正当性に数学的証明を与え、動的検証の併用で未知の脅威にも対応します。システムソフト研究では理論的成果と連係して実行隔離・自動検知・自動対処機構を開発し，ZT-IoTを実証します。アカウンタビリティを保証することでIoTの社会受容を促進します。

ZT-IoTプロジェクトの研究概要

メンバー

NIIシステムソフトウェアグループ

竹房あつ子 (研究代表者), 国立情報学研究所アーキテクチャ科学研究系教授
石川裕, 国立情報学研究所アーキテクチャ科学研究系教授
合田憲人, 国立情報学研究所アーキテクチャ科学研究系教授
清水さや子, 国立情報学研究所アーキテクチャ科学研究系助教
北川直哉, 国立情報学研究所学術ネットワーク研究開発センター特任准教授
小林久美子, 国立情報学研究所クラウド基盤研究開発センター特任研究員
坂根栄作, 国立情報学研究所アーキテクチャ科学研究系准教授
西村健, 国立情報学研究所学術基盤推進部特任研究員
丹生智也, 国立情報学研究所クラウド基盤研究開発センター特任研究員
YIN, Jie, 国立情報学研究所アーキテクチャ科学研究系特任研究員
青木信雄, 総合研究大学院大学先端学術院先端学術専攻情報学コース大学院生（博士課程）

京大理論グループ

五十嵐淳 (主たる共同研究者), 京都大学大学院情報学研究科教授
末永幸平, 京都大学大学院情報学研究科准教授
和賀正樹, 京都大学大学院情報学研究科助教
PARK, Sewon, 京都大学大学院情報学研究科特定研究員
神拓己，京都大学大学院情報学研究科情報学専攻大学院生 (修士課程)
西田雄気，京都大学大学院情報学研究科特定研究員 (〜2023年4月)
稲葉皓信, 京都大学大学院情報学研究科通信情報システム専攻大学院生 (修士課程) (〜2023年10月)
SHI, Zhen, 京都大学大学院情報学研究科通信情報システム専攻大学院生 (修士課程) (〜2023年3月)
阪口裕飛, 京都大学大学院情報学研究科通信情報システム専攻大学院生 (修士課程) (〜2023年3月))

NII理論グループ

関山太朗 (主たる共同研究者), 国立情報学研究所アーキテクチャ科学研究系准教授
石川冬樹, 国立情報学研究所アーキテクチャ科学研究系准教授
勝股審也, 国立情報学研究所アーキテクチャ科学研究系特任准教授
蓮尾一郎, 国立情報学研究所アーキテクチャ科学研究系教授
福田健介, 国立情報学研究所アーキテクチャ科学研究系教授
BRUN, Lelio, 国立情報学研究所アーキテクチャ科学研究系特任研究員
中林美郷, 総合研究大学院大学</a> 複合科学研究科情報学専攻大学院生（博士課程）
椎葉瑠星, 総合研究大学院大学複合科学研究科情報学専攻大学院生（博士課程）
藤浪大弥, 総合研究大学院大学複合科学研究科情報学専攻大学院生（博士課程）
田口研治, 国立情報学研究所アーキテクチャ科学研究系特任研究員 (〜2022年3月)

TIDシステムソフトウェアグループ

松井俊浩 (主たる共同研究者), 東京情報デザイン専門職大学情報デザイン学科教授
小野泰司, 東京情報デザイン専門職大学情報デザイン学科特任助手
若月里香, 東京情報デザイン専門職大学情報デザイン学科特任助手

IISECシステムソフトウェアグループ

須崎　有康 (主たる共同研究者), 情報セキュリティ大学院大学</a> 情報セキュリティ研究科教授
小野泰司, 情報セキュリティ大学院大学情報セキュリティ研究科特任助手
若月里香, 情報セキュリティ大学院大学情報セキュリティ研究科特任助手

研究業績

雑誌論文, 査読付き会議

2024年度

小林久美子, 竹房あつ子, 北川直哉, 大島浩太, 竹島雅之, 平田真樹, 森松文毅, 吉田浩, 合田憲人, IoT アプリケーションシステムのための SINETStream 多種センサデータ可視化・監視機能の開発, 学術情報処理研究 (JACN) (to appear).
Terunobu Inaba, Yutaka Ishikawa, Atsushi Igarashi, Taro Sekiyama, Rabbit: A Language to Model and Verify Data Flow in Networked Systems, Proc. the 11th International Symposium on Networks, Computers and Communications (ISNCC’24).
Masaki Waga, Kotaro Matsuoka, Takashi Suwa, Naoki Matsumoto, Ryotaro Banno, Song Bian, Kohei Suenaga, Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption, Proc. The 24th International Conference on Runtime Verification (RV 2024).
Taro Sekiyama, Hiroshi Unno, Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification, Proc. the ACM on Programming Languages (PACMPL).
Atsuya Osaki, Manuel Poisson, Seiki Makino, Ryusei Shiiba, Kensuke Fukuda, Tadashi Okoshi, Jin Nakazawa, Dynamic Fixed-point Values in eBPF: a Case for Fully In-kernel Anomaly Detection, Proc. AINTEC 2024, pp. 46-54, Aug. 2024. doi: 10.1145/3674213.3674219
Manuel Poisson, Rodrigo Carnier, Kensuke Fukuda, GothX: a generator of customizable, legitimate and malicious IoT network traffic, Proc. CSET 2024, pp. 65-73, Aug. 2024. doi: 10.1145/3675741.3675753
Jie Yin, Yutaka Ishikawa, Atsuko Takefusa, A Linux Audit and MQTT based Monitoring Framework for IoT Devices and Its Evaluation, IPSJ Journal special issue of “Applications and the internet” in conjunction with the main topics of COMPSAC 2023, vol. 65, no. 8, pp. 586-595, Aug. 2024. doi: 10.2197/ipsjjip.32.586
Yuye Uezato, Regular Expressions with Backreferences and Lookaheads Capture NLOG, Proc. the 51st International Colloquium on Automata, Languages, and Programming (ICALP), vol. 297, no. 155, pp. 1-20, Jul. 2024. doi: 10.4230/LIPICS.ICALP.2024.155
Takashi Yagawa, Tadanori Teruya, Kuniyasu Suzaki, Hirotake Abe, Delegating Verification for Remote Attestation using TEE, Proc. IEEE European Symposium on Security and Privacy Workshops (EuroS&PW), pp. 186-192, Jul. 2024. doi: 10.1109/EuroSPW61312.2024.00025
Chisa Ito, Atsuko Takefusa, Hidemoto Nakada, Masato Oguchi, Communication Performance Evaluation Using Compression Processing for IoT Systems in Mobile Environments, Proc. IEEE COMPSAC 2024, SIS-SS, pp. 2374-2379, Jul. 2024. doi: 10.1109/COMPSAC61105.2024.00380
Misato Nakabayashi, Taro Sekiyama, Ichiro Hasuo, Yutaka Ishikawa, Formal Support for Threat Modeling with Attack Decision Diagrams, Proc. the 18th IEEE International Workshop on Security, Trust, and Privacy for Software Applications, pp. 2454-2459, Jul. 2024. doi: 10.1109/COMPSAC61105.2024.00394
Nobuo Aoki, Atsuko Takefusa, Yutaka Ishikawa, Yasushi Ono, Eisaku Sakane, Kento Aida, ZT-OTA Update Framework for IoT Devices toward Zero Trust IoT, Proc. IEEE Computers, Software, and Applications Conference (COMPSAC 2024), NETSAP, pp. 2200-2207, Jul. 2024. doi: 10.1109/COMPSAC61105.2024.00352
須崎有康, IoTデバイスにおけるTEE (Trusted Execution Environment) の実装, システム制御情報学会システム/制御/情報「IoTとセキュリティ」特集号, vol. 68, no. 5, pp. 185-190, May 2024.
竹房あつ子, ゼロトラストIoTのためのシステムソフトウェア研究, システム制御情報学会システム/制御/情報「IoTとセキュリティ」特集号, vol. 68, no. 5, pp. 191-196, May 2024.
Hiroya Fujinami, Ichiro Hasuo, Efficient Matching with Memoization for Regexes with Grouping, Proc. the 33rd European Symposium on Programming, pp. 90-118, Apr. 2024. doi: 10.1007/978-3-031-57267-8_4

2023年度

Taichi Takemura, Ryo Yamamoto, Kuniyasu Suzaki, TEE-PA: TEE Is a Cornerstone for Remote Provenance Auditing on Edge Devices With Semi-TCB, IEEE ACCESS, vol. 12, pp. 26536-26549, Feb. 2024. doi: 10.1109/ACCESS.2024.3366344
Uyen Do, Laura Lahesoo, Rodrigo Matos Carnier, Kensuke Fukuda, Evaluation of XAI Algorithms in IoT Traffic Anomaly Detection, Proc. the 6th International Conference on Artificial Intelligence in Information and Communication, pp. 669-674, Feb. 2024. doi: 10.1109/ICAIIC60209.2024.10463357
Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi, Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers, Proc. the ACM on Programming Languages, pp. 115-147, Jan. 2024. doi 10.1145/3633280
Laura Lahesoo, Uyen Do, Rodrigo Carnier, Kensuke Fukuda, SIURU: A Framework for Machine Learning Based Anomaly Detection in IoT Network Traffic, Proc. the 18th Asian Internet Engineering Conference, pp. 87-95, Dec. 2023. doi: 10.1145/3630590.3630601
Lélio Brun, Ichiro Hasuo, Yasushi Ono and Taro Sekiyama, Automated Security Analysis for Real-World IoT Devices. Proc. HASP ‘23: Hardware and Architectural Support for Security and Privacy, pp 29-37, Oct. 2023. doi: 10.1145/3623652.3623667)
Jie Yin, Yutaka Ishikawa, Atsuko Takefusa, A Linux Audit and MQTT- based Security Monitoring Framework, Proc. IEEE COMPSAC 2023, pp. 648-657, Jun. 2023.
Taro Sekiyama, Unno Hiroshi, Temporal Verification with Answer-Effect Modification: Dependent Temporal Type- and-Effect System with Delimited Continuations, Proceedings of the ACM on Programming Languages (POPL), 7, POPL, pp. 2079-2110, Apr. 2023. doi: 10.1145/3571264
竹房あつ子, 小林久美子, 北川直哉, 孫静涛, 吉田浩, 合田憲人, IoTアプリ構築支援のためのSINETStream Androidライブラリおよびセンサ情報収集アプリの開発, 情報処理学会論文誌デジタルプラクティス(TDP), 4, pp. 110-121, 2023年4月. Link

2022年度

Naoya Kitagawa, Atsuko Takefusa, Kento Aida, Development of a Secure Data Sharing Mechanism for IoT Application Systems, Proc. 2022 IEEE 11th International Conference on Cloud Networking (CloudNet), pp. 131-135, Nov. 2022. doi: 10.1109/CloudNet55617.2022.9978835
Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga, Kohei Suenaga, Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption, Lecture Notes in Computer Science (Computer Aided Verification), 13371, pp. 447-468, Aug. 2022. Link

講演，口頭発表等

2024年度

[Invited Talk] 竹房あつ子, システムソフトウェアと形式検証によるゼロトラストIoTの実現, SASE・ハイブリッドワーク時代のセキュリティ 2024 秋, 基調講演, Oct. 2024.
[Poster] 青木信雄, 山下直希, 丹生智也, 坂根栄作, 合田憲人, 石川裕, 小野泰司, 竹房あつ子, IoTソフトウェアの信頼性とレジリエンスを高めるZT-OTA Update Frameworkのプロトタイプ実装, Computer Security Symposium 2024, Demonstration, Oct. 2024.
[Poster] Jie Yin, Yutaka Ishikawa, Atsuko Takefusa, Towards A light-weight Anomaly Detection Framework for IoT DevicesComputer Security Symposium 2024, Poster, Oct. 2024.
[Talk] 佐々木怜名, 石川裕, 竹房あつ子, 中田秀基, 小口正人, IoTシステムにおける属性ベース暗号の活用に向けた検討, Computer Security Symposium 2024, Oct. 2024.
[Poster] 佐々木怜名, 石川裕, 竹房あつ子, 中田秀基, 小口正人, 属性ベース暗号を用いたIoT通信の性能評価, xSIG 2024 (ポスター), Aug. 2024.
[Poster] Atsuko Takefusa, Yutaka Ishikawa, Yasushi Ono, Design of Trust Chained IoT Key Management using OP-TEE, USENIX OSDI ‘24, Poster, Jul. 2024.
[Poster] Lelio Brun, Taro Sekiyama, 実世界のIoTデバイスの自動セキュリティ分析, NIIオープンハウス2024 ポスター展示, Jun. 2024.
[Poster] 稲葉皓信, 関山太朗, 五十嵐淳, 石川裕, IoTシステムのモデル化とセキュリティ検証のためのプログラミング言語 Rabbit, NIIオープンハウス2024 ポスター展示, Jun. 2024.
[Poster] 竹房あつ子, 関山太郎, 福田健介, 蓮尾一郎, 合田憲人, 石川裕, Society 5.0のためのゼロトラストIoT, NIIオープンハウス2024 ポスター展示, Jun. 2024.
[Poster] 青木信雄, 竹房あつ子, 石川裕, 小野泰司, 坂根栄作, 合田憲人, IoTシステムのソフトウェアの信頼性とレジリエンスを強化するソフトウェア更新, NIIオープンハウス2024 ポスター展示, Jun. 2024.

2023年度

[Talk] 稲葉皓信, 五十嵐淳, 石川裕, 関山太朗, データフローセキュリティの検証のためのIoTシステムモデリング言語 Rabbit, 第26回プログラミングおよびプログラミング言語ワークショップ, Mar. 2024.
[Invited Talk] Atsuko Takefusa, System Software Studies towards Zero Trust IoT (ZT-IoT), Cloud-edge Fusion (CEF) Symposium, CENTRA 7, Feb. 2024.
[Talk] 中林美郷，関山太朗，蓮尾一郎，石川裕, 攻撃決定図の自動生成によるTamarin Proverの脅威モデリング支援, 2024年暗号と情報セキュリティシンポジウム(SCIS2024), Jan. 2024.
[Talk] 合田憲人, 山下直希, 丹生智也, 坂根栄作, 小野泰司, 青木信雄, 竹房あつ子, 石川裕, 研究ソフトウェア信頼性保証のためのソフトウェア認証機構, 2024年暗号と情報セキュリティシンポジウム(SCIS2024), Jan. 2024.
[Invited Talk] 竹房あつ子, SINETStreamによるIoTデータ利活用支援, データ活用社会創成シンポジウム2023, Dec. 2023.
竹房あつ子, 小野泰司, 石川裕, OP-TEEを用いたZero Trust IoTのための階層鍵管理機構の性能評価実験, インターネットと運用技術シンポジウム(IOTS2023) (ポスター), Dec. 2023.
[Exhibition] Zero Trust based IoT Security, SC23 Exhibition Booth #256, Nov. 2023． Link
[Invited Talk] 関山太朗, 形式検証によるセキュアなIoTシステムの実現に向けて, コンピュータセキュリティシンポジウムCSS2023 形式検証とセキュリティワークショップ, Nov. 2023.
[Talk] 青木信雄, 竹房あつ子, 石川裕, 小野泰司, 坂根栄作, 合田憲人, ゼロトラストIoTに向けたIoT機器のOTAソフトウェアアップデートフレームワークの検討, コンピュータセキュリティシンポジウムCSS2023論文集 2F3-4, pp. 652-659, Oct. 2023.
[Invited Talk] Taro Sekiyama, Answer-Refinement Modification: A refinement type system for algebraic effect handlers, Shonan Meeting No.203 (Effect Handlers and General-Purpose Languages), Aug. 2023.
[Talk] 大崎敦也, 牧野青希, 椎葉瑠星, 福田健介, 大越匡, 中澤仁, eBPFとXDPを用いた高速なDDoS攻撃検出・自動対処システムの提案と実装, 電子情報通信学会 IA研究会, Sep. 2023.
[Talk] 今井航一，石川裕，加藤真平, IoTにおけるTrusted Execution Environmentによるシステムコールのモニタリングとポリシー管理の設計, 情報処理学会研究報告 2023-OS-160, Aug. 2023.
[Talk] 稲葉皓信, 関山太朗, 五十嵐淳, 石川裕, Rabbit: a modeling language for verifying data-flow security, 情報処理学会研究報告 PRO, Aug. 2023.
[Talk] 竹房あつ子, 小野泰司, 石川裕, OP-TEEを用いたIoTにおける安全な階層鍵管理機構の検討, 情報処理学会研究報告 2023-OS-160, No. 11, pp. 1-12, Aug. 2023.
[Poster] 青木信雄, 竹房あつ子, 石川裕, 小野泰司, 坂根栄作, 合田憲人, ゼロトラストIoTに基づくIoT機器のOTAソフトウェア更新実現にむけて, cross-disciplinary workshop on computing Systems, Infrastructures, and programminG 2023 (xSIG2023), Aug. 2023.
[Poster] Society 5.0のためのゼロトラストIoT. NIIオープンハウスポスター, 2023年6月.

2022年度

[Poster] Sayako Shimizu, Eisaku Sakane, Takeshi Nishimura, Kento Aida, Atsuko Takefusa, Certification Mechanism to Assure Software Reliability with Digital Signature, International Symposium on Grids & Clouds (ISGC), Mar. 2023.
[Invited Talk] 竹房あつ子, 形式検証とシステムソフトウェアの協働によるゼロトラストIoT, 情報処理学会第85回全国大会イベント企画「Society 5.0時代の安心・安全・信頼を支える基盤ソフトウェア技術の構築」, 2023年3月.
[Talk] 川島佑介，松井俊浩, パスワード及びログの保存設定に着目したIoTデバイスにおけるファームウェアの安全性調査, 情報処理学会第100回コンピュータセキュリティ研究会CSEC, 2023年3月.
[Invited Talk] Atsuko Takefusa, Building System Software for Zero Trust IoT (ZT-IoT), Secure Device Forum 2023, Feb. 2023.
[Invited Talk] Atsushi Igarashi, (I Can’t Get No) Verification, ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications (SPLASH), Dec. 2022. Link
[Exhibition] Zero Trust based IoT Security, SC22 Exhibition Booth #4205, 2022年11月．PDF
[Talk] 松本悟、松井俊浩, Pub/Sub 通信を行うコネクテッド自動運転車の周囲で捕捉されるデジタル証拠収集機能の提案, コンピュータセキュリティシンポジウムCSS2022, 2022年10月.
[Invited Talk] 竹房あつ子, ゼロトラストIoT (ZT-IoT)に向けたシステムソフトウェアの研究, 電子情報通信学会ソサイエティ大会, BI-4-1, 2022年9月. Link
[Invited Talk] 松井俊浩, 小野泰司, 信頼の基点に基づくIoTデバイスの通信, 電子情報通信学会ソサイエティ大会, BI-4-2, 2022年9月. Link
[Talk] 石川裕, Yin Jie, 竹房あつ子, 松井俊浩, 小野泰司, 合田憲人, Pub/Sub通信モデルを用いたセキュリティ監視機構の検討, 情報処理学会研究報告, vol. 2022-OS-156, no. 2, pp. 1-6, 2022年7月. Link, Slide
[Poster] Society 5.0のためのゼロトラストIoT. NIIオープンハウスポスター, 2022年6月. PDF

2021年度

[Talk] 竹房あつ子, 五十嵐淳, 関山太郎, 松井俊浩, 小野泰司, 福田健介, 蓮尾一郎, 合田憲人, 石川裕, ZT-IoT: ゼロトラストIoTのためのシステムソフトウェア構築に向けて, 情報処理学会研究報告, vol. 2022-OS-154, no. 3, pp. 1-16, 2022年3月. Link, Slide
[Poster] 竹房あつ子, 五十嵐淳, 関山太郎, 松井俊浩, 小野泰司, 福田健介, 蓮尾一郎, 合田憲人, 石川裕, ZT-IoT: ゼロトラストIoTのためのシステムソフトウェアの検討, 情報処理学会第154回OS研究発表会, 2022年3月.
[Invited Talk] 竹房あつ子, 形式検証とシステムソフトウェアの協働によるゼロトラストIoT, CREST/さきがけセッション, ComSys 2021, 2021年12月.