Model Checking of Software Defined Networks using Header Space Analysis

Molari, Alessandro (2017) Model Checking of Software Defined Networks using Header Space Analysis. [Laurea], Università di Bologna, Corso di Studio in Ingegneria elettronica, informatica e telecomunicazioni [L-DM270] - Cesena
Documenti full-text disponibili:
[img] Documento PDF (Thesis)
Disponibile con Licenza: Creative Commons: Attribuzione - Non commerciale - Non opere derivate 3.0 (CC BY-NC-ND 3.0)

Download (4MB)


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.

Tipologia del documento
Tesi di laurea (Laurea)
Autore della tesi
Molari, Alessandro
Relatore della tesi
Correlatore della tesi
Corso di studio
Ordinamento Cds
Parole chiave
SDN,ONOS,OpenFlow,Security,Network,Model Checking,NetPlumber,HSA,Header Space Analysis
Data di discussione della Tesi
15 Dicembre 2017

Altri metadati

Statistica sui download

Gestione del documento: Visualizza il documento