Verifying Asynchronous Hyperproperties in Reactive Systems

Raven Beutner

doi:10.1145/3763130

2025-10-01

PRE

Raven Beutner *

Bernd Finkbeiner

DOI：10.1145/3763130

原文链接

原文求助

摘要

En 中文

超属性是系统属性，涉及多个执行轨迹，通常在指定信息流和安全策略时出现。像HyperLTL这样的逻辑利用对执行轨迹的显式量化来表达反应式系统中的时序超属性，即关于无限执行中时序行为的超属性。此类逻辑的一个常不期望的副作用是它们同步比较量化轨迹。这禁止了逻辑表达比较多个轨迹异步的属性，例如Zdancewic和Myers的观察确定性、McLean的非推断，或停顿精化。我们研究了异步HyperLTL（A-HLTL）的一个变体的模型检测问题，这是一种时序逻辑，可以表达跨时间步比较多个轨迹的超属性。除了对系统轨迹进行量化外，A-HLTL还具有对这些轨迹的停顿进行次级量化。因此，A-HLTL能够简洁地指定许多广泛使用的异步超属性。模型检测A-HLTL需要寻找合适的停顿，迄今为止，这仅对非常受限的片段或终止系统可行。在本文中，我们提出了一种新颖的基于博弈的方法，用于验证反应式系统中任意的全称∀与存在∃*A-HLTL公式。在我们的方法中，我们将验证视为验证者和反驳者之间进行的博弈，他们通过控制底层轨迹和停顿的部分来相互挑战。验证者的获胜策略对应于存在量化的轨迹的具体证据和存在量化的停顿的异步对齐。我们确定了使我们的基于博弈的解释完备的片段，从而构成一个有限状态决策过程。我们为有限状态系统贡献了一个原型实现，并报告了令人鼓舞的实验结果。

Keyword:

Temporal Logics

HyperLTL

Asynchronous HyperLTL

Model-Checking

Game-based Semantics

Observational Determinism

Refinement

Hyperliveness