dc.contributor.author | Klimis, V | |
dc.contributor.author | Parisis, G | |
dc.contributor.author | Reus, B | |
dc.date.accessioned | 2024-06-10T07:22:15Z | |
dc.date.available | 2024-06-10T07:22:15Z | |
dc.date.issued | 2020-07-14 | |
dc.identifier.citation | Klimis, V., Parisis, G., Reus, B. (2020). Towards Model Checking Real-World Software-Defined Networks. In: Lahiri, S., Wang, C. (eds) Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science(), vol 12225. Springer, Cham. https://doi.org/10.1007/978-3-030-53291-8_8 | en_US |
dc.identifier.issn | 0302-9743 | |
dc.identifier.uri | https://qmro.qmul.ac.uk/xmlui/handle/123456789/97361 | |
dc.description.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. | en_US |
dc.format.extent | 126 - 148 | |
dc.publisher | Springer Nature | en_US |
dc.rights | This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. | |
dc.title | Towards Model Checking Real-World Software-Defined Networks | en_US |
dc.type | Conference Proceeding | en_US |
dc.rights.holder | © 2020 The Author(s) | |
dc.identifier.doi | 10.1007/978-3-030-53291-8_8 | |
pubs.notes | Not known | en_US |
pubs.publication-status | Published | en_US |
pubs.volume | 12225 LNCS | en_US |
rioxxterms.funder | Default funder | en_US |
rioxxterms.identifier.project | Default project | en_US |
qmul.funder | Interface Reasoning for Interacting Systems::Engineering and Physical Sciences Research Council | en_US |