Problems Related to Opacity

Roughly the opposite goal of opacity: instead of keeping the observer's state estimate imprecise, detectability asks whether that estimate eventually becomes exact. The two properties are built from the same observer/estimator machinery, which is why they're constantly studied side by side.

• Deciding Detectability for Labeled Petri Nets
  Tomáš Masopust, Xiang Yin · Automatica, 104, pp. 238–241, 2019 · doi.org/10.1016/j.automatica.2019.02.058 · preprint: arXiv:1802.02087
  detectability
  Show abstractHide abstract

  Detectability of discrete event systems is a property to decide whether the current and subsequent states can be determined based on observations. We investigate the existence of algorithms for checking strong and weak detectability for systems modeled as labeled Petri nets. Strong detectability requires that we can always determine, after a finite number of observations, the current and subsequent markings of the system, while weak detectability requires that we can determine, after a finite number of observations, the current and subsequent markings for some trajectories of the system. We show that there is an algorithm to check strong detectability requiring exponential space, and that there is no algorithm to check weak detectability.
• Verification of Detectability for Unambiguous Weighted Automata
  Aiwen Lai, Sébastien Lahaye, Alessandro Giua · IEEE Transactions on Automatic Control, 66(3), pp. 1437–1444, 2021 · doi.org/10.1109/TAC.2020.2995173
  detectability · weighted-automata
  Show abstractHide abstract

  In this article, we deal with the detectability problem for unambiguous weighted automata (UWAs). The problem is to determine if, after a finite number of observations, the set of possible states is reduced to a singleton. Four types of detectabilities, namely, strong detectability, detectability, strong periodic detectability, and periodic detectability are defined in terms of different requirements for current state estimation. We first construct a deterministic finite state automaton (called observer) over a weighted alphabet and prove that it can be used as the current-state estimator of the studied UWA. Finally, necessary and sufficient conditions based on the observer are proposed to verify detectabilities of a UWA.
• Detectability of Labeled Weighted Automata over Monoids
  Kuize Zhang · Discrete Event Dynamic Systems, 32(3), pp. 435–494, 2022 · doi.org/10.1007/s10626-022-00362-8 · arXiv:2006.14164
  detectability · weighted-automata
  Show abstractHide abstract

  In this paper, by developing appropriate methods, we for the first time obtain characterization of four fundamental notions of detectability for general labeled weighted automata over monoids (denoted by 𝒜^𝔐 for short), where the four notions are strong (periodic) detectability (SD and SPD) and weak (periodic) detectability (WD and WPD). The contributions of the current paper are as follows. Firstly, we formulate the notions of concurrent composition, observer, and detector for 𝒜^𝔐. Secondly, we use the concurrent composition to give a necessary and sufficient condition for SD, use the detector to give a necessary and sufficient condition for SPD, and use the observer to give necessary and sufficient conditions for WD and WPD, all for general 𝒜^𝔐 without any assumption. Thirdly, we prove that for a labeled weighted automaton over monoid (ℚ^k,+) (denoted by 𝒜^ℚk), its concurrent composition, observer, and detector can be computed in NP, 2-EXPTIME, and 2-EXPTIME, respectively, by developing novel connections between 𝒜^ℚk and the NP-complete exact path length problem (proven by [Nykänen and Ukkonen, 2002]) and a subclass of Presburger arithmetic. As a result, we prove that for 𝒜^ℚk, SD can be verified in coNP, while SPD, WD, and WPD can be verified in 2-EXPTIME. Particularly, for 𝒜^ℚk in which from every state, a distinct state can be reached through some unobservable, instantaneous path, detector 𝒜^ℚk_det can be computed in NP, and SPD can be verified in coNP. Finally, we prove that the problems of verifying SD and SPD of deterministic, deadlock-free, and divergence-free 𝒜^ℕ over monoid (ℕ,+) are both coNP-hard. The original methods developed in this paper will provide foundations for characterizing other fundamental properties (e.g., diagnosability and opacity) in labeled weighted automata over monoids. In addition, in order to differentiate labeled weighted automata over monoids from labeled timed automata, we also initially explore detectability in labeled timed automata, and prove that the SD verification problem is PSPACE-complete, while WD and WPD are undecidable.
• Formulation and Verification of Strong Detectability for Labeled Real-Time Automata — A Concurrent-Composition Method
  Kuize Zhang · Information and Computation, 313, article 105519, 2026 · doi.org/10.1016/j.ic.2026.105519
  detectability
  Show abstractHide abstract

  Real-time automata are a widely-used class of real-time systems. In this paper, two versions of strong detectability are formulated for a labeled real-time automaton (LRTA) which imply after some delay (the number of observed labels or real-time delay), along every generated infinite run, one can determine the current and subsequent states by observing the generated timed label sequence. By using the concurrent composition defined and computed in one of the author’s previous papers, necessary and sufficient conditions for the negations of the two strong versions of detectability are given. It is also proven that the verification problems for the two definitions of strong detectability are both coNP-complete. As a byproduct, an NP state estimation algorithm for LRTAs is shown as well.

Will the system eventually and always detect that a specific fault occurred, within some bounded delay? A third sibling alongside opacity and detectability, often grouped together in surveys as the canonical trio of partial-observation verification problems.

• Overview of Fault Diagnosis Methods for Discrete Event Systems
  Janan Zaytoon, Stéphane Lafortune · Annual Reviews in Control, 37(2), pp. 308–320, 2013 · doi.org/10.1016/j.arcontrol.2013.09.009
  diagnosability
  Show abstractHide abstract

  Fault diagnosis of Discrete Event Systems has become an active research area in recent years. The research activity in this area is driven by the needs of many different application domains such as manufacturing, process control, control systems, transportation, communication networks, software engineering, and others. The aim of this paper is to review the state-of the art of methods and techniques for fault diagnosis of Discrete Event Systems based on models that include faulty behaviour. Theoretical and practical issues related to model description tools, diagnosis processing structure, sensor selection, fault representation and inference are discussed.
• Verification Complexity of a Class of Observational Properties for Modular Discrete Event Systems
  Xiang Yin, Stéphane Lafortune · Automatica, 83, pp. 199–205, 2017 · doi.org/10.1016/j.automatica.2017.06.013
  Covers diagnosability, predictability and detectability rather than opacity itself; the Masopust and Yin paper that follows treats opacity for modular systems.
  distributed · modular · opacity
  Show abstractHide abstract

  A modular discrete event system is modeled by a set of module automata running synchronously. In this paper, we investigate the complexity of the verification problems of three different properties, diagnosability, predictability, and detectability, for partially-observed modular discrete event systems. We first show that deciding diagnosability for modular discrete event systems is PSPACE-complete when the number of modules is unbounded. Then we show that deciding predictability and detectability for modular discrete event systems are both PSPACE-hard problems. These results reveal that in order to verify these properties for the complete system, exploring the state space of the monolithic model may be unavoidable, in the worst case.
• The Complexity of Diagnosability and Opacity Verification for Petri Nets
  Béatrice Bérard, Stefan Haar, Sylvain Schmitz, Stefan Schwoon · Fundamenta Informaticae, 161(4), pp. 317–349, 2018 · doi.org/10.3233/FI-2018-1706 (journal version; conference precursor: 38th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2017), LNCS vol. 10258, pp. 200–220, Springer · doi.org/10.1007/978-3-319-57861-3_13)
  Compares the two problems: diagnosability goes from NL-complete (finite-state systems) to PSPACE-complete (safe convergent nets) and EXPSPACE-complete (general nets without fairness).
  classical · diagnosability · infinite-state · opacity · petri-nets
  Show abstractHide abstract

  Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe convergent Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is EXPSPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.
• Accurate Approximate Diagnosis of (Controllable) Stochastic Systems
  Engel Lefaucheux · Quantitative Evaluation of Systems (QEST 2021), Springer LNCS vol. 12846, pp. 413–434 · doi.org/10.1007/978-3-030-85172-9_22
  Its conclusion relates the accurate approximate disclosure studied here to quantitative opacity, presented as a kind of dual to diagnosability.
  applications · opacity · stochastic
  Show abstractHide abstract

  Diagnosis of partially observable stochastic systems prone to faults was introduced in the late nineties. Diagnosability may be specified in different ways: exact diagnosability requires that almost surely a fault is detected and that no fault is erroneously claimed; approximate diagnosability tolerates a small error probability when claiming a fault; last, accurate approximate diagnosability guarantees that the error probability can be chosen arbitrarily small. While all three notions were studied for passive systems such as observable Markov chains, only the exact notion was considered for systems equipped with a controller. As the approximate notion of diagnosability was shown to be undecidable in passive systems, in this article, we complete the picture by deciding the accurate approximate diagnosability for controllable observable Markov chains. More precisely, we show how to adapt the accurate approximate notion to the active setting and establish EXPTIME-completeness of the associated decision problem. We also show how to measure the set of faulty paths that are detected under the accurate approximate notion in the passive setting.
• Distributed Fault Diagnosis in Discrete Event Systems With Transmission Delay Impairments
  Jiwei Wang, Simone Baldi, Wenwu Yu, Xiang Yin · IEEE Transactions on Automatic Control, 69(8), pp. 5508–5515, 2024 · doi.org/10.1109/TAC.2024.3369510 · preprint: arXiv:2608.06035
  diagnosability · distributed
  Show abstractHide abstract

  This note studies the distributed fault diagnosis problem in partially-observed discrete event systems, where the system is monitored by a group of agents to cooperatively diagnose faults within a finite number of steps. The novelty of this work is the creation of a methodology to verify when the faults can be diagnosed even in the presence of transmission delay impairments. To address this scenario, a new distributed diagnosability condition is proposed, which extends decentralized diagnosability conditions proposed in the literature. Such distributed diagnosability condition is then verified via a novel structure named delay recorder and a new diagnosis function. Theoretical analysis shows that the verification method can successfully determine whether the faults can be diagnosed.
• Distributed Sensing and Information Transmission of Discrete-Event Systems with Edge Sensors
  Yingying Liu, Shaoyuan Li, Jin Hu, Xiang Yin · IEEE Transactions on Automatic Control, 71(5), pp. 3432–3439, 2026 · doi.org/10.1109/TAC.2025.3639520 (journal version; conference precursor: Yingying Liu, Xiang Yin, Shaoyuan Li · 60th IEEE Conference on Decision and Control (CDC 2021), pp. 309–315 · doi.org/10.1109/CDC45484.2021.9683006)
  detectability · diagnosability · distributed
  Show abstractHide abstract

  This article studies distributed sensing and information transmission in partially observed discrete-event systems with edge sensors. We assume that each edge sensor selectively transmits its observable events, according to information transmission policies, to a central site for the purpose of decision making. A general class of decision-making requirement at the central site called distinguishability is considered. We consider both the verification problem and the synthesis problem in this setting. For the verification problem, two different approaches, one based on the observer and the other based on the verifier, are proposed to check whether or not a given set of sensor transmission policies fulfills the distinguishability requirement. For the synthesis problem, we also develop an effective algorithm to design an observer-based optimal information transmission policy for each edge sensor. Moreover, we show that finding an information transmission policy with minimal number of transmitted events is NP-hard.
• Verification and Enforcement of Concealability and Diagnosability in Probabilistic Timed Automata
  Tareq Ahmad Al-Sarayrah, Sjood Ammen Daje, Ding Liu, Mohamed Ghazel, Zhiwu Li · IEEE Transactions on Automation Science and Engineering, 23, pp. 12827–12846, 2026 · doi.org/10.1109/TASE.2026.3709035
  Studies diagnosability in probabilistic timed automata alongside concealability, using diagnosers, and analyzes the interplay between the two.
  concealability · diagnosability · stochastic · timed
  Show abstractHide abstract

  This study explores the diagnosability and concealability in discrete event systems modeled by probabilistic timed automata, with a focus on the concept of enforced concealability. The research enhances methods for verifying concealability, with a particular emphasis on concealability during state transitions and the critical temporal elements that ensure security and operational privacy. In this model, observers and diagnosers are central, with the latter playing a critical role in enhancing system concealability. We analyze the interplay between diagnosability and concealability in discrete event systems, viewed through a probabilistic timed approach to advance system secrecy. A key aspect of this research is the application of supervisory control for selective event disabling, which is effective in maintaining desired system states, thus optimizing process flows. The proposed approach is illustrated through a case study on a city-scale intelligent transportation system modeled via a dual probabilistic timed-automaton construction (a primary model and an auxiliary mimic model) for an urban autonomous passenger transport mission (e.g., an automated shuttle or robo-taxi) under partial observation, which demonstrates not only the framework’s capacity for enforcing concealability but also its impact on operational efficiency and security. Including a practical case study underscores the managerial implications and real-world applicability of these methods, laying the groundwork for future research in process modeling and data feature analysis. The main aim is to facilitate the implementation of the proposed framework as a protective measure in systems necessitating augmented security. Note to Practitioners—Modern engineering systems are increasingly complex, challenging their security and reliability, especially under partial observability and probabilistic constraints. This article introduces a framework using probabilistic timed automata to address these challenges by incorporating diagnosability and concealability concepts, suitable for secure communication protocols and supervisory control systems. We present methods that enhance system secrecy and verify critical transitions, advancing both theoretical understanding and practical application. These techniques are designed to handle uncertainties inherent in cyberphysical systems, making them relevant in cybersecurity, industrial automation, and intelligent transportation systems. Engineers and system designers will find the methodologies valuable for enhancing system reliability and security in dynamic environments. This study provides major insights and tools for professionals in automated control, offering new perspectives and methods to effectively manage nondeterministic observations and state estimations.
• Existential Opacity for Discrete-Event Systems with State Observations
  Zhiyuan Huang, Zhao Tong, Jiakai Li, Bingzhuo Zhong · arXiv preprint, 2026 · arXiv:2609.02132
  Read from the diagnosability side, existential opacity is essentially the negation of a diagnosis requirement: it holds when some secret behavior is never told apart from a non-secret one by the observations, whereas diagnosing the secret would require every secret behavior to be revealed. The standard diagnosability definition adds a bounded-delay condition that is not part of this notion.
  classical · diagnosability · opacity · trajectory-planning
  Show abstractHide abstract

  Opacity is a fundamental system property for confidentiality in discrete-event systems (DES). Classical opacity is typically defined under event-based observations, requiring that any secret system behavior remains indistinguishable from some non-secret behavior to an external intruder. However, in many applications such as path planning or opacity-preserving tasks, the intruder observes system states rather than events. Moreover, it often suffices that the system exhibits secret behaviors that can be exploited for opacity-preserving task execution, but such a system property cannot be fully captured by existing notions of state-observation-based opacity. Motivated by this limitation, we propose a relaxed notion of existing state-observation-based opacity, called existential opacity (EO), which only requires the existence of secret behaviors (instead of all secret behaviors) that are indistinguishable from a non-secret behavior under the state observations of the intruder. We show that the notion of EO is more expressive than existing state-observation-based opacity notions. In addition, a class of EO properties together with their corresponding verification approaches are developed, enabling the analysis of existential opacity in discrete-event systems and providing a new criterion for determining the feasibility of opacity-preserving problems.

An event-level cousin of opacity: rather than an intruder never becoming certain the system is in a secret state, concealability asks that a designated set of secret events never become certain to have occurred, using the same partial-observation eavesdropper model as opacity but operating on events instead of states.

• Event Concealment and Concealability Enforcement in Discrete Event Systems Under Partial Observation
  Wei Duan, Christoforos N. Hadjicostis, Zhiwu Li · IEEE Transactions on Automatic Control, 69(10), pp. 7263–7269, 2024 · doi.org/10.1109/TAC.2024.3397198 · arXiv:2205.03170
  concealability
  Show abstractHide abstract

  In this article, we investigate event concealment and concealability enforcement in discrete event systems modeled as nondeterministic finite automata under partial observation. Given a subset of secret events in a given system, concealability holds if the occurrences of all secret events remain hidden to a curious observer (an eavesdropper). When concealability of a system does not hold, we analyze how a defensive function, placed at the interface of the system with the eavesdropper, can be used to enforce concealability by manipulating the observations generated by the system using event deletions, insertions, or replacements. The defensive function is said to be C-enforcing if, following the occurrence of secret events and regardless of earlier and subsequent activity generated by the system, it can always deploy a strategy to manipulate observations and conceal the secret events perpetually. We propose a polynomial complexity construction for obtaining one necessary and one sufficient condition for C-enforceability.
• Verification and Enforcement of Concealability and Diagnosability in Probabilistic Timed Automata
  Tareq Ahmad Al-Sarayrah, Sjood Ammen Daje, Ding Liu, Mohamed Ghazel, Zhiwu Li · IEEE Transactions on Automation Science and Engineering, 23, pp. 12827–12846, 2026 · doi.org/10.1109/TASE.2026.3709035
  Studies concealability in probabilistic timed automata, with a focus on enforced concealability through supervisory control that selectively disables events.
  concealability · diagnosability · stochastic · timed
  Show abstractHide abstract

  This study explores the diagnosability and concealability in discrete event systems modeled by probabilistic timed automata, with a focus on the concept of enforced concealability. The research enhances methods for verifying concealability, with a particular emphasis on concealability during state transitions and the critical temporal elements that ensure security and operational privacy. In this model, observers and diagnosers are central, with the latter playing a critical role in enhancing system concealability. We analyze the interplay between diagnosability and concealability in discrete event systems, viewed through a probabilistic timed approach to advance system secrecy. A key aspect of this research is the application of supervisory control for selective event disabling, which is effective in maintaining desired system states, thus optimizing process flows. The proposed approach is illustrated through a case study on a city-scale intelligent transportation system modeled via a dual probabilistic timed-automaton construction (a primary model and an auxiliary mimic model) for an urban autonomous passenger transport mission (e.g., an automated shuttle or robo-taxi) under partial observation, which demonstrates not only the framework’s capacity for enforcing concealability but also its impact on operational efficiency and security. Including a practical case study underscores the managerial implications and real-world applicability of these methods, laying the groundwork for future research in process modeling and data feature analysis. The main aim is to facilitate the implementation of the proposed framework as a protective measure in systems necessitating augmented security. Note to Practitioners—Modern engineering systems are increasingly complex, challenging their security and reliability, especially under partial observability and probabilistic constraints. This article introduces a framework using probabilistic timed automata to address these challenges by incorporating diagnosability and concealability concepts, suitable for secure communication protocols and supervisory control systems. We present methods that enhance system secrecy and verify critical transitions, advancing both theoretical understanding and practical application. These techniques are designed to handle uncertainties inherent in cyberphysical systems, making them relevant in cybersecurity, industrial automation, and intelligent transportation systems. Engineers and system designers will find the methodologies valuable for enhancing system reliability and security in dynamic environments. This study provides major insights and tools for professionals in automated control, offering new perspectives and methods to effectively manage nondeterministic observations and state estimations.

An older, language-based-security notion asking that confidential actions never produce any effect observable by an unauthorized user. Some formulations overlap enough with opacity that they've been described as a kind of opacity themselves.

• A Notion of Non-Interference for Timed Automata
  Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, Luca Tesei · Fundamenta Informaticae, 51(1–2), pp. 1–11, 2002 · doi.org/10.5555/2371116.2371118
  non-interference · timed
  Show abstractHide abstract

  The non-interference property of concurrent systems is a security property concerning the flow of information among different levels of security of the system. In this paper we introduce a notion of timed non-interference for real-time systems specified by timed automata. The notion is presented using an automata based approach and then it is characterized also by operations and equivalence between timed languages. The definition is applied to an example of a time-critical system modeling a simplified control of an airplane.
• A Decidable Notion of Timed Non-Interference
  Roberto Barbuti, Luca Tesei · Fundamenta Informaticae, 54(2–3), pp. 137–150, 2003 · doi.org/10.5555/2370741.2370744
  non-interference
  Show abstractHide abstract

  We present a notion of non-interference which embodies the notion of time. It is useful to verify the strength of a system against attacks depending on the frequency of certain actions. In particular we give a decidable definition of non-interference which can be checked by using existing verification tools. We show an application example of our notion of non-interference by defining a variant of the classical Fischer's mutual exclusion protocol and by analyzing its strength against attacks.
• Generalized Abstract Non-interference: Abstract Secure Information-Flow Analysis for Automata
  Roberto Giacobazzi, Isabella Mastroeni · Computer Network Security — MMM-ACNS 2005, LNCS vol. 3685, pp. 209–221, Springer, 2005 · doi.org/10.1007/11560326_17
  non-interference · timed
  Show abstractHide abstract

  Abstract non-interference has been introduced as a weakening non-interference which models attackers as abstract interpretations (i.e., static analyzers) of programming language semantics. In this paper we generalize the notion of abstract non-interference to deal with tree-like models of computation. This allows us to widen the scope of abstract non-interference for modeling security properties in automata, timed automata as models of real-time systems, and concurrent systems. We show that well known definitions of non-interference in these models of computation can be viewed as instances of our generalization. This proves that abstract non-interference can reasonably be considered as a general framework for studying and comparing security properties at different levels of abstraction in both programming languages and systems. Moreover, the most precise harmless attacker of a system is systematically derived by transforming abstract domains, characterizing the security degree of automata and concurrent systems.
• Non-Interference Control Synthesis for Security Timed Automata
  Guillaume Gardey, John Mullins, Olivier H. Roux · Electronic Notes in Theoretical Computer Science, 180(1), pp. 35–53, 2007 · doi.org/10.1016/j.entcs.2005.05.046 · hal-00523598
  non-interference · timed
  Show abstractHide abstract

  In this paper, the problem of synthesizing controllers that ensures non interference for multilevel security dense timed discrete event systems modeled by an extension of Timed Automata, is addressed for the first time. We first discuss a notion of non interference for dense real-time systems that refines notions existing in the literature and investigate decidability issues raised by the verification problem for dense time properties. We then prove the decidability of the problem of synthesis of the timed controller for some of these timed non interference properties, providing so a symbolic method to synthesize a controller that ensures them.
• Checking Noninterference in Timed CSP
  A. W. Roscoe, Jian Huang · Formal Aspects of Computing, 2013 · doi.org/10.1007/s00165-012-0251-6
  non-interference · timed
  Show abstractHide abstract

  A well-established specification of noninterference in CSP is that, when high-level events are appropriately abstracted, the remaining low-level view is deterministic. This is not a workable definition in Timed CSP, where many processes cannot be refined to deterministic ones. We argue that in fact “deterministic” should be replaced by “maximally refined” in the definition above. We show how to automate the resulting timed noninterference check within the context of the recent extension of FDR to analyse a discrete version of Timed CSP, and how an extended theory of digitisation has the potential both to create more accurate specifications and to infer when processes are noninterfering in the more usual continuous-time semantics.
• Control and Synthesis of Non-Interferent Timed Systems
  Gilles Benattar, Franck Cassez, Didier Lime, Olivier H. Roux · International Journal of Control, 88(2), pp. 217–236, 2015 · doi.org/10.1080/00207179.2014.944356 · preprint: arXiv:1207.4984
  non-interference · timed
  Show abstractHide abstract

  We focus on the control and the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference property. Intuitively, non-interference ensures the absence of any causal dependency from a high-level domain to a lower level domain. Various notions of non-interference have been defined in the literature, and in this paper, we focus on strong non-deterministic non-interference (SNNI) and two (bi)simulation-based variants thereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties and their extensions have been mostly studied in the context of discrete event systems, while it is now well-known that time is an important attack vector against secure systems. At the same time, there is an obvious interest in going beyond simple verification to control problems: to be able to automatically make systems secure. We consider non-interference properties in the challenging setting of control of dense-time systems specified by timed automata and we study the two following problems: (1) check whether it is possible to find a sub-system so that it is non-interferent; if yes, (2) compute a (largest) sub-system which is non-interferent. We exhibit decidable sub-classes for these problems, assess their theoretical complexities and provide effective algorithms based on the classical framework of timed games.
• Non-interference in Partial Order Models
  Béatrice Bérard, Loïc Hélouët, John Mullins · ACM Transactions on Embedded Computing Systems, 16(2), article 44, 2017 · doi.org/10.1145/2984639 · hal-01379451
  distributed · infinite-state · non-interference
  Show abstractHide abstract

  Non-interference (NI) is a property of systems stating that confidential actions should not cause effects observable by unauthorized users. Several variants of NI have been studied for many types of models but rarely for true concurrency or unbounded models. This work investigates NI for High-level Message Sequence Charts (HMSCs), a scenario language for the description of distributed systems, based on composition of partial orders. We first propose a general definition of security properties in terms of equivalence among observations of behaviors. Observations are naturally captured by partial order automata, a formalism that generalizes HMSCs and permits assembling partial orders. We show that equivalence or inclusion properties for HMSCs (and hence for partial order automata) are undecidable, which means in particular that NI is undecidable for HMSCs. We hence consider decidable subclasses of partial order automata and HMSCs. Finally, we define weaker local properties, describing situations where a system is attacked by a single agent, and show that local NI is decidable. We then refine local NI to a finer notion of causal NI that emphasizes causal dependencies between confidential actions and observations and extend it to causal NI with (selective) declassification of confidential events. Checking whether a system satisfies local and causal NI and their declassified variants are PSPACE-complete problems.
• Parametric Non-Interference in Timed Automata
  Étienne André, Aleksander Kryukov · 25th International Conference on Engineering of Complex Computer Systems (ICECCS 2020), pp. 37–42 · doi.org/10.1109/ICECCS51672.2020.00012 · arXiv:2010.09527
  non-interference · timed
  Show abstractHide abstract

  We consider a notion of non-interference for timed automata (TAs) that allows to quantify the frequency of an attack; that is, we infer values of the minimal time between two consecutive actions of the attacker, so that (s)he disturbs the set of reachable locations. We also synthesize valuations for the timing constants of the TA (seen as parameters) guaranteeing non-interference. We show that this can reduce to reachability synthesis in parametric timed automata. We apply our method to a model of the Fischer mutual exclusion protocol and obtain preliminary results.
• Timed Non-Interference Under Partial Observability and Bounded Memory
  Anthony Spriet, Didier Lime, Olivier H. Roux · 21st International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2023), LNCS vol. 14138, pp. 122–137 · doi.org/10.1007/978-3-031-42626-1_8 · hal-04312271
  non-interference · timed
  Show abstractHide abstract

  We investigate a timed non-interference property for security systems modeled as timed automata, in which a low-security level user should not be able to deduce the occurrence of some high-security level actions. We assume an attack model in which the malicious (low-level) user has the ability to partially observe and memorize the set of runs of the timed automaton modeling the system. We first formalize a non-interference property that ensures the system security under such an attack model and we then prove the undecidability of that property when the attacker can have an arbitrarily big memory, i.e., when they are able to memorize sequences of previous observations, with time-stamps, of any length. We next assume bounded memory for the attacker and show that the property can then be decided in PSPACE for a subclass of timed automata ensuring finite duration between distinct observations.
• Noninterference Analysis of Stochastically Timed Reversible Systems
  Andrea Esposito, Alessandro Aldini, Marco Bernardo · 45th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2025), LNCS vol. 15740, pp. 75–95 · doi.org/10.1007/978-3-031-95497-9_5
  non-interference · stochastic · timed
  Show abstractHide abstract

  Noninterference theory aims at ensuring the absence of covert channels among different security levels. As far as the verification of information-flow properties via equivalence checking is concerned, in nondeterministic and probabilistic settings weak bisimilarity has turned out to be adequate only for standard systems, while branching bisimilarity has proven to be appropriate for reversible systems too. In this paper we investigate noninterference for stochastically timed systems represented in the interactive Markov chain model of Hermanns. After recasting a selection of noninterference properties via Markovian variants of weak and branching bisimilarities, we study their preservation and compositionality aspects, build their taxonomy, and compare it with the nondeterministic and probabilistic taxonomies. We show the adequacy of our proposal through some examples about a database management system.

Keeping a deviation statistically hard for a passive observer to detect, bounding a hypothesis test's success probability rather than reasoning over the observer's state estimate. Close enough to opacity in motivation to surface constantly in the same searches.

• Covert Planning against Imperfect Observers
  Haoxiang Ma, Chongyang Shi, Shuo Han, Michael R. Dorothy, Jie Fu · Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2024), pp. 1319–1327, 2024 · doi.org/10.5555/3635637.3662990 · preprint: arXiv:2310.16791
  hypothesis-testing · stochastic
  Show abstractHide abstract

  Covert planning refers to a class of constrained planning problems where an agent aims to accomplish a task with minimal information leaked to a passive observer to avoid detection. However, existing methods of covert planning often consider deterministic environments or do not exploit the observer's imperfect information. This paper studies how covert planning can leverage the coupling of stochastic dynamics and the observer's imperfect observation to achieve optimal task performance without being detected. Specifically, we employ a Markov decision process to model the interaction between the agent and its stochastic environment, and a partial observation function to capture the leaked information to a passive observer. Assuming the observer employs hypothesis testing to detect if the observation deviates from a nominal policy, the covert planning agent aims to maximize the total discounted reward while keeping the probability of being detected as an adversary below a given threshold. We prove that finite-memory policies are more powerful than Markovian policies in covert planning. Then, we develop a primal-dual proximal policy gradient method with a two-time-scale update to compute a (locally) optimal covert policy. We demonstrate the effectiveness of our methods using a stochastic gridworld example. Our experimental results illustrate that the proposed method computes a policy that maximizes the adversary's expected reward without violating the detection constraint, and empirically demonstrates how the environmental noises can influence the performance of the covert policies.

A quantitative sibling of opacity that measures leakage via statistical divergence between the observations a secret behavior produces and the observations a designated “cover” behavior produces, rather than via the observer's state estimate.

• Quantification of Secrecy in Partially Observed Stochastic Discrete Event Systems
  Jun Chen, Mariam Ibrahim, Ratnesh Kumar · IEEE Transactions on Automation Science and Engineering, 14(1), pp. 185–195, 2017 · doi.org/10.1109/TASE.2016.2604222
  divergence-secrecy · stochastic
  Show abstractHide abstract

  While cryptography is used to protect the content of information (e.g., a message) by making it undecipherable, behaviors (as opposed to information) may not be encrypted and may only be protected by partially or fully hiding through creation of ambiguity (by providing covers that generate indistinguishable observations from secrets). Having a cover together with partial observability does cause ambiguity about the system behaviors desired to be kept secret, yet some information about secrets may still be leaked due to statistical difference between the occurrence probabilities of the secrets and their covers. In this paper, we propose a Jensen-Shannon divergence (JSD)-based measure to quantify secrecy loss in systems modeled as partially observed stochastic discrete event systems, which quantifies the statistical difference between two distributions, one over the observations generated by secret and the other over those generated by cover. We further show that the proposed JSD measure for secrecy loss is equivalent to the mutual information between the distributions over possible observations and that over possible system status (secret versus cover). Since an adversary is likely to discriminate more if he/she observes for a longer period, our goal is to evaluate the worst case loss of secrecy as obtained in the limit over longer and longer observations. Computation for the proposed measure is also presented. Illustrative examples, including the one with side-channel attack, are provided to demonstrate the proposed computation approach.

As defined in this pair of articles, confidentiality is opacity's closest sibling, and easy to mistake for a synonym: an eavesdropper must not recover the secret, but unlike opacity, a designated "friendly" recipient must still be able to. That authorized-recovery requirement is what keeps it a distinct property rather than a renaming of opacity.

• Existence Conditions for Confidentiality in Discrete-Event Systems
  Bryony H. Laporte (published as Bryony H. Schonewille), Karen Rudie · 2024 American Control Conference (ACC), pp. 5412–5418 · doi.org/10.23919/ACC60939.2024.10644328
  confidentiality
  Show abstractHide abstract

  Confidentiality as it has been formulated for discrete-event systems is a way of defining security which allows friendly agents to recover obscured secret information. This work presents two new definitions for confidentiality in discrete-event systems that model the scenario when an adversary is eavesdropping from the beginning of a system's evolution. Necessary and sufficient conditions are also provided for each version of confidentiality that describe the properties a system needs for an encryption function to exist that enforces confidentiality on the system.
• Existence Conditions for Stealthy Confidentiality of Discrete-Event Systems
  Bryony H. Laporte, Karen Rudie · 2025 IEEE 64th Conference on Decision and Control (CDC), pp. 261–268 · doi.org/10.1109/CDC57313.2025.11312361
  confidentiality
  Show abstractHide abstract

  Confidentiality is a security model for discreteevent systems that uses an encryption function to obscure communications so the original information can be recovered by any agent with the decryption key. In this work we introduce the idea of stealthy confidentiality, namely when the set of possible behaviours of the encrypted system appears to be possible behaviours of the actual plant. We then present conditions that must be satisfied for stealthy confidentiality-enforcing encryption functions to exist under the assumptions from our previous work and under generalized assumptions that permit the existence of strings that are neither secret nor non-secret.