Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Monitoring Temporal Information Flow
verfasst von : Rayna Dimitrova, Bernd Finkbeiner, Markus N. Rabe
Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present a framework for monitoring information flow in security-critical reactive systems, such as communication protocols, cell phone apps, document servers and web browsers. The secrecy requirements in such systems typically vary over time in response to the interaction with the environment. Standard notions of secrecy, like noninterference, must therefore be extended by specifying precisely
when
and
under what conditions
a particular event needs to remain secret. Our framework is based on the temporal logic SecLTL, which combines the standard temporal operators of linear-time temporal logic with the modal
Hide
operator for the specification of information flow properties. We present a first monitoring algorithm for SecLTL specifications, based on a translation of SecLTL formulas to alternating automata, and identify open research questions and directions for future work.