Model Checking Information Flow in Reactive Systems

RS3 Best Paper Award 2011/2012
Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe and Helmut Seidl

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.

13th International Conference on Verification, Model Checking, and Abstract Interpretation January 2012
Contact Data Privacy Policy Imprint
Home People Publications
More