Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems - July 2014

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, Swarat Chaudhuri (Rice University)
Researchers:

HARD PROBLEM(S) ADDRESSED
* Scalability and composability
* Predictive security metrics

PUBLICATIONS
Report papers written as a result of this research. Include title, authors, venue published/presented, and a short description or abstract. Also, please identify which hard problem(s) the publication addressed.

[1] Proving Abstractions of Dynamical Systems through Numerical Simulations, Sayan Mitra. In Hot Topics in Science of Security (HOTSOS), SOS Community meeting, Raleigh, NC 2014.

[2] Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells, Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra and Marta Kwiatkowska. In Computer Aided Verification (CAV 2014), Vienna, Austria, 2014. Part of the Vienna Summer of Logic.

ACCOMPLISHMENT HIGHLIGHTS

* We have developed a technique for deciding bounded time safety properties of deterministic nonlinear hybrid models. These models can capture a wide range of cyberphysical systems. The results will be presented next week in the CAV which is a part of the Vienna Summer of Logic this year. This is the largest gathering of logicians in the history of the field.

* We organized a kick-off meeting on 14th February during which Prof. Swarat Chaudhuri visited Illinois and we discussed different adversary models (from stochastic games and control theory), and relevant analysis techniques, in a day long technical meeting.

* Subsequently, we have formulated a computational problem in automated synthesis of alternating periodic controllers with a model of an adversary that adds arbitrary control inputs. We are currently experimenting with solving these alternating games using SMT solvers.