Model checking of hyperproperties for high-level relational models

Technical Summary: Model Checking of Hyperproperties for High-Level Relational Models

Problem Statement
Many critical system properties, particularly those concerning security (e.g., non-interference, generalized non-interference) and concurrency (e.g., linearizability), are hyperproperties. Unlike traditional trace properties that reason about a single execution, hyperproperties require reasoning about relationships between multiple execution traces. While recent advances have produced model checkers for hyperlogics like HyperLTL, these tools typically operate on low-level, machine-readable formats (e.g., SMV fragments, automata). This creates a significant gap for software engineering practitioners: there is a lack of high-level specification languages that allow for the natural modeling of system designs while supporting the automatic verification of hyperproperties. Existing tools often require users to manually translate high-level concepts into low-level state machines or provide counter-examples in formats (e.g., raw QBF outputs) that are difficult to interpret.

Methodology
The authors propose HyperPardinus, a model finding procedure that extends Pardinus (the temporal logic backend of the Alloy language) to support the automatic verification of hyperproperties over relational models. The approach involves a two-phase pipeline:

1. High-Level Modeling and Translation (HyperPardinus):

   • The authors introduce a minimal extension to the Alloy 6 language, adding a trace keyword to signatures. This allows signatures to represent execution traces, enabling quantification over multiple traces within a single specification.
   • HyperPardinus formalizes the Hyper Relational Model Finding problem. It takes a high-level Alloy specification and translates it into a set of lower-level SMV (Symbolic Model Verifier) state machines and a HyperLTL formula.
   • The translation algorithm converts the relational temporal logic constraints into a prenex normal form, separating trace quantifiers from the non-hyper fragment. It generates SMV models for each quantified trace and encodes the hyperproperty as a HyperLTL formula over these models.
   • Key optimizations are applied during translation, including quantifier composition (merging sequential quantifiers of the same type to reduce the number of traces), multiplicity constraint exploitation (using integer variables instead of Boolean encodings to reduce state space), and symmetry breaking.

2. Low-Level Verification (HyperSMV):

   • The generated SMV models and HyperLTL formulas are processed by HyperSMV, a new model checking tool designed to handle the specific challenges of high-level Alloy translations.
   • HyperSMV supports two backends:
     • Explicit-State (Exp): Converts SMV models into explicit-state systems (Non-deterministic Büchi Automata) and uses automata-based solvers (e.g., AutoHyper, forklift, ROLL). It includes optimizations for compressing formulas and bisimulation reduction.
     • Symbolic (Sym): Converts models and formulas into Quantified Boolean Formulas (QBF) using unrolling techniques, leveraging off-the-shelf QBF solvers (e.g., Quabs, qute).
   • A critical feature of HyperSMV is its ability to backtrace witnesses. It translates solver outputs (which are often low-level traces or QBF assignments) back into readable SMV traces and, ultimately, into high-level relational instances visualized by the Alloy Analyzer.

Key Contributions

• HyperPardinus: The first model checking tool for a first-order hyperlogic. It extends the Alloy ecosystem to support the specification and automatic verification of hyperproperties with flexible trace quantifier alternations.
• HyperSMV: A robust SMV model checker that integrates with both explicit-state and symbolic state-of-the-art solvers. It significantly improves the expressiveness of supported SMV models (handling declarative styles and integer variables) and the scalability of the verification process.
• Alloy Extension: A minimal, backward-compatible extension to Alloy 6 that allows users to specify hyperproperties declaratively and visualize counter-examples at a high level of abstraction.
• Evaluation: A comprehensive evaluation using diverse benchmarks, including conference management systems (CMS), robotic path synthesis, mutation testing, and linearizability of concurrent data structures (SNARK).

Results
The evaluation addresses four research questions regarding feasibility, usability, optimization effectiveness, and performance:

• Expressiveness and Usability: The approach successfully models complex hyperproperties (e.g., linearizability, non-interference) in high-level Alloy. The authors demonstrate that Alloy models are significantly more readable and maintainable than their low-level SMV counterparts, which often require extensive scripting to generate.
• Counter-Example Visualization: Unlike existing tools that provide raw QBF outputs or low-level SMV traces, HyperPardinus provides minimal, high-level relational counter-examples visualized in the Alloy Analyzer. For instance, in the SNARK benchmark, the tool identified a bug and provided a 9-state graphical instance, whereas state-of-the-art tools produced sprawling, unreadable traces.
• Optimization Impact: The optimizations in HyperPardinus (quantifier composition, symmetry breaking, multiplicity constraints) were crucial for the feasibility of the explicit-state backend. Without them, many models (e.g., CMS variants, Robot examples) timed out or failed to generate state machines.
• Performance:
  • High-Level Models: HyperSMV outperformed state-of-the-art tools (AutoHyper, HyperQB) on high-level Alloy models, often solving them in seconds where others timed out.
  • Low-Level Models: When applied to standard SMV benchmarks (translated to Alloy and back), HyperSMV showed competitive performance, replicating expected outcomes with comparable or better efficiency.
  • Symbolic vs. Explicit: The symbolic backend (Sym) performed well for bug finding (finding counter-examples) but often yielded inconclusive results for universal properties due to the limitations of bounded model checking (BMC) semantics. The explicit backend (Exp) was more effective for exhaustive verification of smaller scopes.

Significance and Claims
The paper claims that HyperPardinus bridges the gap between high-level software design and hyperproperty verification. By allowing practitioners to specify and verify hyperproperties directly in a high-level relational language (Alloy), the approach eliminates the need for manual translation to low-level formats. The authors assert that this makes hyperproperty verification accessible to a wider software engineering community.

The work is modest about its scope: it does not claim to solve all decidability issues in hyperlogics but rather demonstrates a practical pipeline for analyzing complex, high-level models that were previously intractable or unusable with existing tools. The significance lies in the usability (high-level specification and visualization) and the feasibility of verifying complex scenarios (like linearizability with alternating quantifiers) that were previously restricted to low-level, manual, or deductive approaches. The authors note that the approach relies on standard formats, ensuring it will benefit from future improvements in low-level model checkers.