TY - GEN
T1 - Secure information release in timed automata
AU - Vasilikos, Panagiotis
AU - Nielson, Flemming
AU - Nielson, Hanne Riis
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-319-89722-6_2
DO - 10.1007/978-3-319-89722-6_2
M3 - Article in proceedings
SN - 978-3-319-89721-9
T3 - Lecture Notes in Computer Science
SP - 28
EP - 52
BT - POST 2018: Principles of Security and Trust
PB - Springer
T2 - 7<sup>th</sup> International Conference on Principles of Security and Trust
Y2 - 14 April 2018 through 20 April 2018
ER -