Model Checking of Software Defined Networks using Header Space Analysis

This thesis investigates the topic of verifying network status validity with a Cyber Security perspective. The fields of interest are dynamic networks like OpenFlow and Software Defined Networks, where these problems may have larger attack surface and greater impact. The framework under study is called Header Space Analysis, a formal model and protocol-agnostic framework that allows to perform static policy checking both in classical TCP/IP networks and modern dynamic SDN. The goal is to analyse some classes of network failure, declaring valid network states and recognizing invalid ones. HSA has evolved in NetPlumber, to face problems caused by high dynamics of SDN networks. The main difference between HSA and NetPlumber is the incremental way that the latter performs checks and keeps state updated, verifying the actual state compliance with the expected state defined in its model, but the concept is the same: declare what's allowed and recognize states violating that model. The second and main contribute of this thesis is to expand existing vision with the purpose of increasing the network security degree, introducing model-checking-based networks through the definition of an abstraction layer that provides a security-focused model-checking service to SDN. The developed system is called MCS (Model Checking Service) and is implemented for an existing SDN solution called ONOS, using NetPlumber as underlying model-checking technology, but it's validity is general, uncoupled with any kind of SDN implementation. Finally, the demo shows how some cases of well-known security attacks in modern networks can be prevented or mitigated using the reactive behavior of MCS.