Efficient Loop Conditions for Bounded Model Checking Hyperproperties

TL;DR

This paper develops advanced loop conditions for bounded model checking of HyperLTL, enabling the detection of infinite traces and completeness in security and concurrency policy verification.

Contribution

It introduces a complete automata-based method and simulation-based algorithms for HyperLTL BMC with loop conditions, improving over previous linear unrolling approaches.

Findings

Automata-based technique guarantees completeness with bounds on unrollings.

Simulation algorithms effectively exploit short loops for SAT query generation.

Empirical evaluation demonstrates practical effectiveness of the proposed methods.

Abstract

Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite structure and to ultimately obtain completeness, BMC incorporates loop conditions that revisit previously observed states. This paper focuses on developing loop conditions for BMC of HyperLTL- a temporal logic for hyperproperties that allows expressing important policies for security and consistency in concurrent systems, etc. Loop conditions for HyperLTL are more complicated than for LTL, as different traces may loop inconsistently in unrelated moments. Existing BMC approaches for HyperLTL only considered linear unrollings without any looping capability, which precludes both finding small infinite traces and obtaining a complete technique. We investigate loop conditions for HyperLTL BMC, where the HyperLTL formula can contain up to one quantifier alternation. We first present a general complete automata-based technique which is based on bounds of maximum unrollings. Then, we introduce alternative simulation-based algorithms that allow exploiting short loops effectively, generating SAT queries whose satisfiability guarantees the outcome of the original model checking problem. We also report empirical evaluation of the prototype implementation of our BMC techniques using Z3py.