Runtime Verification for HyperLTL

Runtime Verification for HyperLTL
复制标题

HyperLTL 的运行时验证

DOI:
10.1007/978-3-319-46982-9_4
复制
发表时间:
2016
期刊:
J. Comput. Secur.
影响因子:
--
通讯作者:
B. Finkbeiner
B. Finkbeiner
中科院分区:
--
文献类型:
--
作者:
Borzoo Bonakdarpour;B. Finkbeiner

文献摘要

参考文献

被引文献

相似文献

信息流安全性通常涉及对多个执行跟踪的推理。这种微妙之处源于这样一个事实,即入侵者可能通过观察和比较几个执行来获得有关系统的知识。跟踪集的这些属性(也称为超属性)的监视对于运行时验证是一个挑战,因为大多数监视技术仅限于对单个跟踪的分析。在本教程中,我们将讨论HyperLTL的这一挑战,HyperLTL是一种用于规范超属性的时态逻辑。
Information flow security often involves reasoning about multiple execution traces. This subtlety stems from the fact that an intruder may gain knowledge about the system through observing and comparing several executions. The monitoring of such properties of sets of traces, also known as hyperproperties, is a challenge for runtime verification, because most monitoring techniques are limited to the analysis of a single trace. In this tutorial, we discuss this challenge with respect to HyperLTL, a temporal logic for the specification of hyperproperties.
DOI: 10.1007/978-3-642-27940-9_12
发表时间: 2012-01
期刊: --
影响因子: --
作者:
Rayna Dimitrova;B. Finkbeiner;Máté Kovács;M. Rabe;H. Seidl
通讯作者: Rayna Dimitrova;B. Finkbeiner;Máté Kovács;M. Rabe;H. Seidl
在具有任意多个代理的工作流中指定和验证保密性
DOI: 10.1007/978-3-319-46520-3_11
发表时间: 2016
期刊:
影响因子: --
作者:
Bernd Finkbeiner;Helmut Seidl;Christian Müller
通讯作者: Christian Müller