| Title | A Formal Analysis of Moving Target Defense |
| Publication Type | Conference Paper |
| Year of Publication | 2020 |
| Authors | Abdul Basit Ur Rahim, Muhammad, Duan, Qi, Al-Shaer, Ehab |
| Conference Name | 2020 IEEE 44th Annual Computers, Software, and Applications Conference (COMPSAC) |
| Date Published | jul |
| Keywords | Analytical models, Automata, Computational modeling, configuration-based mutation, formal specification, IP networks, Metrics, model checking, moving target defense, pubcrawl, Scalability, Switches, Tools, verification |
| Abstract | Static system configuration provides a significant advantage for the adversaries to discover the assets and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry by mutating certain configuration parameters to disrupt the attack planning or increase the attack cost significantly. In this research, we present a methodology for the formal verification of MTD techniques. We formally modeled MTD techniques and verified them against constraints. We use Random Host Mutation (RHM) as a case study for MTD formal verification. The RHM transparently mutates the IP addresses of end-hosts and turns into untraceable moving targets. We apply the formal methodology to verify the correctness, safety, mutation, mutation quality, and deadlock-freeness of RHM using the model checking tool. An adversary is also modeled to validate the effectiveness of the MTD technique. Our experimentation validates the scalability and feasibility of the formal verification methodology. |
| DOI | 10.1109/COMPSAC48688.2020.00050 |
| Citation Key | abdul_basit_ur_rahim_formal_2020 |
A Formal Analysis of Moving Target Defense