Opacity of Stochastic Systems

Definitions, decidability, and complexity results for opacity across the stochastic models on this page. Most of the literature here re-derives the classical automaton-based notions with probabilities, or some other form of graded uncertainty, attached, then asks how hard the resulting problem is to decide, which turns out to be undecidable in general and only recoverable under restrictions.

Algorithms and techniques that make checking, or enforcing, the notions from category A actually tractable, as opposed to defining them. Belief-state estimators blow up combinatorially just like their non-probabilistic counterparts, so each article here targets that scalability problem with a specific technique: two-way observers, belief abstraction, barrier certificates, or a simulation relation that lets a smaller model stand in for verification.

• Privacy Verification and Enforcement via Belief Abstraction
  Bo Wu, Hai Lin · IEEE Control Systems Letters, 2(4), pp. 815–820, 2018 · doi.org/10.1109/LCSYS.2018.2849554 · earlier version: “Privacy Preserving Controller Synthesis via Belief Abstraction”, arXiv:1802.10051, 2018 · arXiv:1802.10051
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  Privacy is a crucial concern in many practical systems. We consider a new notion of privacy based on beliefs of the system states, which is closely related to opacity in discrete event systems. To guarantee the privacy requirement, we propose to abstract the belief space whose dynamics is shown to be mixed monotone where efficient abstraction algorithm exists. Based on the abstraction, we propose two different approaches to preserve privacy with an illustrative example.
• Privacy Verification in POMDPs via Barrier Certificates
  Mohamadreza Ahmadi, Bo Wu, Hai Lin, Ufuk Topcu · 57th IEEE Conference on Decision and Control (CDC), pp. 5610–5615, 2018 · doi.org/10.1109/CDC.2018.8619061
  opacity · stochastic
  Show abstractHide abstract

  Privacy is an increasing concern in cyber-physical systems that operates over a shared network. In this paper, we propose a method for privacy verification of cyber-physical systems modeled by Markov decision processes (MDPs) and partially-observable Markov decision processes (POMDPs) based on barrier certificates. To this end, we consider an opacity-based notion of privacy, which is characterized by the beliefs in system states. We show that the belief update equations can be represented as discrete-time switched systems, for which we propose a set of conditions for privacy verification in terms of barrier certificates. We further demonstrate that, for MDPs and for POMDPs, privacy verification can be computationally implemented by solving a set of semi-definite programs and sum-of-squares programs, respectively. The method is illustrated by an application to privacy verification of an inventory management system.
• Opacity Verification in Stochastic Discrete Event Systems Using Two-Way Observers
  Guangzhao Qi, Fuchun Liu, Hongyan Cui · Journal of Guangdong University of Technology, 40(3), pp. 32–37, 2023 (published in Chinese) · doi.org/10.12052/gdutxb.210169
  opacity · stochastic
  Show abstractHide abstract

  The opacity of stochastic discrete event system is studied for stochastic system models. Firstly, the notions of stochastic infinite-step opacity and stochastic K-step opacity are formalized. By constructing a validator based on a two-way observer, a necessary and sufficient condition is obtained to verify the stochastic infinite-step opacity and stochastic K-step opacity of systems by using the validator of two-way observer. Finally, the verification algorithm for stochastic infinite-step opacity and stochastic K-step opacity based on two-way observer is proposed.
• Verifying Opacity Properties in Security Systems
  Chunyan Mu, David Clark · IEEE Transactions on Dependable and Secure Computing, 20(2), pp. 1450–1460, 2023 · doi.org/10.1109/TDSC.2022.3155323
  Adds a probabilistic operator to OpacTL for quantitative analysis in PRISM; the core model and main results stay qualitative, and an entropy-based quantification is only sketched.
  classical · finite-automata · opacity · stochastic
  Show abstractHide abstract

  We delineate a methodology for the specification and verification of flow security properties expressible in the opacity framework. We propose a logic, OpacTL, for straightforwardly expressing such properties in systems that can be modelled as partially observable labelled transition systems. We develop verification techniques for analysing property opacity with respect to observation notions. Adding a probabilistic operator to the specification language enables quantitative analysis and verification. This analysis is implemented as an extension to the PRISM model checker and illustrated via a number of examples. Finally, an alternative approach to quantifying the opacity property based on entropy is sketched.

Where categories A and B verify or measure leakage in a fixed system, this one is about actively synthesizing a controller or policy in an MDP that keeps a secret opaque going forward: supervisors, masking policies, and planners, several of them adversarial or game-theoretic in flavor.

• Probabilistic Opacity for Markov Decision Processes
  Béatrice Bérard, Krishnendu Chatterjee, Nathalie Sznajder · Information Processing Letters, 115(1), pp. 52–59, 2015 · doi.org/10.1016/j.ipl.2014.09.001 · hal-01176435
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  Opacity is a generic security property, that has been defined on (non-probabilistic) transition systems and later on Markov chains with labels. For a secret predicate, given as a subset of runs, and a function describing the view of an external observer, the value of interest for opacity is a measure of the set of runs disclosing the secret. We extend this definition to the richer framework of Markov decision processes, where non-deterministic choice is combined with probabilistic transitions, and we study related decidability problems with partial or complete observation hypotheses for the schedulers. We prove that all questions are decidable with complete observation and ω-regular secrets. With partial observation, we prove that all quantitative questions are undecidable but the question whether a system is almost surely non-opaque becomes decidable for a restricted class of ω-regular secrets, as well as for all ω-regular secrets under finite-memory schedulers.
• Probabilistic Disclosure: Maximisation vs. Minimisation
  Béatrice Bérard, Serge Haddad, Engel Lefaucheux · 37th IARCS Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017), LIPIcs vol. 93, pp. 13:1–13:14 · doi.org/10.4230/LIPIcs.FSTTCS.2017.13 · hal-01618955
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  We consider opacity questions where an observation function provides to an external attacker a view of the states along executions and secret executions are those visiting some state from a fixed subset. Disclosure occurs when the observer can deduce from a finite observation that the execution is secret, the ε-disclosure variant corresponding to the execution being secret with probability greater than 1 − ε. In a probabilistic and nondeterministic setting, where an internal agent can choose between actions, there are two points of view, depending on the status of this agent: the successive choices can either help the attacker trying to disclose the secret, if the system has been corrupted, or they can prevent disclosure as much as possible if these choices are part of the system design. In the former situation, corresponding to a worst case, the disclosure value is the supremum over the strategies of the probability to disclose the secret (maximisation), whereas in the latter case, the disclosure is the infimum (minimisation). We address quantitative problems (comparing the optimal value with a threshold) and qualitative ones (when the threshold is zero or one) related to both forms of disclosure for a fixed or finite horizon. For all problems, we characterise their decidability status and their complexity. We discover a surprising asymmetry: on the one hand optimal strategies may be chosen among deterministic ones in maximisation problems, while it is not the case for minimisation. On the other hand, for the questions addressed here, more minimisation problems than maximisation ones are decidable.
• Parameter and Insertion Function Co-synthesis for Opacity Enhancement in Parametric Stochastic Discrete Event Systems
  Bo Wu, Zhiyu Liu, Hai Lin · 2018 Annual American Control Conference (ACC), pp. 3032–3037, 2018 · doi.org/10.23919/ACC.2018.8430763
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  Opacity is a property that characterizes the system's capability to keep its “secret” from being inferred by an intruder that partially observes the system's behavior. In this paper, we are concerned with enhancing the opacity using insertion functions, while at the same time, enforcing the task specification in a parametric stochastic discrete event system. We first obtain the parametric Markov decision process that encodes all the possible insertions. Based on which, we convert this parameter and insertion function co-synthesis problem into a nonlinear program such that the security and the task specification can be simultaneously guaranteed.
• Privacy-Preserving POMDP Planning via Belief Manipulation
  Wei Zheng, Taeho Jung, Hai Lin · IEEE Control Systems Letters, 6, pp. 3415–3420, 2022 · doi.org/10.1109/LCSYS.2022.3185186
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  The privacy issue has become one of the most critical concerns in cyber-physical systems (CPSs) as CPSs are vulnerable to information leakage. In particular, a passive intruder could infer the secret information of the system through observations, and the system may be critically compromised or damaged once the intruder has high confidence on certain secret states. In this letter, we investigate the planning problem of a stochastic system in the presence of a passive eavesdropping intruder. In this system, the planner is modeled as a Markov decision process (MDP) who can access the state information and control the system transition. The intruder, who has a partial observation of the system state, is modeled as a hidden Markov model. The goal of the intruder is to infer the secrets of the system in terms of whether the current system is in some sensitive states, and the goal of the defender is to maximize the reward while preventing the intruder from inferring the secret. Distinct from existing work that embedded privacy as a part of the reward or utility function, we quantify privacy as a constraint for the planning. The problem is formulated as a constrained partially observable MDP (POMDP) planning problem and a belief state partition approach is proposed to solve the privacy-preserving planning problem via value iteration. Our observation is that the defender could prevent the intruder from inferring sensitive information via belief manipulation. However, the introduction of the privacy concern may sacrifice the system performance or even cause the problem to be infeasible. A necessary and sufficient condition is given to check the feasibility of the planning problem and examples are shown to illustrate our proposed algorithm.
• Opacity-Enforcing Active Perception and Control Against Eavesdropping Attacks
  Sumukha Udupa, Hazhar Rahmani, Jie Fu · 14th Conference on Decision and Game Theory for Security (GameSec 2023), Springer, pp. 329–348 · doi.org/10.1007/978-3-031-50670-3_17
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  In this paper, we consider opacity-enforcing planning with temporally-extended goals in partially observable stochastic environment. We consider a probabilistic environment modeled as partially observable Markov decision process (POMDP) in which the observation function is actively controlled as the agent decides which sensors to query at each decision step. The agent’s objective is to achieve a temporal objective, expressed using linear temporal logic for finite traces (LTL), while making achieving its goal opaque to a passive observer who can access the sensor readings of a subset of sensors that are unsecured. Opacity, as a security property, means that when from the observer’s perspective, the execution that satisfied the temporal goal is observational-equivalent to an execution that does not satisfy the temporal goal. When both secured and unsecured sensors are available upon query, the agent must be selective in its sensor query to prevent information leaking to the observer and to ensure task completion. We propose an algorithm that synthesizes a strategy that decides jointly the control actions and sensor queries to guarantee that the temporal goal is achieved and made opaque with probability 1. Our approach is based on planning with augmented belief state space. Further, we show how to employ properties in the temporal logic formula to reduce the size of the planning state space and improve scalability. We show the applicability of our algorithm on a case study with robotic planning in a stochastic gridworld with partial observations.
• Security-Aware Reinforcement Learning Under Linear Temporal Logic Specifications
  Bohan Cui, Keyi Zhu, Shaoyuan Li, Xiang Yin · 2023 IEEE International Conference on Robotics and Automation (ICRA), pp. 12367–12373 · doi.org/10.1109/ICRA48891.2023.10160753
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  In this paper, we investigate the problem of reinforcement learning under linear temporal logic (LTL) specifications for Markov decision processes (MDPs) with security constraints. We consider an outside passive intruder (observer) that can observe the external output behavior of the system through an output projection. We assume that the secret of the system is a subset of the initial states. The security constraint requires that the observer can never infer for sure that the agent was initiated from a secret state. Our objective is to learn a control policy that achieves the LTL task while ensuring security. To solve the problem of shaping the reward for reinforcement learning, we propose an approach based on the initial-state estimator and the limit deterministic Büchi automata. We illustrate the proposed approach by a case study of mobile robot example.
• Information-Theoretic Opacity-Enforcement in Markov Decision Processes
  Chongyang Shi, Yuheng Bu, Jie Fu · Proceedings of the 33rd International Joint Conference on Artificial Intelligence (IJCAI 2024), pp. 6779–6787 · doi.org/10.24963/ijcai.2024/749
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  The paper studies information-theoretic opacity, an information-flow privacy property, in a setting involving two agents: A planning agent who controls a stochastic system and an observer who partially observes the system states. The goal of the observer is to infer some secret, represented by a random variable, from its partial observations, while the goal of the planning agent is to make the secret maximally opaque to the observer while achieving a satisfactory total return. Modeling the stochastic system using a Markov decision process, two classes of opacity properties are considered---Last-state opacity is to ensure that the observer is uncertain if the last state is in a specific set and initial-state opacity is to ensure that the observer is unsure of the realization of the initial state. As the measure of opacity, we employ the Shannon conditional entropy capturing the information about the secret revealed by the observable. Then, we develop primal-dual policy gradient methods for opacity-enforcement planning subject to constraints on total returns. We propose novel algorithms to compute the policy gradient of entropy for each observation, leveraging message passing within the hidden Markov models. This gradient computation enables us to have stable and fast convergence. We demonstrate our solution of opacity-enforcement control through a grid world example.
• Planning with Probabilistic Opacity and Transparency: A Computational Model of Opaque/Transparent Observations
  Sumukha Udupa, Jie Fu · 2024 IEEE 63rd Conference on Decision and Control (CDC), pp. 477–484, 2024 · doi.org/10.1109/CDC56724.2024.10886248
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  The qualitative opacity of a secret is a security property, which means that a system trajectory satisfying the secret is observation-equivalent to a trajectory violating the secret. In this paper, we study how to synthesize a control policy that maximizes the probability of a secret being made opaque against an eavesdropping attacker/observer, while subject to other task performance constraints. In contrast to the existing belief-based approach for opacity-enforcement, we develop an approach that uses the observation function, the secret, and the model of the dynamical systems to construct a so-called opaqueobservations automaton that accepts the exact set of observations that enforce opacity. Leveraging this opaque-observations automaton, we can reduce the optimal planning in Markov decision processes(MDPs) for maximizing probabilistic opacity or its dual notion, transparency, subject to task constraints into a constrained planning problem over an augmented-state MDP. Finally, we illustrate the effectiveness of the developed methods in robot motion planning problems with opacity or transparency requirements.
• Policy Gradient Methods for Information-Theoretic Opacity in Markov Decision Processes
  Chongyang Shi, Sumukha Udupa, Michael R. Dorothy, Shuo Han, Jie Fu · arXiv:2511.02704, 2025 · arXiv:2511.02704
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  Opacity, or non-interference, is a property ensuring that an external observer cannot infer confidential information (the "secret") from system observations. We introduce an information-theoretic measure of opacity, which quantifies information leakage using the conditional entropy of the secret given the observer's partial observations in a system modeled as a Markov decision process (MDP). Our objective is to find a control policy that maximizes opacity while satisfying task performance constraints, assuming that an informed observer is aware of the control policy and system dynamics. Specifically, we consider a class of opacity called state-based opacity, where the secret is a propositional formula about the past or current state of the system, and a special case of state-based opacity called language-based opacity, where the secret is defined by a temporal logic formula (LTL) or a regular language recognized by a finite-state automaton. First, we prove that finite-memory policies can outperform Markov policies in optimizing information-theoretic opacity. Second, we develop an algorithm to compute a maximally opaque Markov policy using a primal-dual gradient-based algorithm, and prove its convergence. Since opacity cannot be expressed as a cumulative cost, we develop a novel method to compute the gradient of conditional entropy with respect to policy parameters using observable operators in hidden Markov models. The experimental results validate the effectiveness and optimality of our proposed methods.
• Synthesis of Dynamic Masks for Information-Theoretic Opacity in Stochastic Systems
  Sumukha Udupa, Chongyang Shi, Jie Fu · ACM/IEEE 16th International Conference on Cyber-Physical Systems (ICCPS 2025), pp. 1–12 · doi.org/10.1145/3716550.3722036
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  In this work, we investigate the synthesis of dynamic information releasing mechanisms, referred to as "masks", to minimize information leakage from a stochastic system to an external observer. Specifically, for a stochastic system, an observer aims to infer whether the final state of the system trajectory belongs to a set of secret states. The dynamic mask seeks to regulate sensor information in order to maximize the observer's uncertainty about the final state, a property known as final-state opacity. While existing supervisory control literature on dynamic masks primarily addresses qualitative opacity, we propose quantifying opacity in stochastic systems by conditional entropy, which is a measure of information leakage in information security. We then formulate a constrained optimization problem to synthesize a dynamic mask that maximizes final-state opacity under a total cost constraint on masking. To solve this constrained optimal dynamic mask synthesis problem, we develop a novel primal-dual policy gradient method. Additionally, we present a technique for computing the gradient of conditional entropy with respect to the masking policy parameters, leveraging observable operators in hidden Markov models. To demonstrate the effectiveness of our approach, we apply our method to an illustrative example and a stochastic grid world scenario, showing how our algorithm optimally enforces final-state opacity under cost constraints.
• Almost k-Step Opacity Enforcement in Stochastic Discrete-Event Systems via Differential Privacy
  Rong Zhao, Murat Uzam, Zhiwu Li · Mathematics, 13(8), article 1255, 2025 · doi.org/10.3390/math13081255
  enforcement · mdp · opacity · stochastic
  Show abstractHide abstract

  This paper delves into current-state opacity enforcement in partially observed discrete event systems through an innovative application of differential privacy, which is fundamental for security-critical cyber–physical systems. An opaque system implies that an external agent cannot infer the predefined system secret via its observational output, such that the important system information flow cannot be leaked out. Differential privacy emerges as a robust framework that is pivotal for the protection of individual data integrity within these systems. Motivated by the differential privacy mechanism for information protection, this research proposes the secret string adjacency relation as a novel concept, assessing the similarity between potentially compromised strings and system-generated alternatives, thereby shielding the system’s confidential data from external observation. The development of secret string differential privacy is achieved by substituting sensitive strings. These substitution strings are generated by a modified Levenshtein automaton, following exponentially distributed generation probabilities. The verification and illustrative examples of the proposed mechanism are provided.

Where probabilistic opacity gets applied to a concrete domain, beyond toy or illustrative examples.

• Probabilistic Opacity for a Passive Adversary and Its Application to Chaum's Voting Scheme
  Yassine Lakhnech, Laurent Mazaré · IACR Cryptology ePrint Archive, 2005, article 98 · IACR ePrint 2005/098
  applications · opacity · stochastic
  Show abstractHide abstract

  A predicate is opaque for a given system, if an adversary will never be able to establish truth or falsehood of the predicate for any observed computation. This notion has been essentially introduced and studied in the context of transition systems whether describing the semantics of programs, security protocols or other systems. In this paper, we are interested in studying opacity in the probabilistic computational world. Indeed, in other settings, as in the Dolev-Yao model for instance, even if an adversary is 99% sure of the truth of the predicate, it remains opaque as the adversary cannot conclude for sure. In this paper, we introduce a computational version of opacity in the case of passive adversaries called cryptographic opacity. Our main result is a composition theorem: if a system is secure in an abstract formalism and the cryptographic primitives used to implement it are secure, then this system is secure in a computational formalism. Security of the abstract system is the usual opacity and security of the cryptographic primitives is IND-CPA security. To illustrate our result, we give two applications: a short and elegant proof of the classical Abadi-Rogaway result and the first computational proof of Chaum’s visual electronic voting scheme.
• Quantitative Analysis of Opacity in Cloud Computing Systems
  Wen Zeng, Maciej Koutny · IEEE Transactions on Cloud Computing, 9(3), pp. 1210–1219, 2019 · doi.org/10.1109/TCC.2019.2894768
  applications · opacity · stochastic
  Show abstractHide abstract

  Federated cloud systems increase the reliability and reduce the cost of the computational support. The resulting combination of secure private clouds and less secure public clouds, together with the fact that resources need to be located within different clouds, strongly affects the information flow security of the entire system. In this paper, the clouds as well as entities of a federated cloud system are assigned security levels, and a probabilistic flow sensitive security model for a federated cloud system is proposed. Then the notion of opacity—a notion capturing the security of information flow—of a cloud computing systems is introduced, and different variants of quantitative analysis of opacity are presented. As a result, one can track the information flow in a cloud system, and analyze the impact of different resource allocation strategies by quantifying the corresponding opacity characteristics.