Control and synthesis of non-interferent timed systems

Abstract

We focus on the control and the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference property. Intuitively, non-interference ensures the absence of any causal dependency from a high-level domain to a lower level domain. 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 two (bi)simulation-based variants thereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties and their extensions have been mostly studied in the context of discrete event systems, while it is now well-known that time is an important attack vector against secure systems.

At the same time, there is an obvious interest in going beyond simple verification to control problems: to be able to automatically make systems secure.

We consider non-interference properties in the challenging setting of control of dense-time systems specified by timed automata and we study the two following problems: (1) check whether it is possible to find a sub-system so that it is non-interferent; if yes, (2) compute a (largest) sub-system which is non-interferent.

We exhibit decidable sub-classes for these problems, assess their theoretical complexities and provide effective algorithms based on the classical framework of timed games.

Keywords:

• control
• synthesis
• non-interference
• timed automaton
• safety timed games

Notes

1. For i = 0, this is the amount of time since the system started.

2. We assume that and .

3. Recall that A₂ is deterministic.