Hyperproperties are system properties that relate multiple computation paths in a system and are commonly used to, e.g., define information-flow policies. In this paper, we study a novel class of hyperproperties that allow reasoning about strategic abilities in multi-agent systems. We introduce HyperATL*, an extension of computation tree logic with path variables and strategy quantifiers. Our logic supports quantification over paths in a system - as is possible in hyperlogics such as HyperCTL* - but resolves the paths based on the strategic choices of a coalition of agents. HyperATL* can express strategic hyperproperties, such as that the scheduler in a concurrent system has a strategy to avoid information leakage. This allows us to capture many previously studied (strategic) security notions in a unifying hyperlogic. Moreover, we show that HyperATL* is particularly useful for specifying asynchronous hyperproperties, i.e., hyperproperties where the execution speed on the different computation paths depends on the choices of a scheduler. We show that finite-state model checking of HyperATL* is decidable and present a model checking algorithm based on alternating automata. We establish that our algorithm is asymptotically optimal by proving matching lower bounds. We have implemented a prototype model checker for a fragment of HyperATL* that can check various security properties in small finite-state systems.
翻译:超能力是系统里与多重计算路径相关的系统属性, 通常用于定义信息流政策。 在本文中, 我们研究一种新型超能力类别, 能够对多试剂系统中的战略能力进行推理。 我们引入了超强ATL*, 这是计算树逻辑的延伸, 带有路径变量和战略量化符。 我们的逻辑支持在一个系统中对路径进行量化- 在超超超高CTL* 等超高逻辑中是可能的, 但根据代理人联盟的战略选择解决路径。 HyperATL* 能够表达战略超能力, 例如, 在同时系统里, 调度器有避免信息泄漏的战略。 这使我们能够在统一的超高分辨率系统中捕捉许多先前研究过( 战略) 的安全概念。 此外, 我们显示, 超强技术* 特别有助于在系统里指定不相近的超能力, 也就是超能力, 不同计算路径上的执行速度取决于一个调度器的选择。 我们显示, 定点状态模型检查超强超能力* 是一个避免信息泄漏的策略。 这让我们以最优的方式检查一个基于系统上的硬的硬性矩阵。