Synthesis of Non-Interferent Timed Systems

In this paper, we focus on the synthesis of secure timed systems which are given by timed automata. The security property that the system must satisfy is a non-interference property. Various notions of non-interference have been defined in the literature, and in this paper we focus on Strong Non-deterministic Non-Interference (SNNI) and we study the two following problems: (1) check whether it is possible to enforce a system to be SNNI; if yes (2) compute a subsystem which is SNNI. Key words: Non-Interference, Synthesis, Timed Automaton.

• Type: Conference
• Year: 2009
• Where: FORMATS
• Authors: Gilles Benattar, Franck Cassez, Didier Lime, Olivier H. Roux
• Keywords: Formal Methods, FORMATS 2009, Secure Timed Systems, Strong Non-deterministic Non-Interference, Timed Automata