Klimis, Vassilis, Parisis, George and Reus, Bernhard (2020) Towards model checking real-world software-defined networks. 32nd International Conference on Computer-Aided Verification, Los Angeles, California, USA, July 19-24, 2020. Published in: Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science. 12225 126-148. Springer Verlag ISBN 9783030532901

	PDF - Accepted Version Restricted to SRO admin only Download (1MB)
	PDF (with appendix) - Accepted Version Restricted to SRO admin only Download (1MB)
	PDF - Published Version Available under License Creative Commons Attribution. Download (1MB)

Abstract

In software-defined networks (SDN), a controller program is in charge of deploying diverse network functionality across a large number of switches, but this comes at a great risk: deploying buggy controller code could result in network and service disruption and security loopholes. The automatic detection of bugs or, even better, verification of their absence is thus most desirable, yet the size of the network and the complexity of the controller makes this a challenging undertaking. In this paper, we propose MOCS, a highly expressive, optimised SDN model that allows capturing subtle real-world bugs, in a reasonable amount of time. This is achieved by (1) analysing the model for possible partial order reductions, (2) statically pre-computing packet equivalence classes and (3) indexing packets and rules that exist in the model. We demonstrate its superiority compared to the state of the art in terms of expressivity, by providing examples of realistic bugs that a prototype implementation of MOCS in Uppaal caught, and performance/scalability, by running examples on various sizes of network topologies, highlighting the importance of our abstractions and optimisations.

Item Type:	Conference Proceedings
Schools and Departments:	School of Engineering and Informatics > Informatics
SWORD Depositor:	Mx Elements Account
Depositing User:	Mx Elements Account
Date Deposited:	07 Apr 2020 10:45
Last Modified:	28 Jul 2020 14:26
URI:	http://sro.sussex.ac.uk/id/eprint/90723

View download statistics for this item

📧 Request an update