Toward Formal Verification of SDN Access-Control Misconfigurations

Toward Formal Verification of SDN Access-Control Misconfigurations

Amina Saadaoui
Copyright: © 2019 |Pages: 16
DOI: 10.4018/978-1-5225-7353-1.ch006
OnDemand:
(Individual Chapters)
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

Abstract

Software-defined networking (SDN) allows centralizing and simplifying network management control. It brings a significant flexibility and visibility to networking, but at the same time creates new security challenges. The promise of SDN is the ability to allow networks to keep pace with the speed of change. It allows frequent modifications to the network configuration. However, these changes may introduce misconfigurations by writing inconsistent rules for single flow table or within a multiple open flow switches that need multiple FlowTables to be maintained at the same time. Misconfigurations can arise also between firewalls and FlowTables in OpenFlow-based networks. Problems arising from these misconfigurations are common and have dramatic consequences for networks operations. To avoid such scenarios, mechanisms to prevent these anomalies and inconsistencies are of paramount importance. To address these challenges, the authors present a new method that allows the automatic identification of inter and inter Flowtables anomalies. They also use the Firewall to bring out real misconfigurations.
Chapter Preview
Top

Recently, there have been many verification tools proposed for SDN. Some tools debug controller softwares or applications, while others check the correctness of network policies.

Controller Softwares or Applications Verification

In Canini et al. (2012), the authors propose a tool named NICE which automates the testing of OpenFlow Apps. In fact, it allows to find bugs in real applications and to test the atomic execution of system events. But this tool does not guarantee the errors absence and does not allow to check safety properties. Ball et al. (2014) propose another tool in named vericon that allows to verify the correctness of SDN applications on a large rang of topologies and sequences of network events. The limitation of this work is that authors focus on safety properties without verifying the liveness properties of packets (packets must eventually reach their destinations) and also, they assume that events are executed atomically ignoring out-of order rule installations.

Complete Chapter List

Search this Book:
Reset