Model checking software-defined networks with flow entries that time out

Klimis, Vasileios, Parisis, George and Reus, Bernhard (2020) Model checking software-defined networks with flow entries that time out. Formal Methods in Computer-Aided Design (FMCAD 2020), Online, Sep. 21 - 24, 2020. Published in: Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020. 1 179-184. IEEE digital library, Wien. ISSN 2708-7824 ISBN 9783854480426

[img] PDF - Accepted Version
Download (810kB)
[img] PDF - Published Version
Available under License Creative Commons Attribution.

Download (1MB)

Abstract

Software-defined networking (SDN) enables advanced operation and management of network deployments through (virtually) centralised, programmable controllers, which deploy network functionality by installing rules in the flow tables of network switches. Although this is a powerful abstraction, buggy controller functionality could lead to severe service disruption and security loopholes, motivating the need for (semi-)automated tools to find, or even verify absence of, bugs. Model checking SDNs has been proposed in the literature, but none of the existing approaches can support dynamic network deployments, where flow entries expire due to timeouts. This is necessary for automatically refreshing (and eliminating stale) state in the network (termed as soft-state in the network protocol design nomenclature), which is important for scaling up applications or recovering from failures. In this paper, we extend our model (MoCS) to deal with timeouts of flow table entries, thus supporting soft state in the network. Optimisations are proposed that are tailored to this extension. We evaluate the performance of the proposed model in UPPAAL using a load balancer and firewall in network topologies of varying size

Item Type: Conference Proceedings
Schools and Departments: School of Engineering and Informatics > Informatics
Related URLs:
SWORD Depositor: Mx Elements Account
Depositing User: Mx Elements Account
Date Deposited: 06 Jul 2020 14:12
Last Modified: 20 Oct 2020 13:35
URI: http://sro.sussex.ac.uk/id/eprint/92359

View download statistics for this item

📧 Request an update