Static Dynamic Analysis of Security Metrics for Cyber Physical Systems - January 2017

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 Dullerund 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] 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, 55th IEEE Conference on Decision and Control, Las Vegas, NV, December 12-14, 2016.

[2] Hussein Sibaie and Sayan Mitra, "Optimal data rates for estimation and model detection of switched dynamical systems", 20th ACM International Conference on Hybrid Systems: Computation and Control in conjunction with CPS Week 2017, Pittsburgh, PA, April 18-21, 2017, to appear.

Abstract: State estimation is a fundamental problem for intrusion detection and monitoring. Cyber-Physical systems interconnect sensing and computing devices over a shared bandwidth-limited channels, and therefore, estimation algorithms should strive to use bandwidth optimally. We present a notion of entropy for state estimation of nonlinear switched dynamical systems, an upper bound for it and a state estimation algorithm for the case when the switching signal is unobservable. Our approach relies on the notion of topological entropy and uses techniques from the theory for control under limited information. We show that the average bit rate used is optimal in the sense that, the efficiency gap of the algorithm is within an additive constant of the gap between estimation entropy of the system and its known upper-bound. We apply the algorithm to several system models, including a model of a glycemic index used in medical devices, and discuss the performance implications of the number of tracked modes.

[3] Zhenqi Huang, Yu Wang, Sayan Mitra, and Geir Dullerud. "Differential Privacy and Entropy in Distributed Feedback Systems: Minimizing Mechanisms and Performance Trade-offs", IEEE Transactions on Network Control Systems, to appear.

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

[4] M. Philipe, R. Essick, G.E. Dullerud, and R. Jungers, "Stability of discrete-time switching systems with constrained switching sequences", Automatica, volume 72, pages 242-250, October 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.

[5] Wang, Y., M. Hale, M. Egerstedt, and G. Dullerud, "Differentially Private Objective Functions in Distributed Cloud-based Optimization," 55th IEEE Conference on Decision and Control (CDC 2016), Las Vegas, NV, December 12-14, 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.

[6] Philippe, M., R. Essick, G.E. Dullerud, and R.M. Jungers, "Extremal storage functions and minimal realizations of discrete-time linear switching systems", IEEE Conference on Decision and Control (CDC 2016), Las Vegas, NV, December 12-14, 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 appeared at the IEEE Conference on Decision and Control, December 2016.
• Mitra is Co-chairing the Program Committee for the 20th International Conference on Hybrid Systems, which is one of the flagship conferences of CPSWeek 2017. Contributions on security of cyber-physical systems were especially solicited this year.
• Mitra presented Frontiers seminar "Auditing Algorithms" at the Master of Technology Management Program (MSTM) at the University of Illinois' Business School, December 2nd, 2016.
• Workshop proceedings First International Workshop on Science of Security of CyberPhysical Systems (SOSCPS) to appear as IEEE Proceedings. 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.