Static Application Security Testing (SAST) is a cornerstone of software assurance, enabling early bug detection at scale. In the embedded Linux world, where firmware, drivers, and user-space components often interact tightly, static analysis provides broad coverage but lacks runtime context. It is effective at flagging potential issues quickly, but it can struggle with accuracy and with reasoning about dynamic behavior, concurrency, and environment-dependent states.
Symbolic execution fills some of these gaps. By treating inputs symbolically and exploring multiple execution paths through constraint solving, symbolic execution can uncover subtle bugs such as use-after-free, array out-of-bounds, and stack overflows. It complements static analysis by providing deeper insight into program behavior, especially in scenarios where traditional SAST tools produce false positives or miss issues entirely.
This talk will cover:
1. How SAST works, including its strengths in scalability and early detection, and its inherent limitations in modeling runtime behavior.
2. Symbolic execution methodology, including symbolic inputs, constraint solving, and how it integrates with or augments existing workflows.
3. Practical tools and techniques, including S2E, Z3, and concolic approaches.
4. Key challenges such as path explosion in loops and recursion, modeling OS and hardware interactions, and computational overhead.
5. Mitigation strategies such as state merging, pruning, heuristic search strategies, and hybrid execution to improve scalability.
6. Real-world embedded examples where symbolic execution found issues missed by static tools.
Attendees will leave with a clear understanding of how symbolic execution can be applied effectively in embedded Linux environments, why it matters for complex systems, and how to integrate it into their own analysis workflows. Rather than replacing static analysis, symbolic execution strengthens it by revealing deeper execution behavior.
