超越k-安全的超属性软件验证

时序超属性是关联多条执行轨迹的系统属性。对于（有限状态）硬件，时序超属性已有模型检验算法支持，且存在面向HyperLTL等通用时序逻辑的工具。对于（无限状态）软件，时序超属性的分析迄今仅限于$k$-安全属性，即规定任意$k$条轨迹之间不存在不良交互的属性。本文提出一种用于验证无限状态系统中$\forall^k\exists^l$-安全属性的自动化方法。$\forall^k\exists^l$-安全属性规定：对于任意$k$条轨迹，存在$l$条轨迹，使得所得的$k+l$条轨迹不发生不良交互。这种全称与存在量词的结合使我们能够表达许多超越$k$-安全的属性，包括例如广义非干扰或程序精化。我们的方法基于策略式的存在轨迹量词实例化，并结合程序归约，二者均处于固定谓词抽象的背景下。值得注意的是，我们的框架允许策略与归约相互依赖。