A formal verification of configuration-based mutation techniques for moving target defense

Static system configuration provides a significant advantage for the adversaries to discover the assets and vulnerabilities in the system and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry for the defenders’ advantage by mutating certain configuration parameters proactively in order to disrupt attacks planning or increase the attack cost significantly. A key challenge in developing MTD techniques is guaranteeing design correctness and operational integrity. Due to the dynamic, asynchronous, and distributed nature of moving target defense, various mutation actions can be executed in an interleaved manner causing failures in the defense mechanism itself or negative interference in the cyber operations. Therefore, it is important to verify the correctness and operational integrity, of moving target techniques to identify the design errors or inappropriate run-time behavior that might jeopardize the effectiveness of MTD or cyber operations. To the best of our knowledge, there is no work aiming for the formal verification of the design correctness and integrity of moving target defense techniques. In this paper, we present a methodology for formal verification of configuration based moving target defense. We model the system behaviors with system modeling language (SysML) and formalize the MTD technique using du-ration calculus (DC). The formal model satisfies the constraints and de-sign correctness properties. We use the random host mutation (RHM) as a case study of the MTD system that randomly mutates the IP addresses to make end-hosts untraceable by scanners. We validate the design correctness of RHM using model checking over various configuration-based mutation parameters.