New tool extends Alloy formal method to verify complex security and concurrency properties

A research paper submitted to arXiv describes HyperPardinus, an extension that equips the Alloy formal verification language with the ability to check hyperproperties—a class of temporal properties essential for reasoning about security and concurrent systems.

The gap in existing tools#

Alloy is a lightweight formal method prized by software engineers for its high-level specification language and automated analysis capabilities, particularly during early design phases. Yet it has lacked native support for verifying hyperproperties, which require reasoning across multiple execution traces simultaneously—a critical need for security and concurrency verification.

How HyperPardinus works#

The new approach builds atop Pardinus, the temporal logic engine behind Alloy, by implementing a model-finding procedure that translates hyperproperty specifications into queries understood by existing low-level model checkers. This bridges the gap between Alloy's user-friendly abstraction and the specialized backends already designed for hyperproperty verification.

Practical impact#

By conservatively extending Alloy's syntax, HyperPardinus enables practitioners to specify and automatically verify hyperproperties directly within design models while presenting counterexamples and verification results at a high level of abstraction. The evaluation demonstrates the tool's capability to handle complex hyperproperties involving nested quantifiers, addressing real-world verification scenarios from recent research.