Supervisory Control for Opacity
Jérémy Dubreil, Philippe Darondeau, Hervé Marchand · IEEE Transactions on Automatic Control · 2010
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 systemGthat may leak confidential information, the problem consists in designing a controllerC, possibly disabling occurrences of a fixed subset of events ofG, so that the closed-loop systemG/Cdoes not leak confidential information. We consider this problem in the case whereGis a finite transition system with set of events ¿ and an inquisitive user, called the adversary, observes a subset ¿aof ¿. The confidential information is the fact (when it is true) that the trace of the execution ofGon ¿* belongs to a regular setS¿ ¿*, called the secret. The secretSis said to be opaque w.r.t.G(respectively,G/C) and ¿aif the adversary cannot safely infer this fact from the trace of the execution ofG(respectively,G/C) on ¿a*. In the converse case, the secret can be disclosed. We present an effective algorithm for computing the most permissive controllerCsuch thatSis opaque w.r.t.G/Cand ¿a. This algorithm subsumes two earlier algorithms working under the strong assumption that the alphabet ¿aof the adversary and the set of events that the controller can disable are comparable.