Automated Synthesis of Resilient Architectures - January 2015

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):  Ehab Al-Shaer
Researchers: Ashiq Rahman, Mohamed Alsaleh, Ghaith Husari

HARD PROBLEM(S) ADDRESSED

• Resilient Architectures:  The goal of this project is to develop a formal automated reasoning framework for designing resilient architectures with provable bounds/metrics for cyber and Cyber-physical systems. This includes investigating metric-driven automated  synthesis of security counter-measures to resist and mitigate attacks for cyber and cyber-physical systems. This research work contributes to the design and verification of resilient architectures with guaranteed properties. 

PUBLICATIONS

• Moving Target Defense for Hardening the Security of the Power System State Estimation.

ACCOMPLISHMENT HIGHLIGHTS

• We continue our development of formal logic-based models and tools for investigating/verifying the resiliency of energy management systems (EMS) in smart grids. Our goal is to measure the system resiliency for resisting attacks under varying adversary’s capacity and resources. Our developed tool (smart grid resiliency analyzer) can measure the potential threats and their impacts considering the attacker’s capabilities, knowledge, resources, and potential attack evasion (stealthiness) due to interdependency complexity  of the system components. We also extended our model to determine the most cost-effective resilient architecture/technique to mitigate this threat. I.e., using our smart grid threat analytics tool we can answer questions like: What, Where, and How-far can an attack percolate in the smart grids given system specific including bus-topology and configurations, and varying attack attributions.
• We investigated a new technique that can significantly improve the resiliency of intrusion detection systems in Advanced Metering Infrastructure against highly stealthy attacks. Our technique is based on randomization of smart grid configuration, specifically state estimation and AMI configuration.
• We started investigating using symbolic model checker and temporal logic for verifying the resilience properties of system configuration of cyber systems based on isolation, diversity and redundancy mechanisms.