Model checking of hyperproperties for high-level relational models

TL;DR

This paper introduces HyperPardinus, an extension of Alloy, enabling automated verification of hyperproperties in relational models, thus supporting early-stage system design verification.

Contribution

It proposes HyperPardinus, a novel model finding procedure that extends Alloy to verify hyperproperties using existing low-level model checkers.

Findings

Enables modeling and verification of complex hyperproperties with alternating quantifiers.

Supports visualization of counterexamples at a higher abstraction level.

Feasible for addressing relevant scenarios from current research.

Abstract

Many properties related to security or concurrency must be encoded as so-called hyperproperties, temporal properties that allow reasoning about multiple traces of a system. However, despite recent advances on model checking hyperproperties, there is still a lack of higher-level specification languages that can effectively support software engineering practitioners in verifying properties of this class at early stages of system design. Alloy is a lightweight formal method with a high-level specification language that is supported by automated analysis procedures, making it particularly well-suited for the verification of design models at early development stages. It does not natively support, however, the verification of hyperproperties. This work proposes HyperPardinus, a new model finding procedure that extends Pardinus -- the temporal logic backend of the Alloy language -- to automatically verify hyperproperties over relational models by relying on existing low-level model checkers for hyperproperties. It then conservatively extends Alloy to support the specification and automatic verification of hyperproperties over design models, as well as the visualization of (counter-)examples at a higher-level of abstraction. Evaluation shows that our approach enables modeling and finding (counter-)examples for complex hyperproperties with alternating quantifiers, making it feasible to address relevant scenarios from the state of the art.