Secure information release in timed automata

Panagiotis Vasilikos, Flemming Nielson, Hanne Riis Nielson

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

454 Downloads (Pure)

Abstract

One of the key demands of cyberphysical systems is that they meet their safety goals. Timed automata has established itself as a formalism for modeling and analyzing the real-time safety aspects of cyberphysical systems. Increasingly it is also demanded that cyberphysical systems meet a number of security goals for confidentiality and integrity. Notions of security based on Information flow control, such as non-interference, provide strong guarantees that no information is leaked; however, many cyberphysical systems leak intentionally some information in order to achieve their purposes. In this paper, we develop a formal approach of information flow for timed automata that allows intentional information leaks. The security of a timed automaton is then defined using a bisimulation relation that takes account of the non-determinism and the clocks of timed automata. Finally, we define an algorithm that traverses a timed automaton and imposes information flow constraints on it and we prove that our algorithm is sound with respect to our security notion.
Original languageEnglish
Title of host publicationPOST 2018: Principles of Security and Trust
PublisherSpringer
Publication date2018
Pages28-52
ISBN (Print)978-3-319-89721-9
DOIs
Publication statusPublished - 2018
Event7th International Conference on Principles of Security and Trust - Makedonia Palace, Thessaloniki, Greece
Duration: 14 Apr 201820 Apr 2018

Conference

Conference7th International Conference on Principles of Security and Trust
LocationMakedonia Palace
Country/TerritoryGreece
CityThessaloniki
Period14/04/201820/04/2018
SeriesLecture Notes in Computer Science
Volume10804
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Secure information release in timed automata'. Together they form a unique fingerprint.

Cite this