AUTOMATED FIRMWARE VERIFICATION USING FIRMWARE-HARDWARE INTERACTION PATTERNS

Abstract

Firmware refers to low-level software that is tied to a specific hardware platform. For instance, low-level drivers that physically interface with the peripherals are an example of firmware.

An emerging trend in system design is to implement complex system management functions in firmware rather than hardware. For example, firmware has grown to include software that manages critical hardware platform functions such as power management. As the scale and the importance of firmware is increasing, its validation becomes a critical part of system validation.

Firmware validation relies on having good models of the interacting hardware components because firmware needs to be shipped with the hardware and shares many of the same critical design concerns as the hardware. This is generally addressed through co-simulating C/C++ based firmware code and HDL~(including SystemC) hardware models, which are usually not available until the late design stages.

However, co-simulation tends to be slow, and is further exacerbated by the large number of possible interleavings between the concurrent firmware and hardware threads. Typically, in co-simulation, the thread scheduler, such as the SystemC scheduler, only explores a small number of possible firmware-hardware interleavings and thus may miss critical bugs.

A firmware function is mostly reactive: it continuously provides a service, with a clear start and end, in response to inputs from its interacting software or hardware layer~(i.e., the environment). Thus, a firmware function is often inherently associated with an infinite loop structure. This often makes it impossible to guarantee the completeness of the verification results.

To this end, I address two key problems in this thesis. First, I describe how to co-design firmware with the system components at the service function level, also referred to as 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, this thesis first introduces a specific Service-Function Transaction-Level Model (TLM) for modeling firmware and interacting hardware components.

I capture the particular structure of the proposed TLMs through cross-transaction interaction patterns, such as statelessness, i.e., when variable values are not retained between transaction executions, or producer-consumer 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 test-equivalent to the target firmware transaction and can be used with a standard single-threaded concolic test generator. The tests generated can (i) be directly used for the firmware transaction and (ii) account for the multi-threaded interactions. 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 the previous interaction pattern-based sequentialization method to cover all common interaction patterns with the complete coverage. The resulting general sequentialization method enables the direct application of standard software bounded model checkers such as CBMC on this sequentialized program.

The practical aspects of our work are evaluated using real firmware benchmarks, e.g., the Rockbox mp3 player firmware code and Linux device driver code with its interacting QEMU hardware emulator code.

In summary, this thesis presents novel verification methodologies with new techniques for reducing the search space of concurrent and unbounded firmware systems and their interacting firmware/hardware transactions using common interaction patterns derived from the novel service function-based TLM proposed in this thesis. In doing so, it enables both scalability and completeness of verification whereas many other existing methodologies typically trade completeness for scalability, or vice versa. As the complexity and size of firmware continue to grow, the techniques developed in this thesis will provide the firmware designers a modeling framework for firmware systems that is more natural and close to the human thought process, and it will help firmware developers to have a complete but practical explanation of the behaviors of complicated concurrent and unbounded firmware systems.