Biblio

Active Cyber Defense (ACD) reconfigures cyber systems (networks and hosts) in timely manner in order to automatically respond to cyber incidents and mitigate potential risks or attacks. However, to launch a successful cyber defense, ACD strategies need to be proven effective in neutralizing the threats and enforceable under the current state and capabilities of the network. In this paper, we present a bounded model checking framework based on SMT to verify that the network can support the given ACD strategies accurately and safely without jeopardizing cyber mission invariants. We abstract the ACD strategies as sets of serializable reconfigurations and provide user interfaces to define cyber mission invariants as reachability, security, and QoS properties. We then verify the satisfaction of these invariants under the given strategies. We implemented this system on OpenFlow-based Software Defined Networks and we evaluated the time complexity for verifying ACD strategies on OpenFlow networks of over two thousand nodes and thousands of rules.