Enforcing opacity of regular predicates on modal transition systems

• Published in: Discrete event dynamic systems 2015-06, Vol.25 (1-2), p.251-270
• Main Authors: Darondeau, Philippe, Marchand, Hervé, Ricker, Laurie
• Format: Article
• Language: English
• Subjects: Asymmetry; Computer Science; Control; Control systems; Convex and Discrete Geometry; Dynamical systems; Dynamics; Electrical Engineering; Lift; Machines; Manufacturing; Mathematics; Mathematics and Statistics; Opacity; Operations Research/Decision Theory; Optimization; Processes; Run time (computers); Software Engineering; Systems Theory
• ISSN: 0924-6703; 1573-7594
• DOI: 10.1007/s10626-014-0193-7

Given a labelled transition system G partially observed by an attacker, and a regular predicate S e c over the runs of G , enforcing opacity of the secret S e c in G means computing a supervisory controller K such that an attacker who observes a run of the controlled system K / G cannot ascertain that the trace of this run belongs to S e c based on the knowledge of G and K . We lift the problem from a single labelled transition system G to the class of all labelled transition systems specified by a Modal Transition System M . The lifted problem is to compute the maximally permissive controller K such that S e c is opaque in K / G for every labelled transition system G which is a model of M . The situations of the attacker and of the controller are asymmetric: at run time, the attacker may fully know G and K whereas the controller knows only M and the sequence of actions executed so far by the unknown G . We address the problem in two cases. Let Σ a denote the set of actions that can be observed by the attacker, and let Σ c and Σ o denote the sets of actions that can be controlled and observed by the controller, respectively. We provide optimal and regular controllers that enforce the opacity of regular secrets when Σ c ⊆ Σ o ⊆ Σ a = Σ . We provide optimal and regular controllers that enforce the opacity of regular upper-closed secrets ( S e c = S e c .Σ ∗ ) under the following assumptions: (i) Σ a ⊆ Σ c ⊆ Σ o = Σ or (ii) Σ a , Σ c ⊆ Σ o = Σ and w Σ ∈ Sec ⇒ w ∈ Sec for all Σ∈Σ∖Σ c .