Supervisory Control for Opacity

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 ?? and an inquisitive user, called the adversary, observes a subset ??a of ??. The confidential information is the fact (when it is true) that the trace of the execution of G on ??* belongs to a regular set S ?? ??*, called the secret. The secret S is said to be opaque w.r.t. G (respectively, G/C) and ??a if the adversary cannot safely infer this fact from the trace of the execution of G (respectively, G/C) on ??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 . This algorithm subsumes two earlier algorithms working under the strong assumption that the alphabet ??a of the adversary and the set of events that the controller can disable are comparable.