Visible to the public Automated Synthesis of Resilient Architectures - October 2015Conflict Detection Enabled

Submitted by drwright on Mon, 09/21/2015 - 9:09am

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

ACCOMPLISHMENT HIGHLIGHTS

  • Advanced Metering Infrastructure (AMI) of smart gird is highly vulnerable to attacks that can cause reachability and/or instability problems in smart grid. Therefore, ensuring correct and resilient configuration is important to avoid AMI failures due to misconfigurations or attacks. We identify two major factors for resilient AMI architecture: (1) report-scheduling meter configuration, which determine when and how to report power consumption data, and (2) placement of the smart collectors that connect meters to energy control systems. 

  • We developed formal models and constraints to automatically synthesize dependable AMI architecture including meter configuration and smart collector placement to guarantee services continuity and reachability even if the network is under attack. The AMI configuration synthesis plan can potentially consider provisioned resistance for resiliency against attacks such as “meters should be able to communicate even if 10% of the meters are malicious”.

  • We formulized and implemented our proposed framework using Satisfiability Modulo Theories (SMT) and evaluated the scalability of our model with large size AMI (10,000 meters in one area).

Groups: