在反应式系统中验证异步超属性

《Proceedings of the ACM on Programming Languages》：Verifying Asynchronous Hyperproperties in Reactive Systems

异步超LTL的博弈论模型检查方法及其完全性证明，提出新型博弈框架解决多轨迹异步比较问题，实现任意?*?*公式验证，构建有限状态决策机制，并完成原型验证与实验分析。

　　

摘要

超属性（Hyperproperties）是系统属性，它们关联多个执行轨迹，在指定信息流和安全策略时非常常见。像HyperLTL这样的逻辑通过显式量化执行轨迹来表达反应系统中的时间超属性，即那些能够推理无限执行过程中时间行为的超属性。这类逻辑的一个常见副作用是它们会同步比较被量化的轨迹。这限制了这些逻辑表达异步比较多个轨迹的属性的能力，例如Zdancewic和Myers的观察确定性、McLean的非推断性以及Stuttering细化。我们研究了一种异步HyperLTL（A-HLTL）的模型检测问题，这是一种可以表达跨时间步长比较多个轨迹的超属性的时间逻辑。除了对系统轨迹进行量化外，A-HLTL还对这些轨迹的“抖动”（stutterings）进行二次量化。因此，A-HLTL能够简洁地指定许多广泛使用的异步超属性。对A-HLTL进行模型检测需要找到合适的“抖动”，而到目前为止，这仅对非常有限的片段或终止系统是可行的。在本文中，我们提出了一种基于游戏的新方法，用于验证反应系统中的任意?^*?^* A-HLTL公式。在我们的方法中，我们将验证视为验证者和反驳者之间的游戏，他们通过控制底层轨迹和“抖动”的部分来相互挑战。验证者的获胜策略对应于存在量化的轨迹的具体证据以及存在量化的“抖动”的异步对齐。我们确定了一些片段，在这些片段上我们的基于游戏的解释是完备的，因此构成了一个有限状态决策过程。我们为有限状态系统实现了一个原型，并报告了令人鼓舞的实验结果。