25_Model Checking Software_Defined Networks with Flow Entries that Time Out.pdf (1.22 MB)
Model checking software-defined networks with flow entries that time out
Version 2 2023-06-07, 08:51
Version 1 2023-06-07, 07:26
conference contribution
posted on 2023-06-07, 08:51 authored by Vasileios Klimis, George ParisisGeorge Parisis, Bernhard ReusBernhard ReusSoftware-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
History
Publication status
- Published
File Version
- Published version
Journal
Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020ISSN
2708-7824Publisher
IEEEVolume
1Page range
179-184Event name
Formal Methods in Computer-Aided Design (FMCAD 2020)Event location
OnlineEvent type
conferenceEvent date
Sep. 21 - 24, 2020Place of publication
WienISBN
9783854480426Series
Conference Series: Formal Methods in Computer-Aided DesignDepartment affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2020-07-06First Open Access (FOA) Date
2020-10-20First Compliant Deposit (FCD) Date
2020-07-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC