Biblio

This paper investigates the problem of synthesizing sensor deception attackers against privacy in the context of supervisory control of discrete-event systems (DES). We consider a plant controlled by a supervisor, which is subject to sensor deception attacks. Specifically, we consider an active attacker that can tamper with the observations received by the supervisor. The privacy requirement of the supervisory control system is to maintain initial-state opacity, i.e., it does not want to reveal the fact that it was initiated from a secret state during its operation. On the other hand, the attacker aims to deceive the supervisor, by tampering with its observations, such that initial-state opacity is violated due to incorrect control actions. We investigate from the attacker’s point of view by presenting an effective approach for synthesizing sensor attack strategies threatening the privacy of the system. To this end, we propose the All Attack Structure (AAS) that records state estimates for both the supervisor and the attacker. This structure serves as a basis for synthesizing a sensor attack strategy. We also discuss how to simplify the synthesis complexity by leveraging the structural properties. A running academic example is provided to illustrate the synthesis procedure.

This paper presents a method to improve the diagnosability of power network under multiple faults. In this paper, the steps of fault diagnosis are as follows: first, constructing finite automata model of the diagnostic system; then, a fault diagnoser model is established through coupling operation and trajectory reasoning mechanism; finally, the diagnosis results are obtained through this model. In this paper, the judgment basis of diagnosability is defined. Then, based on the existing diagnosis results, the information available can be increased by adding sensor devices, to achieve the purpose of diagnosability in the case of multiple faults of the system.

In this paper, we investigate joint sensor-actuator cyber attacks in discrete event systems. We assume that attackers can attack some sensors and actuators at the same time by altering observations and control commands. Because of the nondeterminism in observation and control caused by cyber attacks, the behavior of the supervised systems becomes nondeterministic and deviates from the target. We define two bounds on languages, an upper-bound and a lower-bound, to describe the nondeterministic behavior. We then use the upper-bound language to investigate the safety supervisory control problem under cyber attacks. After introducing CA-controllability and CA-observability, we successfully solve the supervisory control problem under cyber attacks.

Supervisor synthesis enables the design of supervisory controllers for large cyber-physical systems, with high guarantees for functionality and safety. The complexity of the synthesis problem, however, increases exponentially with the number of system components in the cyber-physical system and the number of models of this system, often resulting in lengthy or even unsolvable synthesis procedures. In this paper, a new method is proposed for reducing the model of the system before synthesis to decrease the required computational time and effort. The method consists of three steps for model reduction, that are mainly based on symmetry in dependency graphs of the system. Dependency graphs visualize the components in the system and the relations between these components. The proposed method is applied in a case study on the design of a supervisory controller for a road tunnel. In this case study, the model reduction steps are described, and results are shown on the effectiveness of model reduction in terms of model size and synthesis time.

In a diagnosability verifier with polynomial complexity, a non-diagnosable system generates uncertain loops. Such forbidden loops are in this paper transformed to forbidden states by simple detector automata. The forbidden state problem is trivially transformed to a nonblocking problem by considering all states except the forbidden ones as marked states. This transformation is combined with one of the most efficient abstractions for modular systems called conflict equivalence, where nonblocking properties are preserved. In the resulting abstraction, local events are hidden and more local events are achieved when subsystems are synchronized. This incremental abstraction is applied to a scalable production system, including parallel lines where buffers and machines in each line include some typical failures and feedback flows. For this modular system, the proposed diagnosability algorithm shows great results, where diagnosability of systems including millions of states is analyzed in less than a second.

In this paper, we propose and address the problem of supervisor obfuscation against actuator enablement attack, in a common setting where the actuator attacker can eavesdrop the control commands issued by the supervisor. We propose a method to obfuscate an (insecure) supervisor to make it resilient against actuator enablement attack in such a way that the behavior of the original closed-loop system is preserved. An additional feature of the obfuscated supervisor, if it exists, is that it has exactly the minimum number of states among the set of all the resilient and behavior-preserving supervisors. Our approach involves a simple combination of two basic ideas: 1) a formulation of the problem of computing behavior-preserving supervisors as the problem of computing separating finite state automata under controllability and observability constraints, which can be tackled by using SAT solvers, and 2) the use of a recently proposed technique for the verification of attackability in our setting, with a normality assumption imposed on both the actuator attackers and supervisors.

In this paper, we propose and develop an actuator attack model for discrete-event systems. We assume the actuator attacker partially observes the execution of the closed-loop system and eavesdrops the control commands issued by the supervisor. The attacker can modify each control command on a specified subset of attackable events. The goal of the actuator attacker is to remain covert until it can establish a successful attack and lead the attacked closed-loop system into generating certain damaging strings. We then present a characterization for the existence of a successful attacker and prove the existence of the supremal successful attacker, when both the supervisor and the attacker are normal. Finally, we present an algorithm to synthesize the supremal successful normal attackers.