Biblio

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.

Using Software-defined Networks in wide area (SDN-WAN) has been strongly emerging in the past years. Due to scalability and economical reasons, SDN-WAN mostly uses an in-band control mechanism, which implies that control and data sharing the same critical physical links. However, the in-band control and centralized control architecture can be exploited by attackers to launch distributed denial of service (DDoS) on SDN control plane by flooding the shared links and/or the Open flow agents. Therefore, constructing a resilient software designed network requires dynamic isolation and distribution of the control flow to minimize damage and significantly increase attack cost. Existing solutions fall short to address this challenge because they require expensive extra dedicated resources or changes in OpenFlow protocol. In this paper, we propose a moving target technique called REsilient COntrol Network architecture (ReCON) that uses the same SDN network resources to defend SDN control plane dynamically against the DDoS attacks. ReCON essentially, (1) minimizes the sharing of critical resources among data and control traffic, and (2) elastically increases the limited capacity of the software control agents on-demand by dynamically using the under-utilized resources from within the same SDN network. To implement a practical solution, we formalize ReCON as a constraints satisfaction problem using Satisfiability Modulo Theory (SMT) to guarantee a correct-by-construction control plan placement that can handle dynamic network conditions.

While existing proactive-based paradigms such as address mutation are effective in slowing down reconnaissance by naive attackers, they are ineffective against skilled human attackers. In this paper, we analytically show that the goal of defeating reconnaissance by skilled human attackers is only achievable by an integration of five defensive dimensions: (1) mutating host addresses, (2) mutating host fingerprints, (3) anonymizing host fingerprints, (4) deploying high-fidelity honeypots with context-aware fingerprints, and (5) deploying context-aware content on those honeypots. Using a novel class of honeypots, referred to as proxy honeypots (high-interaction honeypots with customizable fingerprints), we propose a proactive defense model, called (HIDE), that constantly mutates addresses and fingerprints of network hosts and proxy honeypots in a manner that maximally anonymizes identity of network hosts. The objective is to make a host untraceable over time by not letting even skilled attackers reuse discovered attributes of a host in previous scanning, including its addresses and fingerprint, to identify that host again. The mutations are generated through formal definition and modeling the problem. Using a red teaming evaluation with a group of white-hat hackers, we evaluated our five-dimensional defense model and compared its effectiveness with alternative and competing scenarios. These experiments as well as our analytical evaluation show that by anonymizing all identifying attributes of a host/honeypot over time, HIDE is able to significantly complicate reconnaissance, even for highly skilled human attackers.