Specification-driven moving target defense synthesis

Cyber agility enables cyber systems to defend proactively against sophisticated attacks by dynamically changing the system configuration parameters (called mutable parameters) in order to deceive adversaries from reaching their goals, disrupt the attack plans by forcing them to change their adversarial behaviors, and/or deterring them through prohibitively increasing the cost for attacks. However, developing cyber agility such as moving target defense techniques that are provable safe is a highly complex task that requires significant time and expertise. Our goal is to address this challenge by providing a framework for automating the creation of configuration-based moving target techniques rapidly and safely. In this paper, we present a cyber agility synthesis framework, called MTDSynth, that contains a formal ontology, MTD policy language, and MTD controller synthesis engine for implementing configuration-based moving target defense techniques. The policy language contains the agility specifications required to model the MTD technique, such as sensors, mutation trigger, mutation parameters, mutation actions, and mutation constraints. Based on the mutation constraints, the MTD controller synthesis engine provides an MTD policy refinement implementation for SDN configuration with provable properties using constraint satisfaction solvers. We show several examples of MTD controller synthesis, including temporal and spatial IP mutation, path mutation, detector mutation. We developed our ActivSDN over OpenDaylight SDN controller as an open programming environment to enable rapid and safe development of MTD sense-making and decision-making actions. Our implementation and evaluation experiments show not only the feasibility of MTD policy refinement but also the insignificant computational overhead of this refinement process.