Firmware Verification using Transaction-Level Modeling

The term firmware refers to software that is tied to a specific hardware platform, e.g., low-level drivers that physically interface with the peripherals. Recent trend is that the complicated hardware functionality is migrated into the firmware, thus the co-design of the firmware and hardware components and testing the co-design have been emphasized. To this end, we introduce a specific Service Function Transaction-Level Model (TLM) for modeling the firmware and interacting hardware components. A service function provides a service in response to a specific trigger. This model suits for firmware since the nature of it is reactive; the firmware performs particular operations in response to the software or hardware inputs. Moreover, we are exploiting structural information of the TLM and the interaction patterns of concurrent firmware and hardware transactions for efficient testing. The challenges in testing are that the explosive number of interleavings of concurrent systems and the possible infinite unrolling of the transaction execution. We show how single-threaded concolic testing can be used for path exploration of such a complicated system.