Current-State opacity based on state outputs: definition and verification

Abstract Cyber-physical systems (CPSs) are formed of physical and computational components that interact to operate a process safely and efficiently according to the desired behavior. To do so, the plant is continuously monitored, and the information obtained from its components is transmitted to computer-based devices. The connection between the plant and the monitoring and control device is carried out using communication networks, which may be susceptible to cyber-attacks. In this paper, we consider that the communication channel used to transmit data from the plant to the monitoring and control device is vulnerable to attacks, and that the attacker eavesdrops on the communication channel to gather sensitive information and discover if the system has reached a secret state. Since we assume that the information transmitted in the network is the status of system components, such as sensors, actuators, and memory variables of local controllers, the system can be modeled, from the attacker’s perspective, as a finite state transducer, where each state of the model is associated with an output vector formed of the signals associated with the system components. Considering that the attacker has full knowledge of the system model and does not know the current state of the system when he/she initiates to eavesdrop on the communication channel, the attacker tries to estimate the current state of the system by observing the state outputs transmitted in the network. Therefore, in this case, it is necessary to verify whether the attacker is never able to detect the secret states of the system. In the Discrete-Event System literature, the system property associated with the intruder’s inability to discover the system secret based on the transmitted information is called opacity. Since, in this paper, the attacker observes state outputs of a finite state transducer instead of events, we introduce a new notion of opacity called Current-State Opacity based on State Outputs (CSO-SO). We also present a method for the verification of CSO-SO. In addition, a comparison between the definition of current-state opacity based on event observations and CSO-SO is provided. A practical system is used to illustrate the definition and verification of CSO-SO.