Model checking information flow in reactive systems

Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe, Helmut Seidl

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

42 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings
Pages169-185
Number of pages17
DOIs
StatePublished - 2012
Event13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012 - Philadelphia, PA, United States
Duration: 22 Jan 201224 Jan 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7148 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012
Country/TerritoryUnited States
CityPhiladelphia, PA
Period22/01/1224/01/12

Fingerprint

Dive into the research topics of 'Model checking information flow in reactive systems'. Together they form a unique fingerprint.

Cite this