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

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] Preprint: Controller Synthesis for Linear Time-varying Systems with Adversaries, Zhenqi Huang, Yu Wang, Sayan Mitra, and Geir Dullerud, Jan 2015. Available from: http://arxiv.org/abs/1501.04925

ACCOMPLISHMENT HIGHLIGHTS

  • Earlier, we had developed a sound and complete algorithm for solving this problem for the special case of linear control systems with L2-norm bounded adversaries. In this quarter, we first attempted to generalize this algorithm to nonlinear model, but it turned out that this approach did not scale because there were too many possible future states to consider with the adversary. This suggested to us an alternative approach which is to synthesize inductive proofs of the system's correctness (with adversaries) together with the controller rules. The preliminary results for this approach look promising.
  • We are developing a toolkit for synthesis using this new approach.