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 secret behaviors in the future. Existing works on pre-opacity only consider non-metric discrete systems, where it is assumed that intruders can distinguish different output behaviors precisely. However, for continuous-space control systems whose output sets are equipped with metrics (which is the case for most real-world applications), it is too restrictive to assume precise measurements from outside observers. In this paper, we first introduce a concept of approximate pre-opacity by capturing the security level of control systems with respect to the measurement precision of the intruder. Based on this new notion of pre-opacity, we propose a verification approach for continuous-space control systems by leveraging abstraction-based techniques. In particular, a new concept of approximate pre-opacity preserving simulation relation is introduced to characterize the distance between two systems in terms of preserving pre-opacity. This new system relation allows us to verify pre-opacity of complex continuous-space control systems using their finite abstractions. We also present a method to construct pre-opacity preserving finite abstractions for a class of discrete-time control systems under certain stability assumptions.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
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 …
RelationCompositional 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…
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…
Local Opacity Verification for Distributed Discrete Event Systems
This paper studies current-state opacity and initial-state opacity verification of distributed discrete event systems. The distributed system's global model is the parallel composition of multiple local systems: each of …
Verification of Neural Network Control Systems in Continuous Time
Neural network controllers are currently being proposed for use in many safety-critical tasks. Most analysis methods for neural network control systems assume a fixed control period. In control theory, higher frequency u…