Visible to the public Automated Synthesis of Resilient Architectures - October 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):  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. 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
 

  • Mohammad Ashiqur Rahman, Ehab Al-Shaer and Rajesh G. Kavasseri, Impact Analysis of Topology Poisoning Attacks on Economic Operation of the Smart Power Grid, The 34th International Conference on Distributed Computing Systems (ICDCS), Number: Madrid, Spain, July 2014

 

ACCOMPLISHMENT HIGHLIGHTS

  •  We model the operational inter-dependency between major critical components of smart grid, namely state estimation, optimal power flow and topology processor. We then use this model to measure to the resiliency of energy management systems against stealthy attacks. Our preliminary results show that state estimation corruption attacks are possible even with the existence of the state of the art bad data injection detection algorithms. In specific, we show that if attackers acquire specific (quantified) capabilities and knowledge, they can launch a stealthy topology poisoning attacks that  compromise the integrity of OPF (Optimal Power Flow) module, and thus undermine smart grid economic operation. We also present a formal verification based framework to systematically analyze the impact of such attacks on OPF. The proposed framework is useful for formally identifying and analyzing vulnerabilities and developing suitable defense strategies for smart grids.
  • The contribution of this work to science of security comes in many folds. First, it provides a formal foundation to investigate the impact of components’ interdependency on the attackability of smart grid.  Second, it developed a formal analytic approach to quantify the attackers’ capabilities required to launch a successful attack. Third, it quantifies the direct and indirect impact of the attack and required mitigation techniques.