Research Project / Detail View

Research project

Verifying and explaining trust: fuzzing, formal methods, and assurance cases

Across all three pillars, we develop techniques for checking whether a system actually deserves trust and for explaining why — fuzzing for concurrent software, formal verification, security analysis, and assurance cases.

Detail

Background

Embedded software keeps growing in size, and more and more of it runs many tasks concurrently. In such software, bugs that depend on timing appear only rarely and are hard to reproduce, which makes them difficult to find with conventional testing.

Detail

The challenge

Safety and security cannot be explained just by saying that testing found no problems. We need systematic ways to show on what grounds a system deserves to be trusted.

In short, there are two problems: how to find, efficiently, the bugs that appear only rarely — and how to justify, with evidence, the claim that what remains can be trusted.

Detail

Finding bugs: fuzzing and formal methods

We apply fuzzing — feeding programs many automatically generated inputs to uncover bugs — to concurrent programs and middleware. By also exploring the order in which threads run, our fuzzers can efficiently find concurrency bugs that rarely show up in normal testing.

Together with programming-language researchers, we also study formal methods: translating concurrent programs that use semaphores into logically constrained term rewrite systems, a mathematical model on which their properties can be verified rigorously.

Detail

Analyzing and assuring: security analysis and assurance cases

We study systematic ways to find weaknesses in systems, such as intrusion detection for in-vehicle networks (CAN) and security analysis based on HAZOP.

We also work on assurance cases — structured arguments that show why a system is safe or secure — and on combining them with quantitative evaluation.

Detail

Achievements so far

In fuzzing, applying coverage-based greybox fuzzing to middleware (IPSJ Journal, 2021) was selected as a specially selected paper and received the Zengo Award. The line has since evolved into Schfuzz, which explores thread schedules with feedback guidance (ENASE 2023), and race-directed fuzzing for more effective concurrency testing (WSSE 2024).

In formal methods, together with programming-language researchers we established a transformation from concurrent programs with semaphores into logically constrained term rewrite systems (Journal of Logical and Algebraic Methods in Programming, 2025).

In automotive security, results range from defenses such as the ID-hopping CAN mechanism IDH-CAN (IEEE Access, 2018) and the centralized authentication scheme CaCAN (2014) to graph-based intrusion detection for CAN networks (CCNC 2026). TZmCFI, an RTOS-aware control-flow integrity mechanism using TrustZone (International Journal of Parallel Programming, 2020), HAZOP-based security analysis (Springer, 2016), and a quantitative security assurance case for in-vehicle systems (2021) cover the range from analysis to assurance.

Detail

Relation to the three pillars

This theme runs across all three research pillars: embedded systems, IoT, and Systems of Systems. Whatever the scale of the target, the same question remains: how do we confirm, and explain, that what we built deserves trust?

Detail

Why this matters

Better verification means bugs that manual testing could not find are caught before shipping, reducing accidents and recalls.

Assurance cases then let developers explain, with evidence, why a system deserves to be trusted. Rather than relying on a developer's confidence alone, this gives users and society a common ground for trusting the systems around them.

Detail

Where we are heading

We want verification and assurance to stop being tools for a small circle of specialists and become part of everyday development, running as routinely as builds and tests.

Fuzzers and formal methods that run continuously, with their results accumulating into assurance cases that serve as a common language between developers, clients, and users — building the theory and the tools for that world is where this theme is heading.

Detail

Future directions and example topics

The targets of verification are expanding from concurrent programs to distributed systems and systems that include machine learning. Students' thesis topics are usually chosen from within these directions, through discussion.

More effective search strategies for fuzzing concurrent and distributed systems
Fuzzing environments combined with embedded-system simulators, independent of physical hardware
Extending verification based on logically constrained term rewrite systems to a wider class of concurrent programs
Practical evaluation of intrusion detection for in-vehicle networks, including dataset development
Safety design and assurance cases for systems that include machine-learning components

Getting started

Overview articles to read first

These overview articles, written in Japanese, are an easier entry point than the research papers below.

CASE Revolution and Cybersecurity in the Automotive Domain (in Japanese)
Yutaka Matsubara, Ryo Kurachi, Hiroaki Takada, IPSJ Magazine, Apr. 2020.

Software and projects for this theme

Open-source software and tools

DoS attack visualization tool for IoT devices

Projects and related sites

Related publications

Papers and articles related to this project

View all publications

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
Impact Evaluation of Window Parameters in Graph-Based Intrusion Detection Systems for CAN
Akari Sasaki, Ryo Kurachi, Yutaka Matsubara, Hiroaki Takada

IPSJ CSEC, Jan. 2026
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

Link
2025
Issue Analysis and Feature Augmentation for Graph-Based Intrusion Detection Systems for CAN
Akari Sasaki, Ryo Kurachi, Yutaka Matsubara, Hiroaki Takada

IPSJ CSEC, Oct. 2025
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

Link
2024
Detecting Concurrency Bugs with Feedback-guided Fuzzing
Hiromasa Ito, Yutaka Matsubara, Hiroaki Takada

IPSJ Journal, Vol.65, No.5, pp.927-941

Link
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
Performance Evaluation of a CAN Intrusion Detection Algorithm
Akari Sasaki, Ryo Kurachi, Yutaka Matsubara, Hiroaki Takada

DICOMO 2024, pp.205-214
2024
Adversarial Attacks by Shadow Insertion on Road Traffic Signs
Kohei Tomoto, Ryo Kurachi, Yutaka Matsubara, Hiroaki Takada

SCIS 2024

Link
2024
Signal-Based CAN IDS Using Hamming Distance and Evaluation on a Dataset
Akari Sasaki, Ryo Kurachi, Yutaka Matsubara, Hiroaki Takada

CSS 2024, Kobe
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

Link
2023
Fuzzing with an Embedded System Simulator
Masaya Motoda, Hiromasa Ito, Yutaka Matsubara, Hiroaki Takada

ETNET 2023, Tokunoshima

Link
2022
Design and Implementation of RTOS-Aware Control-Flow Integrity Mechanism for Microcontroller-Based Systems
Tomoaki Kawada, Shinya Honda, Yutaka Matsubara, Hiroaki Takada

Computer Software, Vol.39, No.2

Link
2022
Zengo Award for Coverage-based Greybox Fuzzing Applied to Middleware
Hiromasa Ito, Yutaka Matsubara, Hiroaki Takada

ASTER
2021
How to Test Middleware with Coverage-based Greybox Fuzzing
Hiromasa Ito, Yutaka Matsubara, Hiroaki Takada

IPSJ Journal, Vol.62, pp.877-890

Link
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

Link
2020
Tsunagaru! Kiso Gijutsu IoT Nyumon (Chapter 2: Security)
Harumi Watanabe, Makoto Imamura, Kenji Hisazumi (eds.)

Corona Publishing

Yutaka Matsubara authored Chapter 2.
2020
CASE Revolution and Cybersecurity in the Automotive Domain
Yutaka Matsubara, Ryo Kurachi, Hiroaki Takada

IPSJ Magazine, Vol.61, No.4, pp.338-343
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

Link
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

Link
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

Link
2020
Transformation from Programs with Mutual Exclusion into Logically Constrained Term Rewriting Systems
Misaki Kojima, Naoki Nishida, Yutaka Matsubara, Masahiko Sakai

IEICE Technical Report SS2019-46, Vol.119, No.451, pp.31-36, Naha
2020
Coverage-based Greybox Fuzzing for Middleware
Hiromasa Ito, Yutaka Matsubara, Hiroaki Takada

SCIS 2020, Kochi

Link
2020
Performance Evaluation of QUIC for Lightweight Secure Communication on IoT Devices
Taiga Komatsu, Yutaka Matsubara, Hiroaki Takada

SCIS 2020, Kochi
2020
Safety Design Concepts for Statistical Machine Learning Components toward Accordance with Functional Safety Standards
Akihisa Morikawa, Yutaka Matsubara

SEAMS Project

Link
2020
Selected Paper Award for Coverage-based Greybox Fuzzing Applied to Middleware
Hiromasa Ito, Yutaka Matsubara, Hiroaki Takada

IPSJ Journal, 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 Based CFI for Asynchronous Exceptions
Tomoaki Kawada, Shinya Honda, Yutaka Matsubara, Hiroaki Takada

SCIS 2019, Otsu
2018
Trends and Prospects in Safety and Security for Connected Cars and Society
Yutaka Matsubara, Ryo Kurachi, Hiroaki Takada

Jidosha Gijutsu, Vol.72, No.5, pp.87-93
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

Link
2018
Safety Analysis Examples in Compliance with ISO 26262 for TOPPERS/ATK2 Conforming to the AUTOSAR OS Specification
Morio Mori, Hideaki Sato, Akira Yamashita, Yutaka Matsubara, Hiroaki Takada

IPSJ Journal, Vol.59, No.2, pp.785-794
2018
FRAM/STPA: Hazard Analysis Method for FRAM Model
Yoshinari Toda, Yutaka Matsubara, Hiroaki Takada

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

Link
2018
Multitask CFI Using Arm TrustZone for Armv8-M
Tomoaki Kawada, Shinya Honda, Yutaka Matsubara, Hiroaki Takada

ESS 2018 Proceedings, Gero, pp.71-74

Link
2018
Performance Evaluation of TLS 1.3 for IoT Devices
Taiga Komatsu, Yutaka Matsubara, Hiroaki Takada

Computer Security Symposium 2018, Nagano, pp.569-576
2018
Symbolic Execution Environment for Finding Bugs in the lwIP Embedded Network Stack
Katsunori Aoki, Yutaka Matsubara, Hiroaki Takada

SCIS 2018, Niigata
2018
Multi-task CFI Using Arm TrustZone for Armv8-M
Tomoaki Kawada, Shinya Honda, Yutaka Matsubara, Hiroaki Takada

SWEST20, Gero
2017
Trends and Prospects in Automotive Safety and Security Toward Autonomous Driving
Yutaka Matsubara, Ryo Kurachi, Hiroaki Takada

IPSJ Magazine, Vol.58, No.11
2017
Automotive Security and IoT
Yutaka Matsubara

Kinou Zairyo, Jun. 2017 serial article
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

Link
2017
Portable DoS Test Tool for Embedded Systems
Keigo Nagara, Katsunori Aoki, Yutaka Matsubara, Hiroaki Takada

ESS 2017 WiP, Gero

Link
2017
Attack Performance Evaluation of Mirai Malware on Embedded Systems
Keigo Nagara, Yutaka Matsubara, Katsunori Aoki, Hiroaki Takada

IPSJ Research Report 2017-EMB-44 No.41, Okinawa, pp.1-6

Link
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 with ACM CCS, Dallas
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
Security and Safety of In-Vehicle Devices
Ryo Kurachi, Yutaka Matsubara, Hiroaki Takada

IPSJ Magazine, Vol.57, No.7
2016
CaCAN: Centralized Authentication System in CAN
Ryo Kurachi, Yutaka Matsubara, Hiroaki Takada, Hiroshi Ueda, Satoshi Horihata

IEICE Transactions, Vol.J99-A No.2, pp.118-130
2016
An Aiding Tool for HAZOP-based Analysis for Embedded Systems
Jingxuan Wei, Yutaka Matsubara, Hiroaki Takada

WOCS2 2016, Tokyo
2016
Safety Analysis Method for AUTOSAR OS Toward Functional Safety
Morio Mori, Hideaki Sato, Hirotaka Hirabayashi, Akira Yamashita, Yutaka Matsubara, Hiroaki Takada

ESS 2016, Tokyo

Link
2016
HAZOP-based Security Analysis for Embedded Systems
Jingxuan Wei, Yutaka Matsubara, Hiroaki Takada

WOCS2 2016, Tokyo
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
Verification Environment for a Data Stream Management System
Masaki Nakai, Yutaka Matsubara, Hiroaki Takada, Akihiro Yamaguchi

IPSJ Research Report 2015-SLDM-170 No.14, Amami Oshima, pp.1-6

Link
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

Link
2014
Research and Development of a Security-Oriented Software Platform for Next-Generation Vehicles and Service Robots
Koichi Goto, Hiroyuki Hattori, Ayumu Sugiyama, Hiroaki Hara, Hiroaki Takada, Yutaka Matsubara, Daichi Mizuguchi, Koichi Takahashi

WOCS2 2014, Tokyo
2013
Safety Measures for Software Faults in Embedded Systems
Yutaka Matsubara, Hiroaki Takada

Computer Software, Vol.30, No.1, pp.119-129
2013
Safety Analysis Method Based on Hierarchical State Transition Diagram for Embedded Systems
Zoohaye Kim, Yutaka Matsubara, Hiroaki Takada

IEICE Transactions, Vol.J96-A No.1, pp.34-48
2012
Safety Analysis Method Focusing on State Transition Diagrams
Zoohaye Kim, Yutaka Matsubara, Hiroaki Takada

IEICE Transactions, Vol.J95-A No.2, pp.198-209
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

Link
2012
Safety Analysis Method Based on Parallel State Transition Diagrams in Embedded Systems
Zoohaye Kim, Yutaka Matsubara, Hiroaki Takada

ESS 2012 Proceedings, Tokyo

Link
2012
Safety Analysis Method Based on Parallel State Transition Diagrams
Zoohaye Kim, Yutaka Matsubara, Hiroaki Takada

WOCS2 2012, Yokohama
2012
Safety Analysis Method Based on Hierarchical State Transition Diagrams
Joohae Kim, Yutaka Matsubara, Hiroaki Takada

ETNET 2012, Matsushima
2011
Safety Analysis Method Focusing on Hierarchical State Transition Diagrams
Zoohaye Kim, Yutaka Matsubara, Hiroaki Takada

WOCS2 2011, Yokohama
2011
Safety Requirements Analysis Method Focusing on State Transition Diagrams
Zoohaye Kim, Yutaka Matsubara, Hiroaki Takada

WOCS 2011, Tokyo
2011
Safety Analysis Method Focusing on Hierarchical State Transition Diagrams
Joohae Kim, Yutaka Matsubara, Hiroaki Takada

Nagoya University Science Forum for Young Women Researchers, Nagoya
2011
Safety Analysis Method Focusing on Hierarchical State Transition Diagrams
Joohae Kim, Yutaka Matsubara, Hiroaki Takada

SWEST13 Proceedings, Gifu
2010
Hierarchical Scheduling Algorithm with Task Start Delay for Time Protection
Yutaka Matsubara, Shinya Honda, Hiroaki Takada

IPSJ Research Report 2010-EMB-19, Kumamoto
2010
Case Study of Safety Functions in Small Embedded System Design
Joohae Kim, Yutaka Matsubara, Hiroaki Takada

Safety Engineering Symposium 2010, Tokyo
2010
Time-Protection Scheduling Algorithm Using Only Task Deadlines
Yutaka Matsubara, Shinya Honda, Hiroaki Takada

IPSJ Research Report 2010-EMB-15 No.8, Yokohama

Link
2010
A Case Study of Safety Requirements Analysis in Small Embedded System Design
Zoohaye Kim, Yutaka Matsubara, Hiroaki Takada

ISSC 2010, Minneapolis
2009
Case Study of Safety Requirements Analysis in Small Embedded System Design
Joohae Kim, Yutaka Matsubara, Hiroaki Takada

DSS 2009, Osaka

Related themes

Other main research projects

Trust in a single computer

Real-time performance assurance in high-performance embedded systems

We study how to keep mixed-criticality systems fast, predictable, and safe even when many applications share CPUs, memory, storage, and networks.

Open this project

Trust in connected devices

IoTxWeb3: lifecycle management and data sharing for Internet of Things (IoT) devices

We combine Internet of Things (IoT) devices with blockchain and smart contracts so that device permissions, data sharing, and lifecycle management can be handled in a transparent way.

Open this project

Trust in systems of systems

Modeling and assuring dependability of Systems of Systems

We study Systems of Systems (SoS — arrangements in which multiple independent systems cooperate to achieve an emergent purpose) as socio-technical systems in which autonomous actors interact, and we aim to establish engineering methods for designing their overall behavior.

Open this project