Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction

Aruna Jayasena, Prabhat Mishra

TL;DR

The paper tackles the challenge of scalable hardware-firmware co-verification, where state-space explosion impedes formal guarantees. It introduces HIVE, an automated framework that generates formal models and system-level hints from the actual implementation by combining static analysis and concrete simulation, and then applies scenario-based decomposition to perform SMT-based proofs efficiently. The approach reduces state-space growth, enables scalable proofs, and can identify complex bugs in real firmware-hardware deployments, as demonstrated on four RISC-V-based SoCs. By removing the need for manual abstraction or hint engineering, HIVE provides a practical path to trustworthy, validated hardware-software systems.

Abstract

Hardware-firmware co-verification is critical to design trustworthy systems. While formal methods can provide verification guarantees, due to the complexity of firmware and hardware, it can lead to state space explosion. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. Manual development of abstraction or hints requires domain expertise and can be time-consuming and error-prone, leading to incorrect proofs or inaccurate results. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification. Our proposed approach is applicable to actual firmware and hardware implementations without requiring any manual intervention during formal model generation or hint extraction. To reduce the state space complexity, we utilize both static module-level analysis and dynamic execution of verification scenarios to automatically generate system-level hints. These hints guide the underlying solver to perform scalable equivalence checking using proofs. The extracted hints are validated against the implementation before using them in the proofs. Experimental evaluation on RISC-V based systems demonstrates that our proposed framework is scalable due to scenario-based decomposition and automated hint extraction. Moreover, our fully automated framework can identify complex bugs in actual firmware-hardware implementations.

HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction

TL;DR

The paper tackles the challenge of scalable hardware-firmware co-verification, where state-space explosion impedes formal guarantees. It introduces HIVE, an automated framework that generates formal models and system-level hints from the actual implementation by combining static analysis and concrete simulation, and then applies scenario-based decomposition to perform SMT-based proofs efficiently. The approach reduces state-space growth, enables scalable proofs, and can identify complex bugs in real firmware-hardware deployments, as demonstrated on four RISC-V-based SoCs. By removing the need for manual abstraction or hint engineering, HIVE provides a practical path to trustworthy, validated hardware-software systems.

Abstract

Hardware-firmware co-verification is critical to design trustworthy systems. While formal methods can provide verification guarantees, due to the complexity of firmware and hardware, it can lead to state space explosion. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. Manual development of abstraction or hints requires domain expertise and can be time-consuming and error-prone, leading to incorrect proofs or inaccurate results. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification. Our proposed approach is applicable to actual firmware and hardware implementations without requiring any manual intervention during formal model generation or hint extraction. To reduce the state space complexity, we utilize both static module-level analysis and dynamic execution of verification scenarios to automatically generate system-level hints. These hints guide the underlying solver to perform scalable equivalence checking using proofs. The extracted hints are validated against the implementation before using them in the proofs. Experimental evaluation on RISC-V based systems demonstrates that our proposed framework is scalable due to scenario-based decomposition and automated hint extraction. Moreover, our fully automated framework can identify complex bugs in actual firmware-hardware implementations.
Paper Structure (32 sections, 1 equation, 23 figures, 5 tables, 4 algorithms)

This paper contains 32 sections, 1 equation, 23 figures, 5 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. State-of-the-Art in State Space Reduction
  3. Abstraction
  4. Symmetry Reduction
  5. Partial-order Reduction
  6. Decomposition
  7. Research Contributions
  8. Background and Related Work
  9. Verification using Manual Abstraction
  10. Formal Verification using Manual Hints
  11. Firmware Validation using Concolic Testing
  12. HIVE: Automated and Scalable Hint-based Formal Verification
  13. Test Cases for Verification Scenarios
  14. Development of Specification
  15. Automated Generation of System Models
  16. ...and 17 more sections

Figures (23)

  • Figure 1: Existing formal firmware verification avenues
  • Figure 2: State space expansion of a state register of a hardware implementation with respect to the evaluated clock cycles.
  • Figure 3: Overview of our automated Hint-based Verification (HIVE) framework. Formal proofs are supported by hints.
  • Figure 4: HIVE utilizes both module-level and test scenario-based decomposition for improving the scalability of proofs.
  • Figure 5: Overview of HIVE framework that consists of five main steps: outlining test scenarios, system model construction, supporting artifact generation by static and dynamic analysis, hint generation, and equivalence checking.
  • ...and 18 more figures