研究プロジェクト

信頼を確かめ、説明する技術: ファジング・形式検証・保証ケース

3つの研究テーマに共通する土台として、作ったシステムが本当に信頼できるかを確かめ、その根拠を説明するための技術を研究しています。並行プログラムのファジング、形式手法による検証、セキュリティ分析、保証ケースなどが対象です。

詳細

背景

組込みシステムのソフトウェアは規模が大きくなり、多数の処理が並行して動くものが増えています。こうしたソフトウェアでは、タイミングに依存してまれにしか現れない不具合が生じやすく、従来のテストでは見つけにくいという問題があります。

詳細

課題

安全性やセキュリティは「テストで問題が出なかった」というだけでは十分に説明できません。どのような根拠でシステムを信頼してよいのかを、体系立てて示す方法が必要です。

つまり課題は2つあります。めったに現れない不具合をどう効率よく見つけるか。そして、残ったシステムを信頼してよいことを、どう根拠付けて示すか、です。

詳細

不具合を見つける: ファジングと形式手法

ファジング（プログラムに自動生成した入力を大量に与えて不具合を見つける手法）を並行プログラムやミドルウェアに適用しています。スレッドの実行順序まで探索の対象に含めることで、通常のテストではめったに現れない並行性バグを効率よく見つけ出します。

また、セマフォを使った並行プログラムを論理制約付き項書換え系という数学的なモデルに変換し、その性質を厳密に検証する形式手法の研究を、プログラミング言語分野の研究者と共同で進めています。

詳細

弱点を分析し、根拠を示す: セキュリティ分析と保証ケース

車載ネットワーク（CAN）への侵入検知や、HAZOP を応用したセキュリティ分析など、システムの弱点を体系的に洗い出す手法を研究しています。

さらに、システムが安全・セキュアであることの根拠を構造化して示す保証ケース（アシュアランスケース）と、その定量的な評価との組み合わせにも取り組んでいます。

詳細

これまでの成果

ファジングの系列では、ミドルウェアへの Coverage-based Greybox Fuzzing の適用（情報処理学会論文誌, 2021）が特選論文に選ばれ、善吾賞を受賞しました。その後、スレッドの実行順序をフィードバック付きで探索する Schfuzz（ENASE 2023）、データレースに狙いを定めた Race Directed Fuzzing（WSSE 2024）へと発展しています。

形式手法では、セマフォを使う並行プログラムを論理制約付き項書換え系に変換する手法を、プログラミング言語分野の研究者と共同で確立しました（Journal of Logical and Algebraic Methods in Programming, 2025）。

車載セキュリティでは、ID ホッピングで CAN を守る IDH-CAN（IEEE Access, 2018）や集中認証方式 CaCAN（2014）といった防御から、グラフベースの侵入検知（CCNC 2026）まで、攻撃の検知と防御の両面で成果を挙げてきました。RTOS と連携する制御フロー保全機構 TZmCFI（International Journal of Parallel Programming, 2020）、HAZOP を応用したセキュリティ分析（Springer, 2016）、車載システムの定量的セキュリティ保証ケース（2021）など、分析から保証までを一貫して扱っています。

詳細

3つの研究テーマとの関係

このテーマは、組込みシステム、IoT、System of Systems という3つの研究テーマすべてに関わる横断的な技術です。対象のスケールが変わっても、「作ったものの信頼をどう確かめ、どう説明するか」という問いは共通しています。

詳細

この研究のうれしさ

検証の技術が進むと、人手のテストでは見つけられなかった不具合を出荷前に発見でき、製品の事故やリコールを減らせます。

さらに保証ケースを使えば、「なぜ安全だと言えるのか」を根拠付きで説明できます。開発者の自信だけに頼らず、利用者や社会がシステムを信頼するための共通の土台を作ることが、このテーマの目標です。

詳細

目指す姿

検証・保証の技術を、一部の専門家の道具から、ビルドやテストと同じように日常の開発に組み込まれる存在に変えることを目指しています。

ファジングや形式手法が自動で回り続け、その結果が保証ケースとして積み上がり、開発者・発注者・利用者の間の共通言語になる。そのための理論と道具立てを整えていきます。

詳細

今後の方向性とテーマの例

検証の対象は、並行プログラムから分散システム、機械学習を含むシステムへと広がっています。学生の研究テーマも、次のような方向性のなかから相談して決めていきます。

並行・分散システムを対象にしたファジングの探索戦略の高度化
組込みシステムシミュレータと組み合わせた、実機に依存しないファジング環境
論理制約付き項書換え系に基づく並行プログラム検証の適用範囲の拡大
車載ネットワーク侵入検知の実用性能評価とデータセットの整備
機械学習コンポーネントを含むシステムの安全設計と保証ケース

初めて学ぶ人へ

まず読むならこの解説

専門の論文より先に、日本語で書かれた次の解説から入るのがおすすめです。

自動車分野のCASE革命とサイバーセキュリティ
松原豊, 倉地亮, 高田広章, 情報処理, 2020年4月号.

このテーマの公開ソフトウェア・プロジェクト

公開ソフトウェア・ツール

IoT 機器向け DoS 攻撃可視化ツール

プロジェクト・関連サイト

このテーマに関連する論文・記事

論文・発表の一覧を見る

2026
Outlier-Ratio Feature Augmentation for Graph-based Intrusion Detection in CAN Networks
Akari Sasaki, Ryo Kurachi, Yutaka Matsubara, Hiroaki Takada

IEEE Consumer Communications & Networking Conference (CCNC 2026), Las Vegas, Jan. 2026
2026
CAN向けグラフベース侵入検知システムにおけるウィンドウパラメータの影響評価
佐々木あかり, 倉地亮, 松原豊, 高田広章

情報処理学会 CSEC研究会, 2026年1月
2025
Transforming Concurrent Programs with Semaphores into Logically Constrained Term Rewrite Systems
Misaki Kojima, Naoki Nishida, Yutaka Matsubara

Journal of Logical and Algebraic Methods in Programming, Vol.143, pp.1-23

リンク
2025
CAN向けグラフベース侵入検知システムの課題分析と特徴量拡張
佐々木あかり, 倉地亮, 松原豊, 高田広章

情報処理学会 CSEC研究会, 2025年10月
2024
Multilingual Investigation of Cross-Project Code Clones in Open-Source Software for Internet of Things Systems
Wenqing Zhu, Norihiro Yoshida, Yutaka Matsubara, Hiroaki Takada

IEEE Access, Vol.12, pp.179104-179118

リンク
2024
Feedback-guided Fuzzingによる並行バグ探索
伊藤弘将, 松原豊, 高田広章

情報処理学会論文誌, Vol.65, No.5, pp.927-941, May 2024

リンク
2024
Race Directed Fuzzing for More Effective Concurrency Testing
Hiromasa Ito, Yutaka Matsubara, Hiroaki Takada

The 6th International Workshop on Software Science and Engineering (WSSE 2024), Kyoto, Aug 2024
2024
CAN侵入検知アルゴリズムの性能評価
佐々木あかり, 倉地亮, 松原豊, 高田広章

分散、協調とモバイル(DICOMO2024)シンポジウム, pp.205-214, 岩手県花巻市, Jun 2024
2024
道路交通標識を対象とした影挿入による敵対的攻撃
戸本航平, 倉地亮, 松原豊, 高田広章

暗号と情報セキュリティシンポジウム(SCIS2024), Jan 2024

リンク
2024
ハミング距離を用いたシグナルベースCANIDSの提案とデータセットでの検証
佐々木あかり, 倉地亮, 松原豊, 高田広章

コンピュータセキュリティシンポジウム（CSS）2024, 兵庫県神戸市神戸国際会議場, Oct 2024
2023
Schfuzz: Detecting Concurrency Bugs with Feedback-Guided Fuzzing
Hiromasa Ito, Yutaka Matsubara, Hiroaki Takada

18th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2023), Prague, pp.273-282, Apr 2023

リンク
2023
組込みシステムシミュレータを用いたファジング
元田匡哉, 伊藤弘将, 松原豊, 高田広章

第62回組込みシステム合同研究発表会(ETNET2023)

リンク
2022
マイコン向けRTOS対応Control-Flow Integrity機構の設計と実装
河田智明, 本田晋也, 松原豊, 高田広章

コンピュータソフトウェア, Vol.39, No.2, May 2022

リンク
2022
善吾賞「ミドルウェアに対するCoverage-based Greybox Fuzzingの適用」
伊藤弘将, 松原豊, 高田広章

NPO法人ソフトウェアテスト技術振興協会（ASTER）
2021
ミドルウェアに対するCoverage-based Greybox Fuzzingの適用
伊藤弘将, 松原豊, 高田広章

情報処理学会論文誌, Vol.62, No.3, pp.877-890, Mar 2021

リンク
2021
Quantitative Security Assurance Case for In-vehicle Embedded Systems
Zhengshu Zhou, Yutaka Matsubara, Hiroaki Takada

CyberSciTech/PICom/DASC/CDBCom 2021, pp.43-50, Oct 2021

リンク
2020
つながる！基礎技術 IoT入門（第2章セキュリティ）
渡辺晴美, 今村誠, 久住憲嗣(編著)

コロナ社

第2章「セキュリティ」を松原豊が執筆。
2020
自動車分野のCASE革命とサイバーセキュリティ
松原豊, 倉地亮, 高田広章

情報処理 2020年4月号特集新たなモビリティ時代のサイバーセキュリティ, Vol.61, No.4, pp.338-343, Mar 2020
2020
TZmCFI: RTOS-Aware Control-Flow Integrity Using TrustZone for Armv8-M
Tomoaki Kawada, Shinya Honda, Yutaka Matsubara, Hiroaki Takada

International Journal of Parallel Programming, Vol.49, pp.136-150

リンク
2020
Agile Software Design Verification and Validation (V&V) for Automated Driving
Yixiao Li, Yutaka Matsubara, Daniel Olbrys, Kazuhiro Kajio, Hiroaki Takada

Proceedings of FISITA 2020, Oct 2020

リンク
2020
Transforming Concurrent Programs with Semaphores into Logically Constrained Term Rewrite Systems
Misaki Kojima, Naoki Nishida, Yutaka Matsubara

Informal Proceedings of WPTE 2020, Jun 2020

リンク
2020
排他制御を用いたプログラムから論理制約付き項書換え系への変換
小嶋美咲, 西田直樹, 松原豊, 酒井正彦

情報処理学会第56回組込みシステム研究発表会
2020
ミドルウェアに対するCoverage-based Greybox Fuzzing
伊藤弘将, 松原豊, 高田広章

第54回EMB合同研究発表会（ETNET2020）

リンク
2020
IoT機器の軽量セキュア通信におけるQUICの性能評価
小松大河, 松原豊, 高田広章

第54回EMB合同研究発表会（ETNET2020）
2020
Safety Design Concepts for Statistical Machine Learning Components toward Accordance with Functional Safety Standards
Akihisa Morikawa, Yutaka Matsubara

SEAMS Project

リンク
2020
特選論文「ミドルウェアに対するCoverage-based Greybox Fuzzingの適用」
伊藤弘将, 松原豊, 高田広章

情報処理学会論文誌, Vol.62, No.3
2019
Shadow Exception Stacks: Control-Flow Integrity for Asynchronous Exceptions Using TrustZone for Armv8-M
Tomoaki Kawada, Shinya Honda, Yutaka Matsubara, Hiroaki Takada

IESS 2019, LNCS Vol.11937, pp.56-71, Friedrichshafen, Nov 2019
2019
Shadow Exception Stacks: 非同期例外に対するTrustZone-MベースCFI
河田智明, 本田晋也, 松原豊, 高田広章

第51回組込みシステム合同研究発表会（ETNET2019）
2018
つながる社会とクルマのセーフティ＆セキュリティの動向と展望
松原豊, 倉地亮, 高田広章

自動車技術 2018年5月号特集：コネクティビティ：つながる社会とクルマ, Vol.72, No.5, pp.87-93, May 2018
2018
IDH-CAN: A Hardware-Based ID Hopping CAN Mechanism With Enhanced Security for Automotive Real-Time Applications
Wufei Wu, Ryo Kurachi, Gang Zeng, Yutaka Matsubara, Hiroaki Takada, Renfa Li, Keqin Li

IEEE Access, Vol.6, pp.54607-54623

リンク
2018
AUTOSAR OS仕様準拠TOPPERS/ATK2を対象とした機能安全規格ISO 26262対応における安全分析事例
毛利守男, 佐藤秀昭, 山下映, 松原豊, 高田広章

情報処理学会論文誌, Vol.59, No.2, pp.785-794, Feb 2018
2018
FRAM/STPA: Hazard Analysis Method for FRAM Model
Yoshinari Toda, Yutaka Matsubara, Hiroaki Takada

FRAMily 2018, pp.1-17, Cardiff, Jun 2018

リンク
2018
Arm TrustZone for Armv8-M を利用したマルチタスク対応 CFI の検討
河田智明, 本田晋也, 松原豊, 高田広章

組込みシステムシンポジウム2018論文集, pp.71-74, 下呂, Aug 2018

リンク
2018
IoTデバイスのためのTLS 1.3の性能評価
小松大河, 松原豊, 高田広章

第51回組込みシステム合同研究発表会（ETNET2019）
2018
組込みネットワークスタック lwIPのバグ発見のためのシンボリック実行環境
青木克憲, 松原豊, 高田広章

第47回組込みシステム合同研究発表会（ETNET2018）
2018
Arm TrustZone for Armv8-M を利用したマルチタスク対応 CFI
河田智明, 本田晋也, 松原豊, 高田広章

第20回組込みシステム技術に関するサマーワークショップ (SWEST20), 下呂市, Aug 2018
2017
自動車分野のセーフティとセキュリティの動向と展望 -自律走行の実現に向けて-
松原豊, 倉地亮, 高田広章

情報処理 2017年11月号特集 IoT時代のセーフティとセキュリティ -日本の産業競争力の強化に向けて-, Vol.58, No.11, Oct 2017
2017
自動車セキュリティの現状とIoT
松原豊

機能材料 2017年6月号連載 IoT時代のセキュリティ対策-繋がる時代に求められる安心・安全-, シーエムシー出版, 2017
2017
IDHCC: A Security-Enhanced ID Hopping CAN Controller Design to Guarantee Real-Time
Wufei Wu, Ryo Kurachi, Gang Zeng, Yutaka Matsubara, Hiroaki Takada, Renfa Li

CERTS 2017, pp.14-21, Jun 2017

リンク
2017
組込みシステム向けのポータブルDoSテストツール
長柄啓悟, 青木克憲, 松原豊, 高田広章

組込みシステムシンポジウム（ESS2017）WiP, 下呂, Aug 2017

リンク
2017
Miraiマルウェアの組込みシステムに対する攻撃性能評価
長柄啓悟, 松原豊, 青木克憲, 高田広章

第46回組込みシステム合同研究発表会

リンク
2017
Open-source software-based portable DoS test tool for IoT devices
Keigo Nagara, Katsunori Aoki, Yutaka Matsubara, Hiroaki Takada

Workshop on Internet of Things Security and Privacy Collocated with ACM CCS, Dallas, Nov 2017
2016
HAZOP-Based Security Analysis for Embedded Systems: Case Study of Open Source Immobilizer Protocol Stack
Jingxuan Wei, Yutaka Matsubara, Hiroaki Takada

Recent Advances in Systems Safety and Security, Springer, pp.79-96
2016
車載機器のセキュリティと安全性
倉地亮, 松原豊, 高田広章

情報処理 2016年7月号小特集乗り物の情報セキュリティと安全性, Vol.57, No.7, Jun 2016
2016
メッセージ認証を用いたCANの集中監視システム
倉地亮, 松原豊, 高田広章, 上田浩史, 堀端啓史

電子情報通信学会論文誌, Vol.J99-A, No.2, pp.118-130, Feb 2016
2016
An Aiding Tool for HAZOP-based Analysis for Embedded Systems
魏景軒, 松原豊, 高田広章

第14回クリティカルソフトウェアワークショップ（WOCS2）, 東京, Dec 2016
2016
機能安全対応に向けたAUTOSAR OSの安全分析手法
毛利守男, 佐藤秀昭, 平林寛崇, 山下映, 松原豊, 高田広章

組込みシステムシンポジウム（ESS2016）, 東京, Oct 2016

リンク
2016
HAZOP-based Security Analysis for Embedded Systems
魏景軒, 松原豊, 高田広章

第13回クリティカルソフトウェアワークショップ（WOCS2）, 東京, Jan 2016
2015
HAZOP-based Security Analysis for Embedded Systems: Case Study of Open Source Immobilizer Protocol Stack
Jingxuan Wei, Yutaka Matsubara, Hiroaki Takada

Proceedings of the 3rd International Workshop on Systems Safety & Security (IWSSS2015), Bucharest, Jun 2015
2015
データストリーム管理システムの検証環境
中井将貴, 松原豊, 高田広章, 山口晃広

第44回組込みシステム合同研究発表会（ETNET2016）

リンク
2014
CaCAN - Centralized Authentication System in CAN
Ryo Kurachi, Yutaka Matsubara, Hiroaki Takada, Naoki Adachi, Yukihiro Miyashita, Satoshi Horihata

Proceedings of the escar 2014 Europe, pp. 1-9, Hamburg, Nov 2014

リンク
2014
次世代自動車向けセキュリティ対応ソフトウェアプラットフォームの研究開発
後藤孝一, 服部博行, 杉山歩, 原浩晃, 高田広章, 松原豊, 水口大知, 高橋孝一

組込みシステムシンポジウム（ESS2014）, 東京, Oct 2014
2013
組込みシステムにおけるソフトウェア障害の安全対策
松原豊, 高田広章

コンピュータソフトウェア, Vol.30, No.1, pp.119-129, Jan 2013
2013
組込みシステムにおける階層型状態遷移図に基づく安全分析手法
金周慧, 松原豊, 高田広章

電子情報通信学会論文誌, Vol.J96-A, No.1, pp.34-48, Jan 2013
2012
状態遷移図に着目した安全分析手法
金周慧, 松原豊, 高田広章

電子情報通信学会論文誌, Vol.J95-A, No.2, pp.198-209, Feb 2012
2012
Safety Analysis Method Based on Parallel State Transition Diagram for Embedded Systems
Zoohaye Kim, Yutaka Matsubara, Hiroaki Takada

SEA 2012, pp.417-425, Las Vegas, Nov 2012

リンク
2012
並列状態遷移図を用いた組込みシステム向け安全性分析手法
金周慧, 松原豊, 高田広章

組込みシステムシンポジウム（ESS2012）論文集, 東京, Oct 2012

リンク
2012
組込みシステムにおける並列状態遷移図に基づく安全分析手法
金周慧, 松原豊, 高田広章

組込みシステムシンポジウム（ESS2012）
2012
階層型状態遷移図を基にした安全性分析手法
金周慧, 松原豊, 高田広章

第30回EMB合同研究発表会, 鳥取, Mar 2012
2011
階層型状態遷移図を基にした安全性分析手法
金周慧, 松原豊, 高田広章

第12回組込みシステム技術に関するサマーワークショップ(SWEST12), 浜松, Sep 2011
2011
状態遷移図に注目した安全要求分析手法
金周慧, 松原豊, 高田広章

第8回クリティカルソフトウェアワークショップ（WOCS2011）
2011
階層型状態遷移図を基にした安全性分析手法
金周慧, 松原豊, 高田広章

第13回組込みシステム技術に関するサマーワークショップ(SWEST13), 下呂, Sep 2011
2011
小規模組込みシステム設計における安全性要求分析事例
金周慧, 松原豊, 高田広章

第12回組込みシステム技術に関するサマーワークショップ(SWEST12), 浜松, Sep 2010
2010
組込みシステムにおけるソフトウェア障害の安全対策 -OSレベルの安全メカニズムの検討-
松原豊, 本田晋也, 高田広章

組込みシステム技術に関するサマーワークショップ(SWEST12)
2010
小規模組込みシステムの設計における安全機能の事例調査
金周慧, 松原豊, 高田広章

Safety Engineering Symposium 2010, Tokyo
2010
組込みシステムにおけるソフトウェア障害の安全対策 -OSレベルの安全メカニズムの検討-
松原豊, 本田晋也, 高田広章

組込みシステム技術に関するサマーワークショップ(SWEST12)

リンク
2010
小規模組込みシステム設計における安全性要求分析事例
金周慧, 松原豊, 高田広章

第12回組込みシステム技術に関するサマーワークショップ(SWEST12), 浜松, Sep 2010
2009
小規模組込みシステム設計の安全要求分析の事例調査
金周慧, 松原豊, 高田広章

組込みシステム技術に関するサマーワークショップ(SWEST11)