%0 Conference Proceedings
%T A model checking based approach for detecting SDN races
%+ Lomonosov Moscow State University (MSU)
%+ Département Réseaux et Services Multimédia Mobiles (TSP - RS2M)
%+ Institut Polytechnique de Paris (IP Paris)
%+ Méthodes et modèles pour les réseaux (METHODES-SAMOVAR)
%+ Centre National de la Recherche Scientifique (CNRS)
%+ Institute for System Programming of the Russian Academy of Sciences [Moscow] (ISPRAS)
%+ Réseaux, Systèmes, Services, Sécurité (R3S-SAMOVAR)
%A Vinarskii, Evgenii
%A Lopez, Jorge
%A Kushik, Natalia
%A Yevtushenko, Nina
%A Zeghlache, Djamal
%Z Part 4: Testing and Verification Techniques
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B ICTSS 2019: 31st IFIP International Conference on Testing Software and Systems
%C Paris, France
%Y Christophe Gaston
%Y Nikolai Kosmatov
%Y Pascale Le Gall
%I Springer International Publishing
%3 Testing Software and Systems
%V LNCS-11812
%P 194-211
%8 2019-10-15
%D 2019
%R 10.1007/978-3-030-31280-0_12
%K Races
%K Verification
%K Switch
%K Controller
%K Software Defined Networking (SDN)
%K Testing
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]
%Z Computer Science [cs]/Modeling and Simulation
%Z Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]Conference papers
%X The paper is devoted to the verification of Software Defined Networking (SDN) components and their compositions. We focus on the interaction between three basic entities, an application, a controller, and a switch. When the application submits a request to the controller, containing a set of rules to configure, these rules are expected to be ‘pushed’ and correctly applied by the switch of interest. However, this is not always the case, and one of the reasons is the presence of races or concurrency issues in SDN components and related interfaces. We propose a model checking based approach for deriving test sequences that can identify SDN races. The test generation strategy is based on model checking, and related formal verification is performed with the use of extended automata specifying the behavior of the components of interest; Linear Temporal Logic (LTL) formulas are utilized to express the properties to check. We generalize the races of interest and propose an approach for deriving the corresponding LTL formulas that are later used for verifiation. The Spin model checker is used for that purpose and thus, Promela specifications for interacting components are also provided; those are: the ONOS REST API, the ONOS controller and an OpenFlow Switch. An experimental evaluation with the aforementioned components showcases the existence of race conditions in their compositions.
%G English
%Z TC 6
%Z WG 6.1
%2 https://hal.science/hal-02448964/document
%2 https://hal.science/hal-02448964/file/482770_1_En_12_Chapter.pdf
%L hal-02448964
%U https://hal.science/hal-02448964
%~ INSTITUT-TELECOM
%~ CNRS
%~ TELECOM-SUDPARIS
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ TDS-MACS
%~ IFIP-ICTSS
%~ UNIV-PARIS-SACLAY
%~ TELECOM-SUDPARIS-SACLAY
%~ IP_PARIS
%~ INSTITUTS-TELECOM
%~ IFIP-LNCS-11812