Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus Rabe and Helmut Seidl. Model Checking Information Flow in Reactive Systems. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation, volume 7148 of Lecture Notes in Computer Science, pages 169-185, 2012. 10.1007/978-3-642-27940-9_12. Springer Berlin / Heidelberg.

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 as when and under which conditions a 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.

Reference: Bibtex