On Approximate Opacity of Stochastic Control Systems
This paper investigates an important class of information-flow security property called opacity for stochastic control systems. Opacity captures whether a system's secret behavior (a subset of the system's behavior that is considered to be critical) can be kept from outside observers. Existing works on opacity for control systems only provide a binary characterization of the system's security level by determining whether the system is opaque or not. In this work, we introduce a quantifiable measure of opacity that considers the likelihood of satisfying opacity for stochastic control systems modeled as general Markov decision processes (gMDPs). We also propose verification methods tailored to the new notions of opacity for finite gMDPs by using value iteration techniques. Then, a new notion called approximate opacity-preserving stochastic simulation relation is proposed, which captures the distance between two systems' behaviors in terms of preserving opacity. Based on this new system relation, we show that one can verify opacity for stochastic control systems using their abstractions (modeled as finite gMDPs). We also discuss how to construct such abstractions for a class of gMDPs under certain stability conditions.
Code (0)
등록된 구현이 없습니다.
Tasks
RelationSimilar Papers 제목 키워드 기반
Abstraction-Based Verification of Approximate Pre-Opacity for Control Systems
In this paper, we consider the problem of verifying pre-opacity for discrete-time control systems. Pre-opacity is an important information-flow security property that secures the intention of a system to execute some sec…
Synthesis of Dynamic Masks for Information-Theoretic Opacity in Stochastic Systems
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 stoc…
Verification of Initial-State Opacity for Switched Systems: A Compositional Approach
The security in information-flow has become a major concern for cyber-physical systems (CPSs). In this work, we focus on the analysis of an information-flow security property, called opacity. Opacity characterizes the pl…
Compositional Verification of Initial-State Opacity for Switched Systems
In this work, we propose a compositional framework for the verification of approximate initial-state opacity for networks of discrete-time switched systems. The proposed approach is based on a notion of approximate initi…
Information-Theoretic Opacity-Enforcement in Markov Decision Processes
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 syste…
Policy Gradient Methods