Automated Synthesis of Resilient Architectures - July 2016

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: 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

• Mohammad Ashiqur Rahman, AHM Jakaria, and Ehab Al-Shaer, "Formal Analysis for Dependable Supervisory Control and Data Acquisition in Smart Grids", The 46th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), Toulouse, France, June 2016.

ACCOMPLISHMENT HIGHLIGHTS

• Securing access to SCADA systems is not sufficient to fully protect the operation of smart grid critical infrastructure. However, an effort must be made to guarantee that the SCADA configuration exhibits the resiliency necessary to sustain potential contingencies of successful attacks. We developed an automated technique for verifying and measuring the resiliency of SCADA configuration against multiple concurrent coordinated attacks. In particular, given a SCADA system configuration, we can show if this system exhibits k-resiliency observability, k−Resilient Secured Observability, and k,r−resilient bad data detectability. In other words, we can prove that even if coordinated attacks can successfully make k sensing devices unavailable and r data corrupted, the operational integrity of SCADA is maintained intact.