Automated Synthesis of Resilient Architectures - January 2017
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 Alsaleh and Ehab Al-Shaer, Towards Automated Verification of Active Cyber Defense Strategies on Software Defined Networks, ACM SafeConfig '16 Proceedings of the 2016 ACM Workshop on Automated Decision Making for Cyber Defense, October 2016.
ACCOMPLISHMENT HIGHLIGHTS
-
Cyber resilience requires the deployment of Active Cyber Defense (ACD) capabilities that enable timely and scalable reconfiguration of the cyber system (network devices and hosts) to respond to cyber threats and mitigate potential risks automatically. However, since ACD strategies can dynamically change the state of the cyber systems, a successful deployment of ACD strategies will essentially require guaranteeing that ACD satisfy the following three properties: (1) “correct” (i.e., ACD operations is indeed enforceable using the current network configuration and capabilities), (2) “safe” (i.e., ACD does not cause any damages to the mission) and (3) “effective” (i.e., ACD can eliminate this threat and maintain the cyber mission integrity). In this work, we focus on developing a formal framework for verifying the first two (correctness and safety) of ACD in a dynamic cyber environment. We implemented this system using OpenFlow-based Software Defined Networks, and we evaluated the time complexity for verifying ACD on OpenFlow networks of over two thousand nodes and thousands of rules.
Although the focus of this project, so far, is on network-level ACDs, it can connect very well with various effort in the Lablet the address monitoring and alarm correlation to enable comprehensive and fully-automated ACD capabilities.