A framework for current-state opacity under dynamic information release mechanism
From MaRDI portal
Abstract: Opacity is an important information-flow security property that characterizes the plausible deniability of a dynamic system for its "secret" against eavesdropping attacks. As an information-flow property, the underlying observation model is the key in the modeling and analysis of opacity. In this paper, we investigate the verification of current-state opacity for discrete-event systems under Orwellian-type observations, i.e., the system is allowed to re-interpret the observation of an event based on its future suffix. First, we propose a new Orwellian-type observation model called the dynamic information release mechanism (DIRM). In the DIRM, when to release previous "hold on" events is state-dependent. Then we propose a new definition of opacity based on the notion of history-equivalence rather than the standard projection-equivalence. This definition is more suitable for observations that are not prefix-closed. Finally, we show that by constructing a new structure called the DIRM-observer, current-state opacity can be effectively verified under the DIRM. Computational complexity analysis as well as illustrative examples for the proposed approach are also provided. Compared with the existing Orwellian-type observation model, the proposed framework is more general in the sense that the information-release-mechanism is state-dependent and the corresponding definition of opacity is more suitable for non-prefix-closed observations.
Recommendations
- Strong current-state and initial-state opacity of discrete-event systems
- Comparing the notions of opacity for discrete-event systems
- A general language-based framework for specifying and verifying notions of opacity
- Verification and enforcement of current-state opacity based on a state space approach
- Active opacity of discrete-event systems
Cites work
- A general approach for optimizing dynamic sensor activation for discrete event systems
- A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers
- Active acquisition of information for diagnosis and supervisory control of discrete event systems
- Characterizing intransitive noninterference for 3-domain security policies with observability
- Comparative analysis of related notions of opacity in centralized and coordinated architectures
- Compositional and Abstraction-Based Approach for Synthesis of Edit Functions for Opacity Enforcement
- Current-state opacity modelling and verification in partially observed Petri nets
- Enforcement and validation (at runtime) of various notions of opacity
- Estimation and inference in discrete event systems. A model-based approach with finite automata
- Infinite-step opacity and K-step opacity of stochastic discrete-event systems
- Introduction to Discrete Event Systems
- Modelling opacity using Petri nets
- Notions of Centralized and Decentralized Opacity in Linear Systems
- On Approximate Opacity of Cyber-Physical Systems
- Opacity Enforcement for Confidential Robust Control in Linear Cyber-Physical Systems
- Opacity of discrete event systems and its applications
- Optimal sensor activation for diagnosing discrete event systems
- Supervisory Control for Opacity
- Synthesis of Dynamic Masks for Infinite-Step Opacity
- Synthesis of opaque systems with static and dynamic masks
- Transforming Opacity Verification to Nonblocking Verification in Modular Systems
- Verification of Infinite-Step Opacity and Complexity Considerations
- Verification of State-Based Opacity Using Petri Nets
- Verification of initial-state opacity in security applications of discrete event systems
- \(k\)-memory-embedded insertion mechanism for opacity enforcement
Cited in
(5)- A two-pronged approach to security of discrete-event systems
- Opacity of discrete-event systems under nondeterministic observation mechanism
- Optimal control strategy for k-level opaque systems based on the optimization method of multi-selection problems at each stage
- New insights into opacity verification in timed discrete-event systems
- A general language-based framework for specifying and verifying notions of opacity
This page was built for publication: A framework for current-state opacity under dynamic information release mechanism
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2125535)
