Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems - January 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 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.

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

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

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

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

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.