Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems - October 2016

Public Audience
Purpose: To highlight project progress. Information is generally at a higher level which is accessible to the interested public. All information contained in the report (regions 1-3) is a Government Deliverable/CDRL.

PI(s): Sayan Mitra

Co-PI(s): Geir Dullerud and Swarat Chaudhuri (Rice University)

HARD PROBLEM(S) ADDRESSED
This refers to Hard Problems, released November 2012.

• Scalability and composability: we are developing rigorous, model-based approaches for analyzing and synthesizing security metrics of large cyber-physical systems such as power systems, traffic control systems and implanted medical devices. In order to make the approaches scale to large models, we are developing foundational results on compositional analysis.
• Predictive security metrics: we are developing analysis approaches that tackle different adversary models to give.

PUBLICATIONS
Papers published in this quarter as a result of this research. Include title, author(s), venue published/presented, and a short description or abstract. Identify which hard problem(s) the publication addressed. Papers that have not yet been published should be reported in region 2 below.

[1] Zhenqi Huand and Sayan Mitra, "Approximate Partial Order Reduction", in submission, October 2016.

We develop a partial order reduction method for labeled transition systems over metric spaces. We introduce the notion of e-independent actions such that executing these actions in any order results in states that are close to each other. Then we define e-equivalent action sequences that swap e-independent action pairs. We present an algorithm to over-approximate the reach set of executions that take e-equivalent action sequences. We are also able to show that the over-approximation can be computed up to arbitrary precision.

[2] Jorge Cortes, Geir E. Dullerud, Shuo Han, Jerome Le Ny, Sayan Mitra, and George J. Pappas, "Differential Privacy in Control and Network Systems", Invited Tutorial Paper to appear in IEEE Conference on Decision and Control 2016.

[3] Hussein Sibaie and Sayan Mitra, "Optimal data rates for estimation and model detection of switched dynamical systems", in submission, October 2016.

[4] Zhenqi Huang, Yu Wang, Sayan Mitra, and Geir Dullerud. "Differential Privacy and Entropy in Distributed Feedback Systems: Minimizing Mechanisms and Performance Trade-offs". Under review (second round) for IEEE Trans. On Network Control Systems, Nov 2015.

In distributed control systems with shared resources, participating agents can improve the overall performance of the system by sharing data about their personal preferences. In this article, we formulate and study a natural trade-off arising in these problems between the privacy of the agent's data and the performance of the control system. We formalize privacy in terms of differential privacy of agents' preference vectors. The overall control system consists of N agents with linear discrete-time coupled dynamics, each controlled to track its preference vector. Performance of the system is measured by the mean squared tracking error. We present a mechanism that achieves differential privacy by adding Laplace noise to the shared information in a way that depends on the sensitivity of the control system to the private data. We show that for stable systems the performance cost of using this type of privacy preserving mechanism grows as O(T3/Ne2), where T is the time horizon and e is the privacy parameter. For unstable systems, the cost grows exponentially with time. From an adversary's point of view, we investigate the best estimates that can be derived from a sequence of the noisy shared data. We establish a lower-bound for the entropy of any unbiased estimator of the private data from any noise-adding mechanism that gives e-differential privacy. We show that the mechanism achieving this lower-bound is a randomized mechanism that also uses Laplace noise.

[5] Yu Wang, Geir Dullerud, and Sayan Mitra, "Differential Privacy of Iterative Learning Algorithms", in preparation, October 2016.

[6] Zhenqi Huang, Chuchu Fan, and Sayan Mitra, "Bounded Invariant Verification for Time-Delayed Nonlinear Networked Dynamical Systems", to appear in IFAC Journal for Nonlinear Analysis: Hybrid Systems, 2016. Available online: http://authors.elsevier.com/sd/article/S1751570X16300279

Abstract: We present a technique for bounded invariant verification of nonlinear networked dynamical systems with delayed interconnections. The underlying problem in precise bounded-time verification lies with computing bounds on the sensitivity of trajectories (or solutions) to changes in initial states and inputs of the system. For large networks, computing this sensitivity with precision guarantees is challenging. We introduce the notion of input-to-state (IS) discrepancy of each module or subsystem in a larger nonlinear networked dynamical system. The IS discrepancy bounds the distance between two solutions or trajectories of a module in terms of their initial states and their inputs. Given the IS discrepancy functions of the modules, we show that it is possible to effectively construct a reduced (low dimensional) time-delayed dynamical system, such that the trajectory of this reduced model precisely bounds the distance between the trajectories of the complete network with changed initial states. Using the above results we develop a sound and relatively complete algorithm for bounded invariant verification of networked dynamical systems consisting of nonlinear modules interacting through possibly delayed signals. Finally, we introduce a local version of IS discrepancy and show that it is possible to compute them using only the Lipschitz constant and the Jacobian of the dynamic function of the modules.

[6] M. Naghnaeian, P.G. Voulgaris, and G.E. Dullerud, "A Unified Framework for Lp Analysis and Synthesis of Linear Switched Systems", Proceedings American Control Conference, 2016.

Abstract. In this paper, we develop a new framework to analyze stability and stabilizability of Linear Switched Systems (LSS) as well as their gain computations. Our approach is based on a combination of state space operator descriptions and the Youla parametrization and provides a unified way for analysis and synthesis of LSS, and in fact of Linear Time Varying (LTV) systems, in any Lp induced norm sense. By specializing to the l case, we show how Linear Programming can be used to test stability, stabilizability and to synthesize stabilizing controllers that guarantee a near optimal closed-loop gain.

[7] M. Philipe, R. Essick, G.E. Dullerud, and R. Jungers, "Stability of discrete-time switching systems with constrained switching sequences.", Automatica, 2016.

Abstract. We introduce a novel framework for the stability analysis of discrete-time linear switching systems with switching sequences constrained by an automaton. The key element of the framework is the algebraic concept of multinorm, which associates a different norm per node of the automaton, and allows to exactly characterize stability. Building upon this tool, we develop the first arbitrary accurate approximation schemes for estimating the constrained joint spectral radius p, that is the exponential growth rate of a switching system with constrained switching sequences. More precisely, given a relative accuracy r > 0, the algorithms compute an estimate of p within the range [p, (1 + r)p]. These algorithms amount to solve a well de_ned convex optimization program with known time-complexity, and whose size depends on the desired relative accuracy r > 0.

[7] Zhenqi Huang, Yu Wang, Sayan Mitra, Geir Dullerud, and Swarat Chaudhuri, "Controller Synthesis for Linear Time-varying Systems with Adversaries", IEEE International Conference on Decision and Control (CDC), Osaka, Japan, December 2015.

Abstract: We present a controller synthesis algorithm for reach-avoid problems for piecewise linear discrete-time systems. Our algorithm relies on SMT solvers and in this paper we focus on piecewise constant control strategies. Our algorithm generates feedback control laws together with inductive proofs of unbounded time safety and progress properties with respect to the reach-avoid sets. Under a reasonable robustness assumption, the algorithm is shown to be complete. That is, it either generates a controller of the above type along with a proof of correctness, or it establishes the impossibility of the existence of such controllers. To achieve this, the algorithm iteratively attempts to solve a weakened and strengthened versions of the SMT encoding of the reach-avoid problem. We present preliminary experimental results on applying this algorithm based on a prototype implementation.

[8] Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, and Marta Kwiatkowska, "Simulation-based Verification of Cardiac Pacemakers with Guaranteed Coverage", Special Issue of the IEEE Design and Test, June 2015. DOI 10.1109/MDAT.2015.2448543

Abstract: The testing of medical devices poses numerous challenges due to continuous interactions between the physical processes and the cyber components. This paper highlights the main challenges for the design and verification of pacemakers and describes a framework based on discrepancy functions for investigating and validating the time-bounded safety properties as well as determining the safe ranges for the system parameters.

[9] Zhenqi Huang, Yu Wang, Sayan Mitra, Geir Dullerud, "A Framework for Analyzing Cost of Securing Control Systems" The Next Wave, National Security Agency's Emerging Technologies Journal, December 2015.

Abstract. This article describes our recent progress on the development of rigorous analytical metrics for assessing the threat-performance trade-off in control systems. Computing systems that monitor and control physical processes are now pervasive, yet their security is frequently an afterthought rather than a first-order design consideration. We investigate a rational basis for deciding--at the design level--how much investment should be made to secure the system.

[10] Maurice Heemels, Geir Dullerud, and AndrewTeel, "A Lifting Approach to L2-gain Analysis of Periodic Event-triggered and Switching Sampled-data Control Systems". IEEE International Conference on Decision and Control (CDC), Osaka, Japan. December 2015.

Abstract: In this work we are interested in the stability and L2-gain of hybrid systems with linear flow dynamics, periodic time-triggered jumps and nonlinear possibly set-valued jump maps. This class of hybrid systems includes various interesting applications such as periodic event-triggered control and certain networked control systems with scheduling protocols and fixed transmission intervals. In this paper we also show that sampled-data systems with arbitrarily switching controllers can be captured in this framework by requiring the jump map to be set-valued. We provide novel conditions for the internal stability and L2-gain analysis of these systems adopting a lifting-based approach. In particular, we establish that the internal stability and contractivity in terms of an L2-gain are equivalent to the internal stability and contractivity of a particular discrete-time set-valued nonlinear system. Despite earlier works in this direction, these novel characterizations are the first conditions that are both necessary and sufficient. The results are illustrated through multiple, novel examples.

[11] Maurice Heemels, Geir Dullerud, and AndrewTeel, "L2-gain Analysis for a Class of Hybrid Systems with Applications to Reset and Event-triggered Control: A Lifting Approach", IEEE Transactions on Automatic Control, 2015; accepted.

Abstract. In this paper we study the stability and L2-gain properties of a class of hybrid systems that exhibit linear flow dynamics, periodic time-triggered jumps and arbitrary nonlinear jump maps. This class of hybrid systems is relevant for a broad range of applications including periodic event-triggered control, sampled-data reset control, sampled-data saturated control, and certain networked control systems with scheduling protocols. For this class of continuous-time hybrid systems we provide new stability and L2-gain analysis methods. Inspired by ideas from lifting we show that the stability and the contractivity in L2-sense (meaning that the L2-gain is smaller than 1) of the continuous-time hybrid system is equivalent to the stability and the contractivity in `2-sense (meaning that the `2-gain is smaller than 1) of an appropriate discrete-time nonlinear system. These new characterizations generalize earlier (more conservative) conditions provided in the literature. We show via a reset control example and an event-triggered control application, for which stability and contractivity in L2-sense is the same as stability and contractivity in `2-sense of a discrete-time piecewise linear system, that the new conditions are significantly less conservative than the existing ones in the literature. Moreover, we show that the existing conditions can be reinterpreted as a conservative `2-gain analysis of a discrete-time piecewise linear system based on common quadratic storage/Lyapunov functions. These new insights are obtained by the adopted lifting-based perspective on this problem, which leads to computable `2-gain (and thus L2-gain) conditions, despite the fact that the linearity assumption, which is usually needed in the lifting literature, is not satisfied.

[12] Wang, Y., M. Hale, M. Egerstedt, and G. Dullerud, "Differentially Private Objective Functions in Distributed Cloud-based Optimization," to appear at IEEE Conference on Decision and Control (CDC), 2016.

Abstract. In this work, we study the problem of keeping the objective functions of individual agents "-differentially private in cloud-based distributed optimization, where mobile agents are subject to global constraints and seek to minimize local objective functions. The communication architecture between is cloud-based - instead of communicating directly with each other, they coordinate by sharing states through a trusted cloud computer. In this problem, the difficulty is twofold: the objective functions are used repeatedly in every iteration, and the influence of perturbing them extends to other agents and lasts over time. To solve the problem, we analyze the propagation of perturbations on objective functions over time, and derive an upper bound on them. With the upper bound, we design a noise-adding mechanism that randomizes the cloud based distributed optimization algorithm to keep the individual objective functions "-differentially private. In addition, we study the trade-off between the privacy of objective functions and the performance of the new cloud-based distributed optimization algorithm with noise. We present simulation results to numerically verify the theoretical results presented.

[13] Philippe, M., R. Essick, G.E. Dullerud, and R.M. Jungers, "Extremal storage functions and minimal realizations of discrete-time linear switching systems ", to appear at IEEE Conference on Decision and Control (CDC), 2016.

Abstract. We study the Lp induced gain of discrete- time linear switching systems with graph-constrained switching sequences. We first prove that, for stable systems in a minimal realization, for every p 1, the Lp-gain is exactly characterized through switching storage functions. These functions are shown to be the pth power of a norm. In order to consider general systems, we provide an algorithm for computing min- imal realizations. These realizations are rectangular systems, with a state dimension that varies according to the mode of the system. We apply our tools to the study on the of L2-gain. We provide algorithms for its approximation, and provide a converse result for the existence of quadratic switching storage functions. We finally illustrate the results with a physically motivated example.

ACCOMPLISHMENT HIGHLIGHTS

• A new invited tutorial paper on privacy of control systems has been accepted for the IEEE Conference on Decision and Control, to appear in December 2016.
• Workshop proceedings First International Workshop on Science of Security of CyberPhysical Systems (SOSCPS) to appear as IEEE Proceedings.[Office1] Edited by Sayan Mitra and Geir Dullerud, 2016.
• Zhenqi Huang defended his PhD dissertation in September 2016.
• Our simulation-based formal analysis approaches have gained momentum. The IEEE Design and Test paper mentioned above shows that this approach can be used to analyze models of medical devices like pacemakers together with relevant abstractions of physiology. In another related paper, we show that the approaches can handle challenge problems coming from the automotive industry. That paper received the Robert Bosch sponsored best verification result award at the ARCH workshop of CPSWeek.
• Mitra was awarded Rigorous Systems Engineering (RiSE) Fellowship to visit Technical University of Vienna and presented a lecture on parameterized verification of distributed systems in Dec 2015.
• Developed new security verification tools for nonlinear sampled systems.
• [Office1]Andrea, please update the title or the status as you see fit.