Towards automated verification of active cyber defense strategies on software defined networks

Mohammed Noraden Alsaleh; Ehab Al-Shaer

doi:10.1145/2994475.2994482

Towards automated verification of active cyber defense strategies on software defined networks

Mohammed Noraden Alsaleh, Ehab Al-Shaer

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

2 Scopus citations

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.

Original language	English
Title of host publication	SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016
Publisher	Association for Computing Machinery, Inc
Pages	23-29
Number of pages	7
ISBN (Electronic)	9781450345668
DOIs	https://doi.org/10.1145/2994475.2994482
State	Published - 24 Oct 2016
Externally published	Yes
Event	9th ACM Workshop on Automated Decision Making for Active Cyber Defense, SafeConfig 2016 - Vienna, Austria Duration: 24 Oct 2016 → …

Publication series

Name	SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016

Conference

Conference	9th ACM Workshop on Automated Decision Making for Active Cyber Defense, SafeConfig 2016
Country/Territory	Austria
City	Vienna
Period	24/10/16 → …

Bibliographical note

Publisher Copyright:
© 2016 ACM.

Keywords

Active cyber defense
Bounded model checking
Configuration
OpenFlow
Software defined networks
Verification

ASJC Scopus subject areas

Computer Science Applications
Artificial Intelligence
Computational Theory and Mathematics

Access to Document

10.1145/2994475.2994482

Cite this

Alsaleh, M. N., & Al-Shaer, E. (2016). Towards automated verification of active cyber defense strategies on software defined networks. In SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016 (pp. 23-29). (SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016). Association for Computing Machinery, Inc. https://doi.org/10.1145/2994475.2994482

Alsaleh, Mohammed Noraden ; Al-Shaer, Ehab. / Towards automated verification of active cyber defense strategies on software defined networks. SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016. Association for Computing Machinery, Inc, 2016. pp. 23-29 (SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016).

@inproceedings{35224b5bc69749c98f6096bb50ef11f4,

title = "Towards automated verification of active cyber defense strategies on software defined networks",

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.",

keywords = "Active cyber defense, Bounded model checking, Configuration, OpenFlow, Software defined networks, Verification",

author = "Alsaleh, \{Mohammed Noraden\} and Ehab Al-Shaer",

note = "Publisher Copyright: {\textcopyright} 2016 ACM.; 9th ACM Workshop on Automated Decision Making for Active Cyber Defense, SafeConfig 2016 ; Conference date: 24-10-2016",

year = "2016",

month = oct,

day = "24",

doi = "10.1145/2994475.2994482",

language = "English",

series = "SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016",

publisher = "Association for Computing Machinery, Inc",

pages = "23--29",

booktitle = "SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016",

}

Alsaleh, MN & Al-Shaer, E 2016, Towards automated verification of active cyber defense strategies on software defined networks. in SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016. SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016, Association for Computing Machinery, Inc, pp. 23-29, 9th ACM Workshop on Automated Decision Making for Active Cyber Defense, SafeConfig 2016, Vienna, Austria, 24/10/16. https://doi.org/10.1145/2994475.2994482

Towards automated verification of active cyber defense strategies on software defined networks. / Alsaleh, Mohammed Noraden; Al-Shaer, Ehab.
SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016. Association for Computing Machinery, Inc, 2016. p. 23-29 (SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Towards automated verification of active cyber defense strategies on software defined networks

AU - Alsaleh, Mohammed Noraden

AU - Al-Shaer, Ehab

PY - 2016/10/24

Y1 - 2016/10/24

N2 - 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.

AB - 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.

KW - Active cyber defense

KW - Bounded model checking

KW - Configuration

KW - OpenFlow

KW - Software defined networks

KW - Verification

UR - https://www.scopus.com/pages/publications/84997637249

U2 - 10.1145/2994475.2994482

DO - 10.1145/2994475.2994482

M3 - Conference contribution

AN - SCOPUS:84997637249

T3 - SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016

SP - 23

EP - 29

BT - SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016

PB - Association for Computing Machinery, Inc

T2 - 9th ACM Workshop on Automated Decision Making for Active Cyber Defense, SafeConfig 2016

Y2 - 24 October 2016

ER -

Alsaleh MN, Al-Shaer E. Towards automated verification of active cyber defense strategies on software defined networks. In SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016. Association for Computing Machinery, Inc. 2016. p. 23-29. (SafeConfig 2016 - Proceedings of the 2016 ACM Workshop on Automated Decision Making for Active Cyber Defense, co-located with CCS 2016). doi: 10.1145/2994475.2994482

Towards automated verification of active cyber defense strategies on software defined networks

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this