Verifying Security Policies Using Observability Theory

of Discrete Event Systems

Professor Feng Lin

Wayne State University

Department of Electrical and Computer Engineering

Security has become an increasingly important issue in computer systems and networks. An important requirement related to this issue is secrecy formulated in terms of information flow. The central question is whether or not information can flow from one level to another unintentionally. Intransitive non-interference (INI) is proposed to capture the non-existence of the information leaks, referred to in the security literature as interference. Checking INI, however, is not an easy task. We use observability theory of discrete event systems that we developed for supervisory control to derive a necessary and sufficient condition for INI, called iP –observability.

We developed two algorithms for checking iP-observability. The first one can be applied to system with any number of levels. The complexity of checking iP-observability using the first algorithm is exponential. To reduce this complexity, we proposed another algorithm, which is indirect in the sense that it translates the problem of checking iP-observability into the problem of checking P-observability as in supervisory control. Since checking P-observability can be performed with polynomial complexity, the second algorithm is more efficient in terms of computation. However, its drawback is that it can only be used for systems with at most three domains.

We also consider the timed version of the problem. We use timed automaton to model a system and introduce a timed version of INI. Timed INI captures the security property of the system (aspects of secrecy) when time information is of importance, as in the case of embedded and real-time systems, where clocks are accurate and synchronized. Timed INI is much more complex and difficult to verify than INI. In fact, we can show that the problem of determining whether a system satisfies timed INI is, in general, undecidable. More importantly, however, we focus on showing that under certain assumptions, on the time constraints of the events, we can indeed determine whether or not a system satisfies timed INI. This is done by first converting a timed automaton into a regular automaton, for which we know how to check timed INI.

Friday, March 10, 2006

3:30 – 4:30 p.m.

1500 EECS