Search

The increasingly tight coupling of cyber (computing/communication) and physical (sensing/actuation) components has opened the door for developing many engineering systems with increasing complexity. On the one hand, these systems (commonly termed cyber-physical systems, or CPS for short) have enabled a multitude of applications where decisions are taken at various time-scales, driven by the sensory information, and are used for purposes such as automated control and adaptive interventions. On the other hand, there has been a corresponding increase in attacks targeting the integrity and security of these systems. These attacks pose a significant threat to often sensitive devices, potentially impairing our relation with these technologies. Various unique attributes of sensory information make it particularly challenging to formalize and address these concerns, and approaches thus far to handle them have been largely insufficient. The objective of this dissertation is to develop a principled understanding of these emerging concerns and develop formalisms, algorithms, and system mechanisms to effectively address them.The contributions of this dissertation are multi-fold. We start by playing the role of an adversarial attacker trying to discover new attack vectors for which traditional security mechanisms provide no defense guarantees. In particular, we focus on attacks that take place on sensors that collect information about the physical process in CPS. We show that by exploiting the weakness in securing sensor information, a malicious attacker can cause life-threatening situations which plays as a motivation for the rest of this dissertation. Next, we explore two countermeasures called sensor-level countermeasures and system-level countermeasures. In the sensor-level countermeasures, we propose a physical challenge-response authentication (PyCRA) scheme for sensors that is designed to provide an authorization mechanism that not only detects malicious attacks but provides resilience against them. The majority of this dissertation focuses on designing system-level counter measures to sensor attacks. In the system-level countermeasures, we consider the problem of designing algorithms for CPS whose sensor measurements are corrupted by a malicious attacker. The attacker capabilities are limited in the sense that only a subset of all the sensors can be attacked although this subset is unknown. In particular, we focus on the setup where all measurements from various sensors are sent to a central unit whose functionality is to fuse all these measurements in order to estimate the state of the CPS regardless of the existence of the malicious attacker. We call this problem the secure state estimation problem. We analyze sufficient and necessary conditions for the solvability of the secure state estimation problem under three different setups namely, linear deterministic systems, linear stochastic systems, and nonlinear deterministic systems. We propose the notion of s-sparse observability and show how it plays a vital role in solving the secure state estimation problem. We show that the secure state estimation problem is a combinatorial problem. The most notable contribution of this dissertation is a novel Satisfiability Modulo Theory (SMT) solver that splits the reasoning, about the combinatorial complexity of the secure state estimation problem, over Boolean and real domains and uses a powerful tool from each domain. By leveraging results from formal methods over real numbers, we provide guarantees on the soundness and completeness of our algorithm. We also extend the SMT-solver to estimate the state under sensor attacks to the context of stochastic linear dynamical system and nonlinear differentially flat systemsFinally, we touch upon the related problem of privacy attacks in cyber-physical systems. Unlike sensor attacks, privacy attacks are a form of passive attacks that target data collection that can be used to leak sensitive information. We present a novel model-based obfuscation approach with strong formal guarantees. Our approach preserves both the utility of the event trace and its spatio-temporal-plausibility while providing strong privacy guarantees.

Sensors are the means by which cyber-physical systems perceive their own state as well as the state of their environment. Any attack on sensor measurements, or their transmission, has the potential to lead to catastrophic consequences since control actions would be based on an incorrect state estimate. In this chapter, we introduce the secure state estimation problem, discuss under which conditions it can be solved, and review existing algorithms.

We consider a problem where multiple agents participate in solving a quadratic optimization problem subject to linear inequality constraints in a privacy-preserving manner. Several variables of the objective function as well as the constraints are privacy-sensitive and are known to different agents. We propose a privacy-preserving protocol based on partially homomorphic encryption where each agent encrypts its own information before sending it to an untrusted cloud computing infrastructure. To find the optimal solution the cloud applies a gradient descent algorithm on the encrypted data without the ability to decrypt it. The privacy of the proposed protocol against coalitions of colluding agents is analyzed using the cryptography notion of zero knowledge proofs.

© 1963-2012 IEEE. Secure state estimation is the problem of estimating the state of a dynamical system from a set of noisy and adversarially corrupted measurements. Intrinsically a combinatorial problem, secure state estimation has been traditionally addressed either by brute force search, suffering from scalability issues, or via convex relaxations, using algorithms that can terminate in polynomial time but are not necessarily sound. In this paper, we present a novel algorithm that uses a satisfiability modulo theory approach to harness the complexity of secure state estimation. We leverage results from formal methods over real numbers to provide guarantees on the soundness and completeness of our algorithm. Moreover, we discuss its scalability properties, by providing upper bounds on the runtime performance. Numerical simulations support our arguments by showing an order of magnitude decrease in execution time with respect to alternative techniques. Finally, the effectiveness of the proposed algorithm is demonstrated by applying it to the problem of controlling an unmanned ground vehicle.

Personalized IoT adapt their behavior based on contextual information, such as user behavior and location. Unfortunately, the fact that personalized IoT adapt to user context opens a side-channel that leaks private information about the user. To that end, we start by studying the extent to which a malicious eavesdropper can monitor the actions taken by an IoT system and extract user's private information. In particular, we show two concrete instantiations (in the context of mobile phones and smart homes) of a new category of spyware which we refer to as Context-Aware Adaptation Based Spyware (SpyCon). Experimental evaluations show that the developed SpyCon can predict users' daily behavior with an accuracy of 90.3%. Being a new spyware with no known prior signature or behavior, traditional spyware detection that is based on code signature or system behavior are not adequate to detect SpyCon. We discuss possible detection and mitigation mechanisms that can hinder the effect of SpyCon.

We propose an efficient multi-robot motion planning algorithm for missions captured by linear temporal logic (LTL) specifications, in the presence of bounded disturbances and denial-of-service (DoS) attacks against the communication between robots and base stations. Given an LTL formula Ψ, our goal is to construct robot trajectories, and associated control strategies, to satisfy Ψ and continuously establish communication paths between robots and base stations despite the DoS attacks and the disturbances on the robot states. Our approach combines and extends results from robust control and efficient motion planning via satisfiability modulo convex programming (SMC). We first compute a feedback controller that rejects the disturbance together with a perturbation of the DoS-free workspace that accounts for the worst-case disturbance scenario. On the perturbed workspace, we formulate the planning problem as a feasibility problem over Boolean and convex constraints, respectively capturing the DoS-resilient mission constraints and the constraints on the nominal, disturbance-free, robot dynamics. Numerical results show the effectiveness of our algorithm in providing DoS-resilient plans that are robust to disturbances and support the execution of complex missions.

In this paper, we consider the problem of automatically designing a Rectified Linear Unit (ReLU) Neural Network (NN) architecture that is sufficient to implement the optimal Model Predictive Control (MPC) strategy for an LTI system with quadratic cost. Specifically, we propose AReN, an algorithm to generate Assured ReLU Architectures. AReN takes as input an LTI system with quadratic cost specification, and outputs a ReLU NN architecture with the assurance that there exist network weights that exactly implement the associated MPC controller. AReN thus offers new insight into the design of ReLU NN architectures for the control of LTI systems: instead of training a heuristically chosen NN architecture on data -- or iterating over many architectures until a suitable one is found -- AReN can suggest an adequate NN architecture before training begins. While several previous works were inspired by the fact that both ReLU NN controllers and optimal MPC controller are both Continuous, Piecewise-Linear (CPWL) functions, exploiting this similarity to design NN architectures with correctness guarantees has remained elusive. AReN achieves this using two novel features. First, we reinterpret a recent result about the implementation of CPWL functions via ReLU NNs to show that a CPWL function may be implemented by a ReLU architecture that is determined by the number of distinct affine regions in the function. Second, we show that we can efficiently over-approximate the number of affine regions in the optimal MPC controller without solving the MPC problem exactly. Together, these results connect the MPC problem to a ReLU NN implementation without explicitly solving the MPC and directly translates this feature to a ReLU NN architecture that comes with the assurance that it can implement the MPC controller. We show through numerical results the effectiveness of AReN in designing an NN architecture.

The recent developments in the automobile industry and the self-driving technology necessitated an increase in the traditional automobile features to guarantee the drivers safety, improve the driving convenience and realize the autonomous driving. To support these necessary functions and features, a significant amount of the hardware equipment, i.e., Electronic Control Unit (ECU), is integrated into the car system. However, these ECUs also bring security vulnerabilities because their communication follows the Controller Area Network (CAN) protocol that was designed without supporting message origin authentication. Several methods to resolve this problem have been proposed in the literature, but most of them would require heavy communications and calculations to support the cryptography algorithms. In this paper, we propose a delay-based Intrusion Detection System (IDS) to protect the CAN network by identifying the location of the compromised ECU for the in-vehicle network. We develop and implement our detection method on CAN bus prototype, and our results show that our method is capable of an overall detection accuracy above 97%. The proposed scheme is demonstrated to protect the integrity of the messages on CAN bus leading to a further improve the security and safety of autonomous vehicles.

The development of large-scale distributed control systems has led to the outsourcing of costly computations to cloud-computing platforms, as well as to concerns about privacy of the collected sensitive data. This paper develops a cloud-based protocol for a quadratic optimization problem involving multiple parties, each holding information it seeks to maintain private. The protocol is based on the projected gradient ascent on the Lagrange dual problem and exploits partially homomorphic encryption and secure multi-party computation techniques. Using formal cryptographic definitions of indistinguishability, the protocol is shown to achieve computational privacy, i.e., there is no computationally efficient algorithm that any involved party can employ to obtain private information beyond what can be inferred from the party's inputs and outputs only. In order to reduce the communication complexity of the proposed protocol, we introduced a variant that achieves this objective at the expense of weaker privacy guarantees. We discuss in detail the computational and communication complexity properties of both algorithms theoretically and also through implementations. We conclude the paper with a discussion on computational privacy and other notions of privacy such as the non-unique retrieval of the private information from the protocol outputs.