Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems - July 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 quantitative measures of security metrics in a model-based design environment, with respect to different adversary classes.

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 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. 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.

[2] 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.

[3] 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.

[4] 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.

[5] 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.

[6] 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.

[7] M. Naghnaeian, P.G. Voulgaris, and G.E. Dullerud, "A Unified Framework for Lp Analysis and Synthesis of Linear Switched Systems", to appear at 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.

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

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.

ACCOMPLISHMENT HIGHLIGHTS

• 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.
• Our inductive synthesis algorithm is currently under review. Zhenqi Huang attended the Excape Synthesis Summer School at MIT. This summer we are looking to apply these approaches to realistic drone models for automatic synthesis.
• 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.