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

https://hal.inria.fr/hal-02917644
Contributor : Hervé Marchand <>
Submitted on : Wednesday, August 19, 2020 - 3:46:10 PM
Last modification on : Thursday, January 7, 2021 - 4:19:37 PM
Long-term archiving on: : Monday, November 30, 2020 - 9:53:42 PM

File

IFAC20_3494_FI.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02917644, version 1

Citation

Graeme Zinck, Laurie 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⟩

Share

Metrics

Record views

41

Files downloads

191