Verifying the enforcement and effectiveness of network lateral movement resistance techniques

As the sophistication of cyber-attacks is ever increasing, cyber breaches become inevitable and their consequences are often highly damaging. Isolation and diversity are key techniques of cyber resilience for creating built-in resistance in cyber networks against the lateral movement of multi-step Advanced Persistent Threats (APTs) and epidemic attacks. However, the key unaddressed challenges are (1) how to ensure that specific isolation and diversity configurations are sufficient to prevent the lateral movement of attacks and (2) how to verify that such configurations are enforced safely despite the complex inter-dependency between cyber components. In this paper, we address these challenges by developing formal models and properties to verify the effectiveness and enforceability of proactive cyber resistance techniques. We present a bounded model checking approach based on satisfiability Modulo theories (SMT) for OpenFlow software defined networks (SDNs). We verify that given resistance techniques are enforced in a way that does not violate the cyber mission requirements and we evaluate the configuration resistance based on user-defined resistance properties.