| Title | Towards Automated Verification of Active Cyber Defense Strategies on Software Defined Networks |
| Publication Type | Conference Paper |
| Year of Publication | 2016 |
| Authors | Alsaleh, Mohammed Noraden, Al-Shaer, Ehab |
| Conference Name | Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4566-8 |
| Keywords | active cyber defense, bounded model checking, configuration, Human Behavior, Metrics, OpenFlow, pubcrawl, Resiliency, Scalability, Software Defined Networks, threat mitigation, verification |
| Abstract | 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. |
| URL | http://doi.acm.org/10.1145/2994475.2994482 |
| DOI | 10.1145/2994475.2994482 |
| Citation Key | alsaleh_towards_2016 |
Towards Automated Verification of Active Cyber Defense Strategies on Software Defined Networks