Enforcing Opacity in Modular Systems

Graeme Zinck (1) , Laurie S. L. Ricker (1) , Hervé Marchand (2) , Loïc Hélouët (2)

1 Department of Mathematics and Computer Science [Mount Allison University]
2 SUMO - SUpervision of large MOdular and distributed systems

In discrete-event systems, the opacity of a secret ensures that some behaviors or states cannot be inferred with certainty from partial observation of the system. Enforcing opacity in a discrete-event system, encoded by a finite labelled transition system (LTS), is a way to avoid information leakage. Checking opacity is decidable but costly (EXPTIME in the worst cases). This paper addresses opacity for modular systems in which every module, represented by an LTS, has to protect its own secret (a set of secret states S) w.r.t. a local attacker. Once the system is composed, we assume a coalition between the attackers that share their local view (called the global attacker). Assuming the global attacker can observe all interactions between modules, we provide a reduced-complexity opacity verification technique and an algorithm for constructing local controllers that enforces opacity for each secret separately.

Mots clés: opacity; supervisory control; labelled transition systems; modular systems

Domaines: Génie logiciel [cs.SE]

Graeme Zinck, Laurie S. L. Ricker, Hervé Marchand, Loïc Hélouët. Enforcing Opacity in Modular Systems. IFAC 2020 - Ifac world Congress, Nov 2020, Virtual, Germany. pp.1-8. ⟨hal-02917644⟩