Search

Accurate localization from Cyber-Physical Systems (CPS) is a critical enabling technology for context-aware applications and control. As localization plays an increasingly safety-critical role, location systems must be able to identify and eliminate faulty measurements to prevent dangerously inaccurate localization. In this article, we consider the range-based localization problem and propose a method to detect coordinated adversarial corruption on anchor positions and distance measurements. Our algorithm, G ordian , rapidly finds attacks by identifying geometric inconsistencies at the graph level without requiring assumptions about hardware, ranging mechanisms, or cryptographic protocols. We give necessary conditions for which attack detection is guaranteed to be successful in the noiseless case, and we use that intuition to extend G ordian to the noisy case where fewer guarantees are possible. In simulations generated from real-world sensor noise, we empirically show that G ordian ’s trilateration counterexample generation procedure enables rapid attack detection even for combinatorially difficult problems.

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.

We consider the problem of estimating the state of a noisy linear dynamical system when an unknown subset of sensors is arbitrarily corrupted by an adversary. We propose a secure state estimation algorithm, and derive (optimal) bounds on the achievable state estimation error given an upper bound on the number of attacked sensors. The proposed state estimator involves Kalman filters operating over subsets of sensors to search for a sensor subset which is reliable for state estimation. To further improve the subset search time, we propose Satisfiability Modulo Theory based techniques to exploit the combinatorial nature of searching over sensor subsets. Finally, as a result of independent interest, we give a coding theoretic view of attack detection and state estimation against sensor attacks in a noiseless dynamical system., Submitted to IEEE TCNS special issue on secure control of cyber physical systems. A preliminary version of this work appeared in the proceedings of ISIT 2015. arXiv admin note: text overlap with arXiv:1504.05566

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.

This paper describes two algorithms for state reconstruction from sensor measurements that are corrupted with sparse, but otherwise arbitrary, "noise". These results are motivated by the need to secure cyber-physical systems against a malicious adversary that can arbitrarily corrupt sensor measurements. The first algorithm reconstructs the state from a batch of sensor measurements while the second algorithm is able to incorporate new measurements as they become available, in the spirit of a Luenberger observer. A distinguishing point of these algorithms is the use of event-triggered techniques to improve the computational performance of the proposed algorithms., 30 pages, 3 figures

This paper discusses the problem of reconstructing the state of a linear time invariant system when some of its actuators and sensors are compromised by an adversarial agent. In the model considered in this paper, the adversarial agent attacks an input (output) by manipulating its value arbitrarily, i.e., we impose no constraints (statistical or otherwise) on how control commands (sensor measurements) are changed by the adversary other than a bound on the number of attacked actuators and sensors In the first part of this paper, we introduce the notion of sparse strong observability and we show that is a necessary and sufficient condition for correctly reconstructing the state despite the considered attacks. In the second half of this work, we propose an observer to harness the complexity of this intrinsically combinatorial problem, by leveraging satisfiability modulo theory solving. Numerical simulations illustrate the effectiveness and scalability of our observer.

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.

IoT devices are permeating every corner of our lives today paving the road for more substantial smart systems. Despite their ability to collect and analyze a significant amount of sensory data, traditional IoT typically depends on fixed policies and schedules to enhance user experience. However, fixed policies that do not account for variations in human mood, reactions, and expectations, fail to achieve the promised user experience. In this paper, we propose an architecture for personalized and autonomous IoT systems that weaves personalization and context-awareness into the very fabric of smart systems. By building upon ideas from reinforcement learning, we show---using an example of smart and personalized home services---how the proposed architecture can adapt to human behaviors that are varying between individuals and vary, for the same individual, across time while addressing some of the security and privacy challenges.

The design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of 'cyber' components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step in our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming.

This paper surveys recent challenges and solutions in the design, implementation, and verification of embedded software for robotics. Emphasis is placed on mobile robots, like self-driving cars. In design, it addresses programming support for robotic systems, secure state estimation, and ROS-based monitor generation. In the implementation phase, it describes the synthesis of control software using finite precision arithmetic, real-time platforms and architectures for safety-critical robotics, efficient implementation of neural network based-controllers, and standards for computer vision applications. The issues in verification include verification of neural network-based robotic controllers, and falsification of closed-loop control systems. The paper also describes notable open-source robotic platforms. Along the way, we highlight important research problems for developing the next generation of high-performance, low-resource-usage, correct embedded software.

We study a crowdsourcing aided road traffic estimation setup, where a fraction of users (vehicles) are malicious, and report wrong sensory information, or even worse, report the presence of Sybil (ghost) vehicles that do not physically exist. The motivation for such attacks lies in the possibility of creating a "virtual" congestion that can influence routing algorithms, leading to "actual" congestion and chaos. We propose a Sybil attack-resilient traffic estimation and routing algorithm that is resilient against such attacks. In particular, our algorithm leverages noisy information from legacy sensing infrastructure, along with the dynamics and proximity graph of vehicles inferred from crowdsourced data. Furthermore, the scalability of our algorithm is based on efficient Boolean Satisfiability (SAT) solvers. We validated our algorithm using real traffic data from the Italian city of Bologna. Our algorithm led to a significant reduction in average travel time in the presence of Sybil attacks, including cases where the travel time was reduced from about an hour to a few minutes.

We present an efficient algorithm for multi-robot motion planning from linear temporal logic (LTL) specifications. We assume that the dynamics of each robot can be described by a discrete-time, linear system together with constraints on the control inputs and state variables. Given an LTL formula specifying the multi-robot mission, our goal is to construct a set of collision-free trajectories for all robots, and the associated control strategies, to satisfy We show that the motion planning problem can be formulated as the feasibility problem for a formula p over Boolean and convex constraints, respectively capturing the LTL specification and the robot dynamics. We then adopt a satisfiability modulo convex (SMC) programming approach that exploits a monotonicity property of p to decompose the problem into smaller subproblems. Simulation results show that our algorithm is more than one order of magnitude faster than state-of-the-art sampling-based techniques for high-dimensional state spaces while supporting complex missions.

This paper addresses the problem of state estimation of a linear time-invariant system when some of the sensors or/and actuators are under adversarial attack. In our set-up, the adversarial agent attacks a sensor (actuator) by manipulating its measurement (input), and we impose no constraint on how the measurements (inputs) are corrupted. We introduce the notion of “sparse strong observability” to characterize systems for which the state estimation is possible, given bounds on the number of attacked sensors and actuators. Furthermore, we develop a secure state estimator based on Satisfiability Modulo Theory (SMT) solvers.

Aided by advances in sensors and algorithms, systems for localizing and tracking target objects or events have become ubiquitous in recent years. Most of these systems operate on the principle of fusing measurements of distance and/or direction to the target made by a set of spatially distributed observers using sensors that measure signals such as RF, acoustic, or optical. The computation of the target's location is done using multilateration and multiangulation algorithms, typically running at an aggregation node that, in addition to the distance/direction measurements, also needs to know the observers' locations. This presents a privacy risk for an observer that does not trust the aggregation node or other observers and could in turn lead to lack of participation. For example, consider a crowd-sourced sensing system where citizens are required to report security threats, or a smart car, stranded with a malfunctioning GPS, sending out localization requests to neighboring cars -- in both cases, observer (i.e., citizens and cars respectively) participation can be increased by keeping their location private. This paper presents PrOLoc, a localization system that combines partially homomorphic encryption with a new way of structuring the localization problem to enable efficient and accurate computation of a target's location without requiring observers to make public their locations or measurements. Moreover, and unlike previously proposed perturbation based techniques, PrOLoc is also resilient to malicious active false data injection attacks. We present two realizations of our approach, provide rigorous theoretical guarantees, and also compare the performance of each against traditional methods. Our experiments on real hardware demonstrate that PrOLoc yields location estimates that are accurate while being at least 500\times faster than state-of-art secure function evaluation techniques.

This demo abstract presents PrOLoc, a localization system that combines partially homomorphic encryption with a new way of structuring the localization problem to enable efficient and accurate computation of a target's location while preserving the privacy of the observers.

We address the problem of determining the satisfiability of a Boolean combination of convex constraints over the real numbers, which is common in the context of hybrid system verification and control. We first show that a special type of logic formulas, termed monotone Satisfiability Modulo Convex (SMC) formulas, is the most general class of formulas over Boolean and nonlinear real predicates that reduce to convex programs for any satisfying assignment of the Boolean variables. For this class of formulas, we develop a new satisfiability modulo convex optimization procedure that uses a lazy combination of SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. Our approach can then leverage the efficiency and the formal guarantees of state-of-the-art algorithms in both the Boolean and convex analysis domains. A key step in lazy satisfiability solving is the generation of succinct infeasibility proofs that can support conflict-driven learning and decrease the number of iterations between the SAT and the theory solver. For this purpose, we propose a suite of algorithms that can trade complexity with the minimality of the generated infeasibility certificates. Remarkably, we show that a minimal infeasibility certificate can be generated by simply solving one convex program for a sub-class of SMC formulas, namely ordered positive unate SMC formulas, that have additional monotonicity properties. Perhaps surprisingly, ordered positive unate formulas appear themselves very frequently in a variety of practical applications. By exploiting the properties of monotone SMC formulas, we can then build and demonstrate effective and scalable decision procedures for problems in hybrid system verification and control, including secure state estimation and robotic motion planning.

We present a scalable robot motion planning algorithm for reach-avoid problems. We assume a discrete-time, linear model of the robot dynamics and a workspace described by a set of obstacles and a target region, where both the obstacles and the region are polyhedra. Our goal is to construct a trajectory, and the associated control strategy, that steers the robot from its initial point to the target while avoiding obstacles. Differently from previous approaches, based on the discretization of the continuous state space or uniform discretization of the workspace, our approach, inspired by the lazy satisfiability modulo theory paradigm, decomposes the planning problem into smaller subproblems, which can be efficiently solved using specialized solvers. At each iteration, we use a coarse, obstacle-based discretization of the workspace to obtain candidate high-level, discrete plans that solve a set of Boolean constraints, while completely abstracting the low-level continuous dynamics. The feasibility of the proposed plans is then checked via a convex program, under constraints on both the system dynamics and the control inputs, and new candidate plans are generated until a feasible one is found. To achieve scalability, we show how to generate succinct explanations for the infeasibility of a discrete plan by exploiting a relaxation of the convex program that allows detecting the earliest possible occurrence of an infeasible transition between workspace regions. Simulation results show that our algorithm favorably compares with state-of-the-art techniques and scales well for complex systems, including robot dynamics with up to 50 continuous states.

We introduce a scalable observer architecture, which can efficiently estimate the states of a discrete-time linear-time-invariant system whose sensors are manipulated by an attacker, and is robust to measurement noise. Given an upper bound on the number of attacked sensors, we build on previous results on necessary and sufficient conditions for state estimation, and propose a novel Multi-Modal Luenberger (MML) observer based on efficient Satisfiability Modulo Theory (SMT) solving. We present two techniques to reduce the complexity of the estimation problem. As a first strategy, instead of a bank of distinct observers, we use a family of filters sharing a single dynamical equation for the states, but different output equations, to generate estimates corresponding to different subsets of sensors. Such an architecture can reduce the memory usage of the observer from an exponential to a linear function of the number of sensors. We then develop an efficient SMT-based decision procedure that is able to reason about the estimates of the MML observer to detect at runtime which sets of sensors are attack-free, and use them to obtain a correct state estimate. Finally, we discuss two optimization-based algorithms that can efficiently select the observer parameters with the goal of minimizing the sensitivity of the estimates with respect to sensor noise. We provide proofs of convergence for our estimation algorithm and report simulation results to compare its runtime performance with alternative techniques. We show that our algorithm scales well for large systems (including up to 5,000 sensors) for which many previously proposed algorithms are not implementable due to excessive memory and time requirements. Finally, we illustrate the effectiveness of our approach, both in terms of resiliency to attacks and robustness to noise, on the design of large-scale power distribution networks.