Model Checking Information Flow in Reactive Systems
Model Checking Information Flow in Reactive Systems
复制标题
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
大多数信息流特性的分析方法没有考虑时间限制。然而，在实践中，这样的属性很少静态地发生，而是必须考虑约束，例如何时以及在何种条件下变量必须保密。在本文中，我们提出了一个自然的整合信息流的性质到线性时间时序逻辑（LTL）。我们增加了一个新的模态算子，隐藏算子，表示系统的可观察行为与秘密变量的赋值无关。我们提供了一个复杂性分析的模型检查问题所产生的逻辑SecLTL，我们确定了一个表达片段，这个问题是有效的决定。我们还表明，隐藏操作符的路径为基础的性质允许无缝集成到分支时间逻辑。
Most analysis methods for information flow properties do not consider temporal restrictions. In practice, however, such properties rarely occur statically, but have to consider constraints such aswhen and under which conditionsa variable has to be kept secret. In this paper, we propose a natural integration of information flow properties into linear-time temporal logics (LTL). We add a new modal operator, the hide operator, expressing that the observable behavior of a system is independent of the valuations of a secret variable. We provide a complexity analysis for the model checking problem of the resulting logic SecLTL and we identify an expressive fragment for which this question is efficiently decidable. We also show that the path based nature of the hide operator allows for seamless integration into branching time logics.