The recent development in communication networks and computational devices has greatly enhanced the technological evolution of Cyber-Physical Systems (CPSs), such as networked mobile robots, autonomous vehicles, intelligent transportation systems, smart manufacturing systems, and other classes of systems that have a large degree of autonomy. The physical components in these systems are monitored and controlled by embedded (cyber) subsystems that exchange vital and confidential information over their communication networks. These subsystems often interact with an external environment that is uncertain, dynamic, and sometimes even malicious. Operating in such an environment therefore demands correct-by-design methodologies that reliably enforce a required property and preserve security requirements of these systems.
Furthermore, the operations of many modern CPSs, ranging from intelligent manufacturing systems to transportation networks, are governed by the sequential execution of certain control actions that show the largely event-driven nature of these systems. This inspires this dissertation to focus on the cyber behavior of CPSs in the framework of discrete event systems (DESs), as this class of dynamic systems provides suitable formal models and analytical techniques to study event-driven systems. In this dissertation, we tackle two classes of problems: control of DESs in the presence of dynamic environments, and security enforcement and analysis of these systems under attack of malicious environments.
To study the behavior of a DES operating in a dynamic environment, we propose a novel DES model, namely open DES, that captures the internal model of a system and its interactions with an external dynamic environment. With this model, we are able to characterize the uncontrollable behavior of a DES that is imposed by its internal dynamic and the external environment inputs. Due to the unpredictability of the external environment, an open DES should be controlled in such a way that a desired property is guaranteed for any possible environment. For this problem, a game-theoretic approach is designed to compute a reactive supervisor that controls the system to fulfill the specifications regardless of the environment behaviors. We present necessary and sufficient conditions for the existence of such a reactive supervisor.
Apart from the reactive control of open DESs in the presence of dynamic environments, we investigate the security of these systems under the attack of a malicious environment, termed active intruder, who is able to strategically manipulate the system behavior to infer its confidential information. This security problem is formulated in terms of opacity. For this configuration, we present a new notion of opacity, namely reactive opacity, characterizing a property that the system does not leak it’s secret information regardless of how the intruder manipulates the system behavior. We provide an algorithm for verifying this opacity notion and, furthermore, consider enforcement of this property based on dynamic masking techniques.
Along with the reactive opacity notion, we study the opacity problem of probabilistic DES in the presence of an active intruder. We propose a qualitative reactive opacity notion that captures the accumulated probability that the intruder can force the system to expose its secret, termed reactive opacity level. A formal verification algorithm is provided to check if a given probabilistic DES satisfies the desired reactive opacity level. To enhance the system reactive opacity level, we propose to design an obfuscation function that dynamically changes the probability distribution of the system output to deceive the intruder inference model. We then show that the design of such an obfuscation function can be converted to a two-player stochastic game between the active intruder and the obfuscation function. Finally, we turn our focus to applications of opacity in real-word CPSs. We study the privacy problem of location-based services in the probabilistic DES formalism. We characterize a user mobility model by a Markov decision process (MDP) and use the opacity notion to measure the user location privacy under an attack model of a passive Bayesian intruder. We then exploit the MDP model to design a location protection mechanism that guarantees a user-specified privacy level.