ABSTRACT

Static system configuration provides the advantage for the attackers to discover the vulnerabilities of the system and launch attacks.

Moving Target Defense (MTD) can break this asymmetry for the defenders by mutating certain configuration parameters proactively and at the same time maintaining the run-time correctness and operational integrity. MTD is essentially distributed by nature since the processes or actions in MTD are executed in an interleaved manner. For any distributed system, it is important to verify the correctness and integrity, since they may be jeopardized by design errors or run time inconsistencies. In this work we present a framework for formal verification of MTD techniques. We describe MTD techniques with formal ontology and model the system behaviors with timed automata, and verify the correctness, liveness, fairness and deadlock-free properties of the system. We use Random Host Mutation (RHM) as the case study or MTD formal verification.

Our experimentation validates the feasibility and scalability of the formal verification framework.