Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

HyperQB: A Bounded Model Checker for Hyperproperties

Tzu-Han Hsu, Milad Rabizadeh, Kenneth Rogale, Fedor Filippov, Marco A. de Oliveira Batista, César Sánchez, Borzoo Bonakdarpour

TL;DR

HyperQB addresses the lack of practical tooling for hyperproperty verification by delivering a push-button bounded model checker for HyperLTL and A-HLTL that accepts NuSMV and Verilog inputs. Its end-to-end Rust implementation unifies models into a compact IR, unrolls traces to a bound $k$, and encodes the problem into SMT or QBF with loop-conditions to guarantee completeness for applicable fragments. Extensive empirical evaluation across HyperLTL and A-HLTL benchmarks, hardware-Verilog designs, and comparisons with AutoHyper demonstrate substantial performance gains and practical applicability to information-flow, linearizability, and hardware-security verification. The work enables rapid bug finding and witness generation, and points to future extensions including C-program support and API access for broader reuse in verification pipelines.

Abstract

We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.

HyperQB: A Bounded Model Checker for Hyperproperties

TL;DR

HyperQB addresses the lack of practical tooling for hyperproperty verification by delivering a push-button bounded model checker for HyperLTL and A-HLTL that accepts NuSMV and Verilog inputs. Its end-to-end Rust implementation unifies models into a compact IR, unrolls traces to a bound , and encodes the problem into SMT or QBF with loop-conditions to guarantee completeness for applicable fragments. Extensive empirical evaluation across HyperLTL and A-HLTL benchmarks, hardware-Verilog designs, and comparisons with AutoHyper demonstrate substantial performance gains and practical applicability to information-flow, linearizability, and hardware-security verification. The work enables rapid bug finding and witness generation, and points to future extensions including C-program support and API access for broader reuse in verification pipelines.

Abstract

We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.

Paper Structure

This paper contains 29 sections, 8 equations, 7 figures, 8 tables.

Table of Contents

  1. Introduction
  2. Key features.
  3. Overall architecture.
  4. Organization.
  5. Input/Output Features of HyperQB
  6. Modeling Languages
  7. Input Specification and Semantics
  8. Specification language.
  9. Bounded semantics.
  10. Loop conditions.
  11. User Interface, Tool Usage, and Output
  12. Tool interface and output.
  13. Command-line usage example.
  14. Graphical User Interface (GUI).
  15. Algorithmic Backbone and Implementation
  16. ...and 14 more sections

Figures (7)

  • Figure 1: The standalone and web-based GUI for HyperQB$^{\textsf{\small 2.0}}$ demonstrating counterexample generation on a NuSMV model.
  • Figure 2: Overall architecture of HyperQB$^{\textsf{\small 2.0}}$.
  • Figure 3: A NuSMV model with implicit leak from high to low.
  • Figure 4: Transition relation of \ref{['fig:nusmv-model']}.
  • Figure 5: Grammar of HyperLTL/A-HLTL input formulas (full grammar in \ref{['appendix:fullgrammar']}).
  • ...and 2 more figures