Completeness bounds and sequentialization for model checking of interacting firmware and hardware

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

An emerging trend in system design is to implement complex system management functions in firmware (FW). This changing design scenario requires support for verifying FW in the context of its hardware (HW) environment. As shown in previous work, there is value in a unified HW-FW model for driving the verification tasks. This model can help identify specific commonly-occurring interaction patterns between the HW and FW. These patterns enable pruning the verification search space as demonstrated in previous work in automating FW test generation using concolic testing. In this work, we introduce a bounded model checking (BMC)-based methodology for FW verification. Although BMC is effective for finding bugs by unrolling the underlying transition system up to some bound, it requires a completeness threshold on the bound to ensure complete verification. We show how commonly occurring FW code patterns can be exploited, using inexpensive static analysis techniques, to determine this completeness bound. Further, we show how this bound analysis, combined with the interaction patterns in the unified HW-FW model, is used to sequen-tialize the concurrent FW and HW code, i.e., to derive a sequential program that represents the parallel interaction of the FW and HW. This enables the direct application of standard software model checkers such as CBMC on this sequentialized program. We have automated this process by implementing: (i) a static completeness bound analyzer on top of the tool Frama-C, and (ii) a sequentializer to generate code for verification by the CBMC model checker. We evaluate the resulting tool using three real FW benchmarks, each consisting of a Linux device driver and its interacting QEMU-emulated HW code with multiple correctness properties. We successfully computed the BMC completeness bounds for 41 out of 46 properties and completed model checking for 12 out of 16 FW transactions.

Original languageEnglish (US)
Title of host publication2015 International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages202-211
Number of pages10
ISBN (Electronic)9781467383219
DOIs
StatePublished - Nov 17 2015
EventInternational Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2015 - Amsterdam, Netherlands
Duration: Oct 4 2015Oct 9 2015

Publication series

Name2015 International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2015

Other

OtherInternational Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2015
CountryNetherlands
CityAmsterdam
Period10/4/1510/9/15

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Software
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Completeness bounds and sequentialization for model checking of interacting firmware and hardware'. Together they form a unique fingerprint.

  • Cite this

    Ahn, S., Malik, S., & Gupta, A. (2015). Completeness bounds and sequentialization for model checking of interacting firmware and hardware. In 2015 International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2015 (pp. 202-211). [7331383] (2015 International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2015). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/CODESISSS.2015.7331383