Formal methods and Fuzzing for security in Internet of Things, embedded systems, real-time operating systems, and general software

Research Areas: Cyber-Physical Systems

Principal Investigator: Jamie Davis

Embedded software makes the world go 'round. Static and dynamic analysis of embedded software is a necessary capability for high-assurance software engineering (e.g. IEC 61508, ISO 26262). These capabilities facilitate many security tasks, e.g., vulnerability detection and repair, and reverse engineering. This project evaluates the security of embedded software applications as well as the infrastructure on which they depend, such as embedded network stacks (lwIP etc.) and real-time operating systems (RTOSes like FreeRTOS). We are evaluating static analysis options and identifying shortcomings. We are performing vulnerability analysis to identify common weaknesses across vendors. We are working on automated rehosting to apply state-of-the-art dynamic analysis techniques (e.g. fuzzing) in a UNIX environment.

Personnel

Other PIs: Aravind Machiry (ECE)

Students: Paschal Amusuo (PhD student @ECE) Sid Muralee (PhD student @ECE) Ritvik Tanksalkar (PhD student @ECE)

Representative Publications

Towards Automated Identification of Layering Violations in Embedded Applications (WIP).
Shen, Davis, and Machiry.
Proceedings of the 24th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES) 2023.
“If security is required”: Engineering and Security Practices for Machine Learning-based IoT Devices.
Gopalakrishna, Anandayuvaraj, Detti, Bland, Rahaman, and Davis.
Proceedings of the 4th International Workshop on Software Engineering Research & Practices for the Internet of Things (SERP4IoT) 2022.
LEMIX: Enabling Testing of Embedded Applications as Linux Applications.
Tanksalkar, Muralee, Danduri, Amusuo, Bianchi, Davis, and Machiry.
Proceedings of the 34th USENIX Security Symposium (SECURITY) 2025.
Reactive Bottom-Up Testing.
Muralee, Cherupattamoolayil, Davis, Bianchi, and Machiry.
arXiv 2025
Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification.
Amusuo, Cochell, Le Lievre, Patil, Machiry, and Davis.
Proceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE) 2026.
ZTD-JAVA: Mitigating Software Supply Chain Vulnerabilities via Zero-Trust Dependencies.
Amusuo, Robinson, Singla, Peng, Machiry, Torres-Arias, Simon, and Davis.
Proceedings of the ACM/IEEE 47th International Conference on Software Engineering (ICSE) 2025.
A Unit Proofing Framework for Code-level Verification: A Research Agenda.
Amusuo, Patil, Cochell, Le Lievre, and Davis.
Proceedings of the 47th IEEE/ACM International Conference on Software Engineering - New Ideas and Emerging Results Track (ICSE-NIER) 2025.
Systematically Detecting Packet Validation Vulnerabilities in Embedded Network Stacks.
Amusuo, Méndez, Xu, Machiry, and Davis.
Proceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering (ASE’23) 2023.
Towards Rehosting Embedded Applications as Linux Applications.
Srinivasan, Tanksalkar, Amusuo, Davis, and Machiry.
Proceedings of the 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks — Disrupt track (DSN-Disrupt) 2023.
Usage and Effectiveness of Static Analysis in Open-Source Embedded Software: CodeQL Finds Hundreds of Defects.
Shen, Yuan, Pillai, Zhang, Davis, and Machiry.
arXiv 2024.
A Unified Taxonomy and Evaluation of IoT Security Guidelines.
Chen, Anandayuvaraj, Davis, and Rahaman.
arXiv 2023.
FalseCrashReducer: Mitigating False Positive Crashes in OSS-Fuzz-Gen Using Agentic AI.
Amusuo, Liu, Calvo, Metzman, Chang, and Davis.
arXiv 2025.

Keywords: analysis, CPS, cyber-physical systems, fuzzing, real-time operating systems, RTOS