Symbolic Execution for Embedded Binaries
Embedded systems now sit at the center of automotive, IoT, and critical infrastructure, and the security burden has shifted from the surrounding network to the device itself. But testing embedded binaries is hard: complex conditional logic, architecture-specific quirks, and validation routines make conventional fuzzing struggle, while symbolic execution alone runs into path explosion and expensive constraint solving.
This talk presents a hybrid approach that flips the usual playbook. Instead of fuzzing first and calling in symbolic execution to break through hard branches (as in Driller or SAGE), I use trace-guided symbolic execution, built on angr, as the primary path discovery engine, then hand a comprehensive seed corpus to AFL++ for deep vulnerability hunting. Starting from minimal input, the tool captures execution traces, extracts and negates path constraints, and iteratively solves for new inputs until it's covered every discoverable path, before fuzzing even starts.
On a custom benchmark suite modeled on real embedded targets (ARM and RISC-V), this approach hits 3.6× better code coverage than traditional fuzzing and surfaces bugs buried deep in execution paths that random mutation alone never reaches.
I'll walk through the architecture, the trade-offs of "symbolic-first, fuzz-second," and what it took to make trace-based analysis practical on real hardware-adjacent firmware, plus what didn't work along the way.
This talk walks through the design and evaluation of a hybrid vulnerability-discovery pipeline for embedded firmware, developed as part of my M.Sc. thesis and refined during my time on NXP Semiconductors' Vulnerability Analysis Team.
Background: Most hybrid fuzzing systems (Driller, SAGE) use coverage-guided fuzzing as the primary driver and call in symbolic execution only to break through hard-to-reach branches. This talk covers the opposite approach, using trace-guided symbolic execution as the primary path discovery mechanism, then handing a comprehensive input corpus to AFL++ to focus purely on vulnerability discovery in the paths that matter.
Talk outline:
- The problem: why embedded binaries defeat conventional fuzzing, architecture-specific constraints, validation routines, path explosion in symbolic execution
- Architecture walkthrough: how execution traces (from real hardware or cycle-accurate emulation) guide symbolic analysis in angr, and how path constraints are extracted and negated to systematically generate new inputs
- Why symbolic-first beats fuzz-first here: eliminating coordination overhead, getting deterministic and independently verifiable path coverage
- Live look at the pipeline against a custom ARM/RISC-V benchmark suite: coverage results, and vulnerabilities found in deep paths that random mutation never reaches
- What didn't work: dead ends, tuning problems, and lessons for anyone building similar tooling
- Q&A
Audience takeaway: attendees will leave with a concrete mental model for combining symbolic execution and fuzzing on embedded targets, a sense of where trace-based analysis pays off versus where it doesn't, and pointers to the tools (angr, AFL++) and techniques needed to try this on their own targets.
Prior knowledge assumed: basic familiarity with fuzzing and reverse engineering concepts. No prior symbolic execution experience required.
Ahmed holds an M.Sc. in Computer Science (IT Security and Reliability) from the University of Passau, where his thesis focused on hybrid symbolic-execution-and-fuzzing techniques for embedded firmware. He worked on NXP Semiconductors' Vulnerability Analysis Team in Hamburg, developing concolic execution engines, AFL++-based fuzzing pipelines, and taint analysis tooling for ARM and RISC-V firmware, and is now focused on vulnerability research.