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.

翻译：许多与安全性或并发性相关的属性必须编码为所谓的超属性，即允许对系统多条迹进行推理的时序属性。然而，尽管近年来超属性模型检测取得了进展，但仍缺乏高级规约语言来有效支持软件工程实践者在系统设计早期阶段验证此类属性。Alloy是一种轻量级形式化方法，其高级规约语言配备自动化分析程序，特别适用于早期开发阶段设计模型的验证。但该语言原生不支持超属性的验证。本文提出HyperPardinus——一种新的模型发现程序，它扩展了Pardinus（Alloy语言的时序逻辑后端），通过依赖现有的底层超属性模型检测器，自动验证关系模型上的超属性。在此基础上，本文保守地扩展Alloy，使其支持设计模型上超属性的规约与自动验证，以及更高抽象层级中（反）例的可视化。评估表明，我们的方法能够对包含交替量词的复杂超属性进行建模并发现（反）例，从而有效解决当前前沿研究中的相关场景。