TY - GEN
T1 - Model checking information flow in reactive systems
AU - Dimitrova, Rayna
AU - Finkbeiner, Bernd
AU - Kovács, Máté
AU - Rabe, Markus N.
AU - Seidl, Helmut
N1 - Funding Information:
This work was partially supported by the German Research Foundation (DFG) under the project SpAGAT (grant no. FI 936/2-1) in the priority program “Reliably Secure Software Systems – RS3”.
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84856149534&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-27940-9_12
DO - 10.1007/978-3-642-27940-9_12
M3 - Conference contribution
AN - SCOPUS:84856149534
SN - 9783642279393
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 169
EP - 185
BT - Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings
T2 - 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012
Y2 - 22 January 2012 through 24 January 2012
ER -