Klimis2020_Chapter_TowardsModelCheckingReal-World.pdf (1006.18 kB)
Towards model checking real-world software-defined networks
Version 2 2023-06-12, 09:26
Version 1 2023-06-09, 21:03
conference contribution
posted on 2023-06-12, 09:26 authored by Vasileios Klimis, George ParisisGeorge Parisis, Bernhard ReusBernhard ReusIn 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.
History
Publication status
- Published
File Version
- Published version
Journal
Computer Aided Verification. CAV 2020. Lecture Notes in Computer SciencePublisher
Springer VerlagExternal DOI
Volume
12225Page range
126-148Event name
32nd International Conference on Computer-Aided VerificationEvent location
Los Angeles, California, USAEvent type
conferenceEvent date
July 19-24, 2020ISBN
9783030532901Series
Lecture Notes in Computer ScienceDepartment affiliated with
- Informatics Publications
Full text available
- No
Peer reviewed?
- Yes
Legacy Posted Date
2020-04-07First Open Access (FOA) Date
2020-07-28First Compliant Deposit (FCD) Date
2020-04-07Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC