论文标题
k-safety超越超前的软件验证
Software Verification of Hyperproperties Beyond k-Safety
论文作者
论文摘要
时间超构物是与多个执行轨迹相关的系统属性。对于（有限状态）硬件，通过模型检查算法支持时间超构，并且存在诸如HyperLTL之类的一般时间逻辑的工具。对于（Infinite）软件，到目前为止，对暂时性超腐烂的分析仅限于$ k $ - 安全性属性，即规定任何$ k $ trace之间没有不良交互的属性。在本文中，我们提出了一种自动化方法，用于验证$ \ forall^k \的存在^l $ - 安全性属性。 A $ \ forall^k \存在^l $ -SAFETY属性规定，对于任何$ k $ traces，存在$ l $ trace，以致于产生的$ k+l $ traces痕迹不会差异不佳。通用量化和存在性量化的这种组合使我们能够表达出$ k $ - 安全的许多属性，包括普遍的非干预或程序改进。我们的方法基于基于策略的存在痕量量化与程序降低的实例化，这是在固定的谓词抽象的背景下。值得注意的是，我们的框架可以相互依赖战略和减少。
Temporal hyperproperties are system properties that relate multiple execution traces. For (finite-state) hardware, temporal hyperproperties are supported by model checking algorithms, and tools for general temporal logics like HyperLTL exist. For (infinite-state) software, the analysis of temporal hyperproperties has, so far, been limited to $k$-safety properties, i.e., properties that stipulate the absence of a bad interaction between any $k$ traces. In this paper, we present an automated method for the verification of $\forall^k\exists^l$-safety properties in infinite-state systems. A $\forall^k\exists^l$-safety property stipulates that for any $k$ traces, there exist $l$ traces such that the resulting $k+l$ traces do not interact badly. This combination of universal and existential quantification enables us to express many properties beyond $k$-safety, including, for example, generalized non-interference or program refinement. Our method is based on a strategy-based instantiation of existential trace quantification combined with a program reduction, both in the context of a fixed predicate abstraction. Notably, our framework allows for mutual dependence of strategy and reduction.
