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，以支持在设计模型上对高阶属性的规约与自动验证，并在更高抽象层次上可视化（反）示例。评估表明，我们的方法能够为具有交替量词的复杂高阶属性建模并查找（反）示例，从而使其能够处理当前技术发展水平中的相关场景。