Model checking of hyperproperties for high-level relational models

技术摘要：高层关系模型的超性质模型检测

问题陈述
许多关键系统属性，特别是涉及安全（例如，非干扰、广义非干扰）和并发（例如，线性化）的属性，都是超性质。与仅针对单一执行进行推理的传统轨迹属性不同，超性质要求对多个执行轨迹之间的关系进行推理。尽管近期进展已产生针对 HyperLTL 等超逻辑的模型检测器，但这些工具通常运行在低级、机器可读的格式上（例如，SMV 片段、自动机）。这为软件工程从业者造成了显著差距：缺乏能够自然建模系统设计同时支持超性质自动验证的高级规范语言。现有工具通常要求用户手动将高级概念转换为低级状态机，或者提供难以解读的格式（例如，原始 QBF 输出）的反例。

方法论
作者提出了HyperPardinus，这是一种模型查找过程，扩展了Pardinus（Alloy 语言的时序逻辑后端）以支持对关系模型进行超性质的自动验证。该方法涉及一个两阶段流水线：

1. 高级建模与翻译（HyperPardinus）：

   • 作者对Alloy 6语言进行了最小化扩展，在签名（signatures）中添加了 trace 关键字。这使得签名能够表示执行轨迹，从而允许在单个规范中对多个轨迹进行量化。
   • HyperPardinus 形式化了超关系模型查找问题。它接收高级 Alloy 规范，并将其翻译为一组低级 SMV（符号模型验证器）状态机和一条 HyperLTL 公式。
   • 翻译算法将关系时序逻辑约束转换为前束范式，将轨迹量词与非超部分分离。它为每个量化轨迹生成 SMV 模型，并将超性质编码为这些模型上的 HyperLTL 公式。
   • 在翻译过程中应用了关键优化，包括量词组合（合并同一类型的连续量词以减少轨迹数量）、多重性约束利用（使用整数变量代替布尔编码以减少状态空间）以及对称性破缺。

2. 低级验证（HyperSMV）：

   • 生成的 SMV 模型和 HyperLTL 公式由HyperSMV处理，这是一个专为处理高级 Alloy 翻译的特定挑战而设计的新模型检测工具。
   • HyperSMV 支持两种后端：
     • 显式状态（Exp）： 将 SMV 模型转换为显式状态系统（非确定性 Büchi 自动机），并使用基于自动机的求解器（例如，AutoHyper, forklift, ROLL）。它包含用于压缩公式和双模拟归约的优化。
     • 符号式（Sym）： 使用展开技术将模型和公式转换为量化布尔公式（QBF），利用现成的 QBF 求解器（例如，Quabs, qute）。
   • HyperSMV 的一个关键特性是其回溯见证的能力。它将求解器输出（通常是低级轨迹或 QBF 赋值）翻译回可读的 SMV 轨迹，并最终翻译为由 Alloy Analyzer 可视化的高级关系实例。

主要贡献

• HyperPardinus： 首个针对一阶超逻辑的模型检测工具。它扩展了 Alloy 生态系统，支持使用灵活的轨迹量词交替来规范和自动验证超性质。
• HyperSMV： 一个健壮的 SMV 模型检测器，集成了显式状态和符号式的最先进求解器。它显著提高了所支持 SMV 模型的表达能力（处理声明式风格和整数变量）以及验证过程的可扩展性。
• Alloy 扩展： 对 Alloy 6 进行了最小化、向后兼容的扩展，允许用户以声明方式指定超性质，并在高级抽象层次上可视化反例。
• 评估： 使用多样化的基准测试进行了全面评估，包括会议管理系统（CMS）、机器人路径合成、变异测试以及并发数据结构（SNARK）的线性化。

结果
评估解决了关于可行性、可用性、优化有效性和性能的研究问题：

• 表达能力与可用性： 该方法成功地在高级 Alloy 中对复杂超性质（例如，线性化、非干扰）进行了建模。作者证明，Alloy 模型比其低级 SMV 对应物更具可读性和可维护性，后者通常需要大量脚本来生成。
• 反例可视化： 与提供原始 QBF 输出或低级 SMV 轨迹的现有工具不同，HyperPardinus 提供了最小化的高级关系反例，并在 Alloy Analyzer 中进行可视化。例如，在 SNARK 基准测试中，该工具识别出一个错误并提供了一个 9 状态的图形实例，而最先进工具则生成了 sprawling（杂乱无章）、不可读的轨迹。
• 优化影响： HyperPardinus 中的优化（量词组合、对称性破缺、多重性约束）对于显式状态后端的可行性至关重要。如果没有这些优化，许多模型（例如，CMS 变体、机器人示例）会超时或无法生成状态机。
• 性能：
  • 高级模型： HyperSMV 在高级 Alloy 模型上优于最先进工具（AutoHyper, HyperQB），通常能在几秒内解决它们，而其他工具则超时。
  • 低级模型： 当应用于标准 SMV 基准测试（翻译为 Alloy 再翻译回来）时，HyperSMV 表现出具有竞争力的性能，以相当或更好的效率复现了预期结果。
  • 符号式与显式： 符号式后端（Sym）在查找错误（发现反例）方面表现良好，但由于有界模型检测（BMC）语义的限制，对于全称属性往往得出不确定的结果。显式后端（Exp）在较小范围的穷举验证方面更为有效。

意义与主张
本文主张 HyperPardinus 弥合了高级软件设计与超性质验证之间的差距。通过允许从业者直接在高级关系语言（Alloy）中规范和验证超性质，该方法消除了手动翻译为低级格式的需求。作者断言，这使得超性质验证对更广泛的软件工程社区变得可及。

该工作对其范围持谦逊态度：它并不声称解决超逻辑中的所有可判定性问题，而是展示了一个实用的流水线，用于分析以前使用现有工具难以处理或无法使用的高级复杂模型。其意义在于可用性（高级规范和可视化）以及验证复杂场景（如带有交替量词的线性化）的可行性，这些场景以前仅限于低级、手动或演绎方法。作者指出，该方法依赖于标准格式，确保其将从低级模型检测器的未来改进中受益。