Automated Synthesis of Resilient Architectures - January 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

• Ashiq Rahman, Ehab Al-Shaer.  Submitted.  Automated Synthesis of Resilient Network Access Controls: A Formal Framework with Refinement. IEEE Transactions of Parallel and Distributed Computing (TPDC),.

• Yasir Khan, Ehab Al-Shaer.  2015.  Cyber Resilience-by-Construction: Modeling, Measuring & Verifying. ACM CCS Workshop on Automated Decision Making for Active Cyber Defense.

• Yasir Khan, Ehab Al-Shaer.  2015.  Property-Based Verification of Evolving ddd Petri Nets. International Conference of Software Engineering Advances.

ACCOMPLISHMENT HIGHLIGHTS

• Isolation is one of the most common resiliency techniques to enforce least privilege and restrict attack propagation and minimize attack consequences. We use hypothesis testing with our automated synthesis of security configuration framework to determine the optimal fine-grained isolation between any two hosts in the network. Our approach enables the users of the system to incrementally and automatically create and validate null hypotheses until the configuration for statistically optimal isolation is found.

• We developed a formal model to enable resilient-by-construction development of cyber system. Our preliminary model has two components: (1) resiliency metrics based on Cyber Resilience Engineering Framework (CREF), and (2) formal verification to investigate and extend the cyber model in order to exhibit the desired resilient properties in the design phase.

• It is important for resiliency property verification to reduce the state space generated for model checking as a result of dynamic reactive actions that can potentiall evolve the system states. We developed a preliminary formal framework to reduce the re-verification cost of an evolved model by restricting the model checking to the model part that is evolved, rather the entire system. This reduces the space and time complexity of resiliency verification.