Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems - July 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 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, 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, volume 4, issue 1, March 2017. http://ieeexplore.ieee.org/document/7833044/

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.

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

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] Joao Jansch Porto and Geir E. Dullerud, "Decentralized Control with Moving-Horizon Linear Switched Systems: Synthesis and Testbed Implementation", American Control Conference 2017, Seattle, WA, May 24-26, 2017.

Abstract: In this paper, we develop new exact results on switched decentralized control to accommodate moving horizon conditions, and explicitly implement the developed algorithms on a cyberphysical testbed system. Here the switching can be regarded as coming from attacks, or as changes to operating conditions. Using derivations for a centralized controller with look-ahead, we derive decentralized algoriths with finite memory to include receding horizon modal information. We compare the performance of a switched controller with finite memory and look-ahead horizon to that of a linear time independent (LTI) controller using a simulation. The decentralized controller is further tested with a real-world system comprised of multiple model-sized hovercrafts.

[4] Wang, Y., S. Mitra, and G. Dullerud, "Differential Privacy and Minimum-Variance Unbiased Estimation in Multi-agent Control Systems," to appear IFAC World Congress, Toulouse, France, July 9-14, 2017, to appear.

Abstract: In a discrete-time linear multi-agent control system, where the agents are coupled via an environmental state, a knowledge of the environmental state is desirable to control the agents locally. However, since the environmental state depends on the behavior of the agents, sharing it directly among these agents jeopardizes the privacy of the agents' profiles, defined as the combination of the agents' initial states and the sequence of local control inputs over time. A commonly used solution is to randomize the environmental state before sharing - this leads to a natural trade-off between the privacy of the agents' profiles and the accuracy of estimating the environmental state. By treating the multi-agent system as a probabilistic model of the environmental state parametrized by the agents' profiles, we show that when the agents' profiles is epsilon-differentially private, there is a lower bound on the L1-induced norm of the covariance matrix of the minimum-variance unbiased estimator of the environmental state. This lower bound is achieved by a randomized mechanism that uses Laplace noise.

ACCOMPLISHMENT HIGHLIGHTS

• Dullerud giving keynote at DARS Workshop, CAV, 2017.
• 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.
• Chaudhuri Co-Chaired the International Conference on Computer Aided Verification (CAV), 2016.
• 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.