Monitoring hyperproperties
Monitoring hyperproperties
复制标题
DOI：
10.1007/s10703-019-00334-z
复制
发表时间：
2019-11-01
影响因子：
0.8
通讯作者：
Tentrup, Leander
中科院分区：
文献类型：
--
作者：
Finkbeiner, Bernd;Hahn, Christopher;Tentrup, Leander
不干扰和观测决定论等超属性将多个系统执行相互关联。它们不能在标准的时态逻辑中表达，如LTL、CTL和CTL*，因此无法使用标准的运行时验证技术进行监控。为了表示超属性，HyperLTL扩展了线性时间时态逻辑(LTL)，在迹上进行了显式量化。我们研究了HyperLTL公式在三种不同输入模型下的运行时验证问题：(1)并行模型，其中固定数量的系统执行是并行处理的。(2)无界顺序模型，其中系统执行是按顺序处理的，一次一个执行。在该模型中，传入的执行数量是先验的无限的，并且实际上可能永远增长。(3)有界序列模型，其中跟踪是按顺序处理的，传入执行的数量是有界的。我们证明了并行和有界序列模型中的界的存在导致了与无界序列模型中不同的可监控性概念。我们证明了判定无交错超LTL的可测性问题是PSpace-完全的，而这个问题一般是不可判定的。对于每个输入模型，我们都提供了监控算法以及运行时和存储优化。通过识别规范的属性，如自反性、对称性和传递性，我们减少了踪迹之间的比较次数。对于顺序模型，我们提出了一种最小化需要存储的轨迹数量的技术。我们对我们的优化进行了评估，结果表明，这会带来更具伸缩性的监控，特别是显著降低内存消耗。
Hyperproperties, such as non-interference and observational determinism, relate multiple system executions to each other. They are not expressible in standard temporal logics, like LTL, CTL, and CTL*, and thus cannot be monitored with standard runtime verification techniques. HyperLTL extends linear-time temporal logic (LTL) with explicit quantification over traces in order to express hyperproperties. We investigate the runtime verification problem of HyperLTL formulas for three different input models: (1) The parallel model, where a fixed number of system executions is processed in parallel. (2) The unbounded sequential model, where system executions are processed sequentially, one execution at a time. In this model, the number of incoming executions is a-priori unbounded and may in fact grow forever. (3) The bounded sequential model where the traces are processed sequentially and the number of incoming executions is bounded. We show that the existence of a bound in the parallel and bounded sequential models leads to a different notion of monitorability than in the unbounded sequential model. We show that deciding the monitoriability problem for alternation-free HyperLTL is PSpace-complete while the problem is undecidable in general. For every input model, we provide monitoring algorithms along with run-time and storage optimizations. By recognizing properties of specifications such as reflexivity, symmetry, and transitivity, we reduce the number of comparisons between traces. For the sequential models, we present a technique that minimizes the number of traces that need to be stored. We evaluate our optimizations, showing that this leads to a more scalable monitoring and, in particular, a significantly lower memory consumption.