Visible to the public Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems - October 2015Conflict Detection Enabled

Submitted by awhitesell on Tue, 10/06/2015 - 11:05am

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
  • Predictive security metrics

Our mathematical framework and algorithms will provide 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] Controller Synthesis for Linear Time-varying Systems with Adversaries. Zhenqi Huang, Yu Wang, Sayan Mitra, Geir Dullerud, and Swarat Chaudhuri. To appear in the proceedings of IEEE International Conference on Decision and Control (CDC), Osaka, Japan. December 2015.

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

[3] A Framework for Analyzing Cost of Securing Control Systems. Zhenqi Huang, Yu Wang, Sayan Mitra, Geir Dullerud, In the Next Wave, National Security Agency's Emerging Technologies Journal. To appear in December 2015.

[4] A lifting approach to L2-gain analysis of periodic event-triggered and switching sampled-data control systems. Maurice Heemels, Geir Dullerud, and AndrewTeel, To appear in the proceedings of IEEE International Conference on Decision and Control (CDC), Osaka, Japan. December 2015.

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

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.

Groups: