Embedded Software Engineering

How can analysis and assurance become practical for embedded software?

Four complementary lines of work meet at practical assurance. Understanding failure asks what goes wrong in real embedded software, through studies of packet validation and layering violations. Making code reachable asks how firmware can be analyzed away from its target hardware, through rehosting, LEMIX and bottom-up testing. Analyzing at scale asks whether useful analyses can become cheap enough to apply broadly, using CodeQL and OSS-Fuzz-Gen. Establishing guarantees asks whether verification can become an ordinary engineering step, through Unit Proofing, compositional bounded model checking and AutoSOUP.

Embedded software runs where failures are expensive, and in conditions that defeat the assumptions most analysis tools are built on: no operating system to speak of, hardware that the analysis cannot reach, and code that cannot simply be run in a test harness.

Our work has attacked that gap in stages. We studied defects in real embedded network stacks, built rehosting infrastructure so firmware can execute away from its target hardware, and applied static analysis at a scale where it finds hundreds of defects across many projects. A current thrust, Unit Proofing, asks whether component-level formal verification can be made cheap enough to use as an ordinary engineering step rather than a special occasion.

Understanding embedded failures

Embedded software runs where failures are expensive, under conditions that defeat the assumptions most analysis tools are built on. This work establishes what actually goes wrong, and why the usual techniques do not reach it.

• Systematically Detecting Packet Validation Vulnerabilities in Embedded Network Stacks
  ASE · 2023
  Found high-severity defects in the network stacks that low-resource devices depend on, and showed the defects were systematic enough to look for deliberately. The empirical start of the line.
• Towards Automated Identification of Layering Violations in Embedded Applications (WIP)
  LCTES · 2023
  Layered design is what makes embedded software portable, so violations of the layering are a defect class worth detecting automatically.

Making the code reachable

Analysis cannot begin until the software can be executed and inspected away from the hardware it was written for. Rehosting turns embedded applications into something ordinary tools can work on.

• Towards Rehosting Embedded Applications as Linux Applications
  DSN-Disrupt · 2023
  First statement of rehosting embedded applications as ordinary Linux programs, so dynamic analysis no longer waits on hardware emulation.
• LEMIX: Enabling Testing of Embedded Applications as Linux Applications
  SECURITY · 2025
  LEMIX made that rehosting practical: embedded applications become testable as Linux applications, removing the fidelity-versus-effort tradeoff earlier approaches were stuck with.
• Reactive Bottom-Up Testing
  arXiv · 2025
  Reactive bottom-up testing: reaching deep code by building tests upward from the units rather than driving from the top.

Analysis at ecosystem scale

Once analysis is affordable, the question becomes what it finds when pointed at many real projects rather than one.

• Usage and Effectiveness of Static Analysis in Open-Source Embedded Software: CodeQL Finds Hundreds of Defects
  ISSTA · 2025
  Applied static analysis across many open-source embedded projects and found hundreds of defects, showing that analysis at ecosystem scale is affordable and that projects were not already doing it.
• Lessons from Mitigating False Positives in Google's OSS-Fuzz-Gen
  FSE-Industry · 2026
  False positives are what make automated fuzz-driver generation unusable in practice; this reports what reducing them took inside Google's OSS-Fuzz-Gen.

From defect detection to guarantees

A found defect is weaker than a guaranteed absence. The current thrust asks whether component-level verification can be made cheap enough to use as an ordinary engineering step.

• A Unit Proofing Framework for Code-level Verification: A Research Agenda
  ICSE-NIER · 2025
  Sets out the Unit Proofing agenda: design-level verification does not expose implementation defects, so verification has to reach the code.
• Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
  ICSE · 2026
  Asked whether unit proofs work rather than assuming they do, and measured compositional bounded model checking for memory safety on real code.
• AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification
  AutoSOUP generates the proofs. Automating construction is what moves unit proofing from a technique that works to one a team can afford to use.

Funding and support

This work has been supported by:

• Rolls-Royce — Securing Software Implementations through System Fuzz Testing and Modular Formal Methods
• Qualcomm, Inc. — Qualcomm Innovation Fellowship
• OpenAI — Cybersecurity Grant Program — AutoUP: Automated Unit Proofing
• Rolls-Royce — Facilitating Effective Dynamic Analysis of Embedded Software
• Rolls-Royce — Dynamic Security Analysis of Embedded Software Systems
• Rolls-Royce — Dynamic Analysis of Embedded Firmware