Supervisory Control for Opacity

Jérémy Dubreil (1) , Philippe Darondeau (2) , Hervé Marchand (1)

1 VERTECS - Verification models and techniques applied to testing and control of reactive systems
2 S4 - System synthesis and supervision, scenarios

In the field of computer security, a problem that received little attention so far is the enforcement of confidentiality properties by supervisory control. Given a critical system G that may leak confidential information, the problem consists in designing a controller C, possibly disabling occurrences of a fixed subset of events of G, so that the closed-loop system G/C does not leak confidential information. We consider this problem in the case where G is a finite transition system with set of events A and an inquisitive user, called the adversary, observes a subset A_a of A. The confidential information is the fact (when it is true) that the trace of the execution of G on A^* belongs to a regular set S in A^*, called the secret. The secret S is said to be opaque w.r.t. G (resp. G/C) and A_a if the adversary cannot safely infer this fact from the trace of the execution of G (resp. G/C) on A_a^*. In the converse case, the secret can be disclosed. We present an effective algorithm for computing the most permissive controller C such that S is opaque w.r.t. G/C and A_a. This algorithm subsumes two earlier algorithms working under the strong assumption that the alphabet A_a of the adversary and the set of events that the controller can disable are comparable

Domaines: Génie logiciel [cs.SE]

Jérémy Dubreil, Philippe Darondeau, Hervé Marchand. Supervisory Control for Opacity. IEEE Transactions on Automatic Control, 2010, 55 (5), pp.1089-1100. ⟨10.1109/TAC.2010.2042008⟩. ⟨inria-00483891⟩