战略超能力时空逻辑 (A Temporal Logic for Strategic Hyperproperties)

Hyperproperties are commonly used in computer security to define information-flow policies and other requirements that reason about the relationship between multiple computations. In this paper, we study a novel class of hyperproperties where the individual computation paths are chosen by the strategic choices of a coalition of agents in a multi-agent system. We introduce HyperATL*, an extension of computation tree logic with path variables and strategy quantifiers. HyperATL* can express strategic hyperproperties, such as that the scheduler in a concurrent system has a strategy to avoid information leakage. HyperATL* is particularly useful to specify asynchronous hyperproperties, i.e., hyperproperties where the speed of the execution on the different computation paths depends on the choices of the scheduler. Unlike other recent logics for the specification of asynchronous hyperproperties, our logic is the first to admit decidable model checking for the full logic. We present a model checking algorithm for HyperATL* based on alternating word automata and show that our algorithm is asymptotically optimal by providing a matching lower bound. We have implemented a prototype model checker for a fragment of HyperATL*, able to check various security properties on small programs.

翻译：计算机安全中通常使用超偏异性来定义信息流政策和其他要求,这些要求可以解释多种计算之间的关系。在本文中,我们研究的是新型的超异性,其中个人计算路径是由多试系统中一个代理人联盟的战略选择选择所选择的。我们引入了HyperATL*,这是使用路径变量和战略量化符来计算树逻辑的延伸。超ATL* 能够表达战略超异性,例如,同时系统中的排程器有一个避免信息泄漏的战略。HyperATL* 特别有用,以具体说明非同步性超异性,即超异性,即,在不同的计算路径上执行速度取决于排程的选择。不同于最近关于无交替性超正异性规范的其他逻辑。我们首先可以承认对完全逻辑进行分解模式检查。我们根据交替单词自动数据为超超异性拉提供了一种模型检查算算法,并表明我们的算法通过提供匹配的较低尺寸超异性超异性超异性超异性通性,即提供一种匹配的低尺寸程序。我们已经对各种安全性模型进行了测试。我们对等的模型进行了测试。

相关内容