自动机软件模型检查超性质 (Automata-Based Software Model Checking of Hyperproperties)

We develop model checking algorithms for Temporal Stream Logic (TSL) and Hyper Temporal Stream Logic (HyperTSL) modulo theories. TSL extends Linear Temporal Logic (LTL) with memory cells, functions and predicates, making it a convenient and expressive logic to reason over software and other systems with infinite data domains. HyperTSL further extends TSL to the specification of hyperproperties - properties that relate multiple system executions. As such, HyperTSL can express information flow policies like noninterference in software systems. We augment HyperTSL with theories, resulting in HyperTSL(T),and build on methods from LTL software verification to obtain model checking algorithms for TSL and HyperTSL(T). This results in a sound but necessarily incomplete algorithm for specifications contained in the forall*exists* fragment of HyperTSL(T). Our approach constitutes the first software model checking algorithm for temporal hyperproperties with quantifier alternations that does not rely on a finite-state abstraction.

翻译：我们开发了针对模理论下的Temporal Stream Logic（TSL）和Hyper Temporal Stream Logic（HyperTSL）模型检查算法。TSL通过添加内存单元、函数和谓词来扩展线性时间逻辑（LTL），使其成为适用于具有无限数据域的软件和其他系统的方便且表达力强的逻辑。HyperTSL进一步扩展了TSL以指定关联多个系统执行的超属性——关于信息流策略，比如软件系统中的非干扰。因此，HyperTSL可以表达具有理论的超属性，从而得出了HyperTSL(T)，并借鉴了LTL软件验证的方法，以获得TSL和HyperTSL(T)的模型检查算法。这导致了对于在forall*exists*超TSL(T)片段中包含的规范的声音但必然不完整的算法。我们的方法构成了第一个针对量词交替的超性质的时间超属性的软件模型检查算法，而不依赖于有限状态抽象。