Skip to Main content Skip to Navigation
Conference papers

Enforcing Opacity in Modular Systems

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Hervé Marchand Connect in order to contact the contributor
Submitted on : Wednesday, August 19, 2020 - 3:46:10 PM
Last modification on : Monday, April 4, 2022 - 9:28:22 AM
Long-term archiving on: : Monday, November 30, 2020 - 9:53:42 PM


Files produced by the author(s)


  • HAL Id : hal-02917644, version 1


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⟩



Record views


Files downloads