FTA 2026 – Preliminary Table of Contents

Verification of Protocol Compliance by Symbolic Execution
Xing-Hua Peng and Pai H. Chou
(National Tsing Hua University, Hsinchu, Taiwan)
This paper proposes symbolic execution as an efficient approach to bounded verification of communication-protocol compliance in embedded firmware. Such protocols are often validated empirically, but conventional test cases may fail to expose subtle instances of noncompliance. We present an approach that applies symbolic execution to optimized firmware binaries while modeling hardware side effects and asynchronous events using hardware models manually constructed from vendor documentation, without requiring exhaustive simulation. Experiments on real-world firmware libraries demonstrate that our approach can correctly verify compliant peripheral implementations and efficiently identify noncompliance in bit-banged implementations of the I²C protocol, while minimizing false positives.

Article Search Article: splashws26ftamain-p20-p (type: Full Paper (10 pages, including refs)) doi:10.1145/3842651.3843180

Firmware-Specific Security Guidelines
Tim Lewis
(Insyde Software, USA)
This paper presents the real-world firmware security review guidelines developed and refined at Insyde Software to address that challenge at scale - across 600+ firmware engineers organized in multiple teams. Rather than cataloguing every theoretical attack surface in UEFI firmware, these guidelines focus on the areas where vulnerabilities are most likely to arise in day-to-day development, and where compromise would have the highest impact.
The framework is organized around seven high-risk technology areas, each with specific, numbered review checklist items. The goal is to give en

Article Search Article: splashws26ftamain-p44-p (type: Extended Abstract (2 pages, including refs)) doi:10.1145/3842651.3843182

IAIA: Interrupt-Aware Index Analysis for SSD Firmware
Hyeongseo Yoo and Kwangkeun Yi
(Seoul National University, Republic of Korea; Samsung Electronics, Republic of Korea)
Interrupts make SSD (Solid State Drive) firmware hard to analyze because they can update shared state at nondeterministic points. An array index that looks safe in the main code may therefore become out of bounds after an interrupt handler runs. This paper presents IAIA, an interrupt-aware index analysis that reports OOB candidates whose values may be affected by interrupt handlers. IAIA defines interrupt-aware semantics and implements it as an abstract interpreter. The interpreter models handler effects, computes provenance information, and collects OOB candidates. Post-processing then traces the provenance of each candidate and reports a warning only when the trace reaches an interrupt handler. On the benchmark suite, IAIA reports the intended interrupt-related warnings and produces no warnings for fixed versions or non-handler OOB cases.

Article Search Article: splashws26ftamain-p50-p (type: Full Paper (10 pages, including refs)) doi:10.1145/3842651.3843183

Meeting NSA’s “Guidance for Managing UEFI Secure Boot”
Kevin Davis
(Insyde Software, USA)
In 2017, the NSA’s advice on UEFI Secure Boot was essentially the cybersecurity equivalent of “eat your vegetables and maybe lock the front door.” Today in 2026, we’ve realized the “front door” wasn’t just unlocked, adversaries have been tunneling under the house for years. With the rise of BlackLotus and PKfail, “Default Secure” has become a dangerous myth. This session reviews the NSA’s updated “Guidance for Managing UEFI Secure Boot,” explaining the critical shift from passive enablement to active, owner-managed sovereignty. We will dive into the five core pillars of the guidance. Using InsydeH2O® as our technical lens, we will cover the basics of the guidance and provide the information needed to ensure you can turn the guidance into actionable steps.

Article Search Article: splashws26ftamain-p52-p (type: Extended Abstract (2 pages, including refs)) doi:10.1145/3842651.3843184

From Silicon to Boot Code: Extending Automated Program Repair to Firmware-Layer Security Workarounds
Maisha Mastora and Dean Sullivan
(University of New Hampshire, USA)
Automated program repair (APR) research has been constrained to design time. Current techniques localize and fix bugs in Register- Transfer Level (RTL) or High Level Synthesis (HLS) designs before a chip reaches production. Once a hardware vulnerability surfaces post-silicon, the patch content must be manually generated. Exist- ing automation methods address patch deployment but not patch synthesis. Based on established pre-silicon APR methods, we study the feasibility of extending to this firmware layer a dictionary- guided, localize-synthesize-validate APR methodology originally developed for RTL repair. An automated commit-clustering miner surfaces recurring fix templates across the EDK II (UEFI) firmware repository’s full commit history without depending on previously known Common Vulnerabilities and Exposures (CVE) identifiers, recovering all three known CVE-fix campaigns and surfacing two additional candidate bug families. Grounding our detectors in real fix evidence, we build four independent localizers: missing specu- lation barriers in C (CVE-2017-5753, Spectre v1), missing bounds checks before array writes in C (decompression library CVE), miss- ing Return Stack Buffer (RSB)-stuffing macro calls in x86 assembly (CVE-2017-5715), and missing integer-overflow guards in Hand-Off Block (HOB) creation C code (surfaced by the miner itself). All four achieve 100% recall; precision ranges from 2.1–15.5% on the C families to 100% on the assembly and HOB families. We perform root-cause analysis for the C-family false positives mechanically, which attributes 77–90% to two intra-procedural causes, isolating the inter-procedural alias-analysis gap as a measured 15–20% rather than an estimate. A held-out test confirms Spectre v1 localization holds at 100% recall on unseen files; a fifth, independently built dictionary entry (CVE-2018-3630) shows the methodology extends to a new bug signature at low added cost; and a naive syntactic baseline recalls at most 14% where our targeted detector recalls 100%. We frame these results within a broader research agenda for a unified hardware-to-firmware correctness lifecycle

Article Search Article: splashws26ftamain-p56-p (type: Full Paper (NIER: 8 pages, including refs)) doi:10.1145/3842651.3843185

FTA 2026 – Preliminary Table of Contents

1st International Workshop on Firmware Testing and Analysis (FTA 2026)

Frontmatter

1st International Workshop on Firmware Testing and Analysis (FTA 2026) Papers

1st International Workshop on Firmware Testing and Analysis (FTA 2026)