Firmware is lowlevel software that is tied to a specific hardware platform. As the scale and the importance of firmware is increasing, its validation becomes a critical part of system validation.
Firmware validation relies on the interacting hardware components because firmware needs to be shipped with the hardware. However, their cosimulation is exacerbated by the large number of possible interleavings between the concurrent firmware and hardware threads.
A firmware function is often inherently associated with an infinite loop structure: it continuously provides a finiteduration service in response to inputs from its interacting software/hardware layer. This often makes it impossible to guarantee complete verification results.
To this end, I address two key problems in this thesis. First, I describe how to codesign firmware with the system components at the transaction level. Second, I discuss how to validate firmware interactions with their connected hardware modules while pruning the verification search space and ensuring complete verification. To solve these problems, I first introduce a specific service function transactionlevel model (TLM) for modeling firmware and interacting hardware components. I capture the particular structure of the proposed TLMs through crosstransaction interaction patterns, such as statelessness or producerconsumer relationships. Using the TLM, this thesis presents a scalable firmware validation approach that is based on automatically generating a test set with the goal of complete path coverage for firmware. Instead of explicitly exploring all the interleavings of the concurrent transactions, this thesis exploits the interaction patterns to automatically generate a sequential program, which is testequivalent to the target firmware transaction and can be used with a standard singlethreaded concolic test generator. However, due to the infinite loop structure of the TLMs, the sufficient bound that guarantees the completeness of verification needs to be determined. This thesis provides inexpensive static bound analysis techniques using commonly occurring firmware code patterns. Further, the bound analysis is combined with our sequentialization method to cover all common interaction patterns completely. The practical aspects of our work are evaluated using real firmware benchmarks, e.g., the Rockbox mp3 player code and Linux device driver code with its interacting QEMU hardware emulator code.