Model checking of hyperproperties for high-level relational models
For software engineering practitioners, it enables early-stage verification of hyperproperties in high-level design models, addressing a gap in existing formal methods.
This work extends Alloy to support specification and automatic verification of hyperproperties (e.g., security, concurrency) by proposing HyperPardinus, a model finding procedure that leverages existing low-level hyperproperty model checkers. Evaluation shows it can handle complex hyperproperties with alternating quantifiers, enabling verification of relevant scenarios.
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.