Abdul Majith

Ocan Sankur
email: ocan.sankur@irisa.fr

Hervé Marchand
email: herve.marchand@inria.fr

Thai Dinh
email: dinhthai.bui@nokia-bell-labs.com

Bui

Compositional model checking of SDN platform

Keywords: SDN, slice, compositional checking, verification, isolation, safety

Software-Defined Network (SDN) technology provides the possibility to turn the network infrastructure into a dynamic programmable fabric capable of meeting the application needs in real-time. Thanks to the independence of the control plane from the data plane, the control entity, generally called as controller, has also the flexibility to implement proprietary complex algorithms. Within such a dynamic and complex environment, this document advocates for applying formal verification methods and more precisely composition model checking to ensure the correct behavior of the overall SDN system at design phase. To illustrate this purpose, it proposes to build different comprehensive formal models of a typical SDN platform selected here as a study object. Thorough performance results related to each model are provided and discussed. Thanks to such formal verifications, it is possible to pinpoint issues such as the one regarding network isolation within a complex SDN architecture. Although dealing with formal methods, this document attempts to strike a balance between theory, experimental work and network architecture discussion.

I. INTRODUCTION

The flexibilty of Software-Defined network (SDN) together with the implementation of new complex network algorithms raises new challenges in term of validation and verification. Formal verification methods which are capable of exhaustively checking the behaviors of a given system have been applied in the setting of SDNs (see Section II). We also advocate for applying formal verification methods to ensure the correct behavior of an SDN platform especially during the design phase. More precisely, we demonstrate that compositional model checking is well-adapted to model and verify SDN architectures with all their different layers or planes, namely the data plane, the control plane and the management plane. For this purpose, we propose to build complete models of a typical SDN architecture taken here as a study object. Compositional modeling allows for designing and verifying each layer separately from others leading to a more modular and more scalable verification mechanism. Our contribution is fourfold. First, we present a comprehensive formal model of the SDN platform published in [START_REF] Boussard | Softwaredefined lans for interconnected smart environment[END_REF]. We model respectively devices and their mobility, switches and the network topology on the data plane, controllers on the control plane and managers on the management plane. We model communications between components of the same planes (i.e. between devices and switches) as well as those in different planes. Second, we demonstrate that compositional reasoning is well-adapted to model-check SDN by decomposing the overall complex system verification into the sum of simpler verifications of the different components. We perform both a vertical (e.g. between planes) and a horizontal (e.g. between devices and switches) decomposition during model checking. Note that our approach consists in model checking the system model offline, that is, exhaustively checking all possible behaviors of the model before deployment. Third, we show that it is possible to verify complex scenarios such as to discover a network slice isolation violation. Finally, we propose a method and related architecture to avoid the issue previously discovered and verify that such a method is valid. After going through state-of-the-art in Section II, we describe the SDN platform of [START_REF] Boussard | Softwaredefined lans for interconnected smart environment[END_REF] taken as a study object in Section III. In Section IV we develop a complete formal model of the studied platform in the form of automata. An implementation of such automata is also proposed in Section V using a tool called Spin [START_REF] Holzmann | The SPIN model checker: Primer and reference manual[END_REF]. In the same section, we argue that compositional reasoning is well appropriate for SDN and propose the application of such reasoning to our previous formal model. Most of experimental works are carried out in Section VI where we discuss on performance of different verification methods according to model sizes while assuming devices are not moving (i.e. no mobility condition). The model with device mobility in Section VII allows us to pinpoint a network slice isolation issue. We finally propose a solution to correct the isolation violation and formally verify that the solution is valid.

II. RELATED WORK

The closest to our work is that of [START_REF] Majumdar | Kuai: A model checker for software-defined networks[END_REF] which presents a tool called Kuai. The latter applies optimizations based on partialorder reduction to simplify the models of SDN protocols, and presents several model checking benchmarks to assess the performance of its optimizations. The tool translates formal models given in the Murphi input format and uses PReach [START_REF] Bingham | Industrial strength distributed explicit state model checking[END_REF] for distributed model checking. One of its optimizations is based on barriers which are used to ensure the order in which switches implement SDN rules. We do not consider barriers in our platform since our SDN rules are applied asynchronously. Also, Kuai uses (0, ∞)-abstractions on packet queue contents which consist in storing whether a given packet is absent (0) or present an unknown number of times (∞). Since we present an abstract model by focusing on particular packets, we do not use this abstraction in our work. Our entire SDN platform is an asynchronous distributed system where various components are with finite number of FIFO queues. There is no priority on queues while reading incoming messages. Instead, each component reads messages by performing queue polling in a round robin fashion. We can model the system mathematically as a synchronous one by encoding state space along with current queue message contents. In an asynchronous system, barriers optimizations and partial order techniques might be used but verifications have to be performed on such abstractions in order to check that they preserve the safety properties. Indeed, reading various messages among different incoming queues in different orders might lead to different results (see the case study described in Section VII).

With regards to experimental tools, we have selected a tool called as SPIN (Simple Promela INterpreter) which has the advantages of implementing in-build partial order techniques. It spares modelers from having to write specific codes to implement partial order techniques while specifying the behaviors of the SDN platform. As per our knowledge, the use of compositional reasoning for SDN protocols is new -e.g. compared to [START_REF] Majumdar | Kuai: A model checker for software-defined networks[END_REF]. Moreover, we consider the SDN architecture with a management plane which renders the system to be analyzed more comprehensive and more complex. To our knowledge, this is the first time compositional reasoning is used to verifying SDN protocol correctness. However, this method has some limitations as one has to guess intermediate formula (See Section V) If such intermediate and global properties are only safety properties then finding such intermediate formulas can be automated for such automated procedure by using e.g. Learning ω-Regular languages [START_REF] Farzan | Extending automated compositional verification to the full class of omegaregular languages[END_REF].

Several other works consider the formal analysis of SDN protocols. [START_REF] Kazemian | Header space analysis: Static checking for networks[END_REF] provides a static analysis of header spaces which detect inconsistencies in routing tables, but does not consider more dynamic behaviors and complex issues due to interleavings as it is done in [START_REF] Majumdar | Kuai: A model checker for software-defined networks[END_REF] and in our work. A similar approach was adopted in [START_REF] Mai | Debugging the data plane with anteater[END_REF]. A modeling language called FlowLog tailored for SDN protocols was given in [START_REF] Nelson | A balance of power: Expressive, analyzable controller programming[END_REF] in which the authors present model checking experiments with the SPIN model checker [START_REF] Holzmann | The SPIN model checker: Primer and reference manual[END_REF] but no particular optimizations are presented. In [START_REF] Canini | A nice way to test openflow applications[END_REF], model checking and symbolic execution are combined in order to check OpenFlow applications for a given number of packets. [START_REF] Sethi | Abstractions for model checking sdn controllers[END_REF] presents data and network abstractions applied on SDN models combined with a manual refinement process based on non-interference lemmas.

In [START_REF] Ball | Vericon: towards verifying controller programs in software-defined networks[END_REF], the authors develop a framework where the system is modeled using first-order logic, and user-provided inductive invariants are checked to prove correctness. This allows one to check the system for all network topologies, and for an unbounded number exchanged packets.

The approach developed in [START_REF] Zou | Veriflow: Verifying network-wide invariants in real time[END_REF] consists in checking the effect of rule updates in real-time, without affecting the system performance. This is complementary to offline verification approaches which analyze the system globally before execution.

In [START_REF] Wang | Automated synthesis of reactive controllers for software-defined networks[END_REF], reactive synthesis is used to automatically synthesize network update rules in response to network requests. Other works consider the synthesis of update rules that makes sure that the intermediate configurations during the update are all admissible [START_REF] Reitblatt | Abstractions for network update[END_REF], [START_REF] Mcclurg | Efficient synthesis of network updates[END_REF], or compute correct networkwide configurations [START_REF] El-Hassany | Network-wide configuration synthesis[END_REF]. The procedure described in [START_REF] Reitblatt | Abstractions for network update[END_REF] allow to automatically synthesize network updates but are only described at a theoretical level and its deployment to realtime system procedure is difficult. Because, in the proposed solution, each subsystem need the approval of the global system in order to deploy new rules (ths is performed by the use of a so-called wait command. Such mechanism is possible in asynchronous system whenever the protocol have an authentication mechanism or at least timestamp needs to be added within the exchanged messages.

Abstractions and other transformations that preserve the properties of networks for rendering the verification more efficient are presented in [START_REF] Plotkin | Scaling network verification using symmetry and surgery[END_REF]. In this work, we are interested to provide the methodology to use compositional reasoning to verify SDN platform correctness. Properties selected for verification are estimated by the authors as critical for a good behavior of an SDN platform. Naturally, compositional reasoning is a well-adapted verification analysis for SDN, since SDN platforms consist in a clear separation between control, management and data planes. In order to ensure that the SDN platform satisfies global properties, it is sufficient to verify that each plane satisfies specific local properties, which makes the model checking procedure scalable with respect to time and space complexity. This methodology also allows for analyzing and designing successively each individual component in a iterative manner of whole complex system.

III. THE SDN PLATFORM DESCRIPTION

In this document, we build a formal and abstract model of the SDN platform [START_REF] Boussard | Softwaredefined lans for interconnected smart environment[END_REF] which is taken here as a study object. We think that this SDN platform has a representative architecture to make our study as generic as possible.

A. Architecture Building Blocks

As most of SDN platforms, SDN platform [START_REF] Boussard | Softwaredefined lans for interconnected smart environment[END_REF] consists of three layers, namely a management plane, a control plane and a data plane. The management plane are formed of entities called 'managers'. Each manager has the role of interfacing with the user and of converting the user's intents into high level network policies. The control plane consists of entities called 'controllers' which have the role of converting managers' high level network policies into fine grain network rules and of enforcing those rules onto the data plane. The data plane consists of network elements embodied in the selected platform as Open vSwitches (OVS) [START_REF] Foundation | [END_REF]. OVSes are opensource OpenFlow switches [START_REF] Foundation | Openflow switch specification -version 1[END_REF] controlled by SDN controllers.

The platform is made of several administrative domains with each domain built up with one manager, one controller and several switches (i.e. OVSes). A given switch can only be part of one unique domain so that switches of all domains form a partition of the overall data plane. In order to simplify the controller algorithm in the forwarding of multicast/broadcast messages, the data plane topology of each domain is loopfree (the LLDP and the spanning-tree mechanisms should be added to the controller logics if non loop-free topologies are considered. This is part of our next steps). In this document, such a topology is a tree topology departing from a root switch. The latter is the domain border switch. Root switches of all domains are interconnected together in a full meshed topology so that there is only one network hop between any pairs of root switches. Figure 1 provides us with a schematic representation of the SDN platform.

The data plane is also completed with devices. Each of them can be connected to a switch port called as an Accessport via a network link called as an Access-link (thin green links). Similarly, switches within a domain are connected together via network links called as Intra-links (medium-size green links) thanks to their Intra-ports. Root switches from different domains are interconnected together via Inter-links (thick green links) thanks to their Inter-ports.

B. The User's Intent

The user's intent consists in a set of predicates on device characteristics or device capabilities [START_REF] Peloso | Enforcing users' constraints in dynamic, software-defined networks of devices[END_REF]. This set of predicates or intent allows the user to select devices and gather them into a private group called in the following sections as Virtual Space or VS. Devices of the same VS are to be connected together by controllers on the different domains where these devices are detected (i.e. via the MAC learning process). A VS is enforced by the control plane as a network slice in the data plane. While enforcing OpenFlow rules, controllers should make sure that a pair of devices which do not belong to any common VS are not connected together. This is defined as the network slice isolation property or isolation property for short (i.e. data traffic isolation between network slices) in this document. For the sake of simplicity, the user's intent will be presented in the rest of the document as a nominative list of devices -e.g. {d1, d2, d3}. This is done without losing the genericity of our discussions since the present verification work is not focusing on the consistency of the overall users' intents but rather on the safety of the underlying SDN mechanisms. Moreover, we do not present details on how the controller which identifies a given device by its MAC address, and the associated manager which identifies the same device by its name, agree with each other on the device identity, as per the limited size of the document. Please refer to [START_REF] Boussard | Softwaredefined lans for interconnected smart environment[END_REF] for further information.

C. Device Discovery via MAC Learning

The controller implements the well-known MAC learning mechanism as per [START_REF] Foundation | Open vswitch advanced features[END_REF]. Thanks to this mechanism, the controller can discover newly connected device (e.g. new MAC address) and inform the associated manager. In return, it receives from the manager high level network policies (derived from users' intents) regarding the new device.

Once the new device has been discovered by the domain controller, the latter 'leaks' multicast/broadcast packets from the former to all neighbor domains where devices of the same VS are located (and only to those domains). Such packets are treated as MAC learning packets in such neighboring domains, meaning that they are flooded within the aforementionned domains except to their Access-ports. The leaking process is triggered thanks to knowledges coming from managers which synchronize between them, VS predicate and device location. In order to avoid forwarding loops during the leaking process, controllers apply a simple algorithm known as the split horizon algorithm. Within such an algorithm, a root switch never forwards to other root switches a packet it has received from another root switch. The split horizon algorithm does properly ensure reachability between domain given that we have a full mesh topology between root switches.

The work in this document is modeling the above device discovery procedure through MAC learning at all planes.

D. Packet Forwarding

A unicast packet with source MAC address 'S' and destination MAC address 'D' is forwarded if MAC addresses 'S' and 'D' are considered as part of the same VS (assuming the right mapping between MAC addresses and device names as discussed previously). Otherwise, the packet is dropped.

Concerning multicast (including broadcast) packets, the controller derives a multicast tree for each source MAC address 'S' [START_REF] Bui | Supporting multicast and broadcast traffic for groups of connected devices[END_REF] based on the different VSes this MAC address 'S' belongs to. In order to avoid network loops when forwarding multicast packets over Inter-links, each domain controller implements the well-known split horizon algorithm taking into account the full mesh nature of the Inter-links topology. The split horizon algorithm simply consists in not forwarding to other Inter-links a packet coming from an Inter-link.

Apart from multicast packet forwarding, all the data plane including unicast forwarding and flooding mechanism which is part of the MAC learning process is modelled during this work. As it concerns the control plane and the management plane, their essential behaviors are completely captured by the models described in this document.

IV. AUTOMATA-BASED FORMAL MODELS

We formalize our model using finite automata. We start by introducing the formalism, and then describe the formal model of SDN platform.

A. Preliminaries

Definition IV.1. Automaton: an automaton is a tuple of the form (Q, q init , Σ∪{τ }, ∆, L), where Q is the finite set of states, q init ∈ Q is the initial state, Σ = Σ in ∪ Σ out is the alphabet and τ a distinguished symbol for internal transition, ∆ : Q × Σ ∪ {τ } → Q is the transition relation, and L : Q → 2 AP is a labeling function with AP a given set of atomic predicates.

A transition δ = (q, σ, q ) ∈ ∆ will also be written as q σ -→ q if δ is clear from the context. Moreover, for better readability, we will use σ! if σ ∈ Σ out , and σ? if σ ∈ Σ in . This is only to help the reader; formally the label does not contain the symbols ? and !.

Definition IV.2. Synchronized product of automata: given automata

A i = (Q i , q i init , Σ i ∪ {τ }, ∆ i , L i ) for i ∈ {1, . . . , n}, the synchronized product of A i is defined as A = A 1 . . . A n = (Π n i=1 Q i , (q 1 init , . . . , q n init ), Σ ∪ {τ }, ∆, L) where Σ = ∪ n i=1 Σ i , L : Π n i=1 Q i → (2 AP1 , .
., 2 APn ) s.t L(q 1 , q 2 , .., q n ) = ( L 1 (q 1 ), .., L n (q n ) ), and ∆ is defined as follows. For all states (q 1 , . . . , q n ) ∈ Π n i=1 Q i , • for all 1 ≤ i ≤ n, and q i ∈ Q i such that ∆ i (q i , τ, q i ), ((q 1 , . . . , q i , . . . , q n ), τ, (q 1 , . . . , q i , . . . , q n )) ∈ ∆, • for all σ ∈ Σ, writing

I σ = {1 ≤ i ≤ n | ∃q i ∈ Q i , ∆ i (q i , σ, q i )}, (q 1 , . . . , q n ) σ -→ (q 1 , . . . , q n ) if,
and only if for all i ∈ I σ , ∆ i (q i , σ, q i ), and for all i ∈ I σ , there exists no q i such that ∆ i (q i , σ, q i ).

In our automata, the set AP contains predicates Sync(σ) for all labels σ ∈ Σ, such that Sync(σ) is true iff the previous transition was labeled by σ. Note that these predicates appear in several components but all states of the product agree on their values by definition of the synchronized product.

B. Important Concepts

An instance of the platform is defined by providing the topology for different planes. Recall that there is exactly one manager associated to each controller. Each controller only communicates with its own manager and the switches in its domain. Managers are interconnected together via a complete graph of communication.

Formally, consider a set of controllers Cont = {c 1 , . . . , c k }, a set of managers Man = {man 1 , . . . , man k } with the same cardinal, and a set of switches Sw = Sw 1 ∪ . . . ∪ Sw k given as a partition. Within the selected platform, the switches of Sw i belong to the domain i which is controlled by the controller c i . The latter is itself managed by man i . We consider a set Dev of devices which can connect to switches of different domains.

In each domain i, there is one designated switch called the root switch, denoted by root i ∈ Sw i . The data plane topology is a graph G = (Sw, E) such that the subgraph restricted to each Sw i is an undirected tree rooted at root i , and the subgraph induced by the set of roots {root 1 , . . . , root k } is a complete graph.

In our studied platform, we distinguish so-called Accessports through which devices connect to switches. We also have Intra-ports which are used to interconnect switches that belong to the same domain, and Inter-ports which are used to interconnect root switches of different domains. We also define a finite set Pts which refer to the set of Access-ports available at all switches.

Platform instance: an instance of the studied platform is defined as a tuple (Man, Cont, Sw, G) where: ,E) is the topology graph as explained above. We also use the function cont : Sw → Cont which identifies the controller associated to each switch, thus determining its domain: for all i ∈ {1, . . . , k} and v ∈ Sw i , we have cont(v) = c i .

• Man = {man 1 , . . . , man k }, • Cont = {c 1 , . . . , c k }, • Sw = k i=1 Sw i , • G = (Sw
Virtual Spaces (VSes): we consider the covering of Dev by the set of Virtual Spaces

VS = {V 1 , V 2 , .., V f }, with V i ⊆ Dev for all 1 ≤ i ≤ f , and ∪ l i=1 V i = Dev. Let us define the function VS(x) = {V ∈ VS | x ∈ V }
which assigns to each device x the set of VSes to which x belongs.

Exchanged Data Packets: two types of packets are exchanged between switches and devices. MAC learning packets are sent by devices and forwarded by switches, and they contain the device identifier; while ping packets contain the source and target device identifiers.

These are defined, respectively, as MacPkts = {mac}×Dev and PingPkts = {ping} × Dev × Dev. These packets will be written as mac(x) and ping(x, y) respectively, for x, y ∈ Dev.

Exchanged Control Packets: let us define ManPkts = Dev × {1, .., k} × 2 VS a set of packets from the management plane to the controller plane and ContPkts = {(man i , c i )|i ∈ {1, .., k}}×Dev is the set of packets from the controller plane to the management plane.

It is noted that MacPkts forwarded by switches to the associated controllers are also part of exchanged control packets.

OpenFlow Rules: controller sends two types of rule updates to switches.

Rules impacting the forwarding of ping packets are defined as PingRules = Dev × Dev × (Pts ∪ Sw) where the triple contains the source and target devices identifiers and the port or the switch to forward to.

Rules impacting the forwarding of MAC learning packets are MacRules = Dev × Sw where the pair contains the identifier of the device that has generated the mac learning packet, and the switch to forward to.

We let Rules = PingRules ∪ MacRules. Notice that we use switch identifiers as destinations instead of Intra-port identifier or Inter-port identifier to which both ping and MAC packets are forwarded to. This is because switch identifiers are used as port numbers for the communication between switches (see more detailed in section IV-C2).

C. Automata Models

We now describe the different automata that respectively model devices, switches, controllers, and managers. We completely define the related state space but only provide descriptive information on the related transitions.

We denote the set of words on the alphabet A by Seq(A) = A * , while the empty word is . This notation will be used to encode packet queues in the automaton below. Note that we describe unbounded packet queues in our formal model, although the real platform uses bounded ones (see below).

1) Automaton for Devices: We define an automaton A Dev that describes the behaviors of the whole set of devices Dev. The automaton stores the positions (i.e. the Access-port which a device is connected to) of all devices, transmits MAC learning and ping packets, receives pings packets and allows devices to change positions. Moreover, the automaton also stores the set of ping packets that have been sent, and the set of ping packets that have been received by each device since the start. This information is used to check whether transmitted and received packets match the verification specifications. We restrict to the case where each device pings at most once any other device.

The device state space contains:

• a position function pos of type Dev → (Pts × Sw) ∪ {⊥} which assigns each device a switch and an Access-port if it is connected, and ⊥ otherwise; • a set spings ⊆ PingPkts which stores sent ping packets; • a set rpings x ⊆ PingPkts each device x which stores received ping packets. Initially, these spings and rpings x for all x ∈ Dev sets are empty, and pos maps all devices to ⊥. Intuitively, a device x can send ping or MAC learning packets m to the switch v through port p (this has the form (x, v, p, (mac, x)) or (x, v, p, (ping, x, y))), and they can receive ping packets m from switch v via port p (this has the form (v, p, (ping, z, x))). The latter does not contain the device identifier. In fact, this packet is forwarded by OVS v to port p, and any device that is connected to this port at that moment receives the packet.

Moreover, a device sends a new MAC learning packet whenever it changes its position.

The automaton A Dev has the following transitions.

Changing position and sending a MAC learning packet: q

(x,v,p,mac(x))! ---------→ q [pos ← pos[x → (v, p)]], for all p ∈ Pts, v ∈ Sw, x ∈ Dev.
Sending a ping packet: q

(x,v,p,ping(x,y))! -----------→ q [spings ← spings ∪ {ping(x, y)}],
for all x ∈ Dev and ping(x, y) ∈ spings, Receiving a ping packet: q (v,p,ping(x,y))?

----------→ q [rpings z ← rpings z ∪ {ping(x, y)}] for all v ∈ Sw, p ∈ Pts and pos(z) = (v, p).

2) Automaton for Switches: Here we define an automaton A Sw that captures the behaviors of all the switches. Remember that we use switch identifiers as destinations instead of Intraport identifier or Inter-port identifier to which both ping and MAC packets are forwarded to. This is because switch identifiers are used as port numbers for the communication between switches.

For simplicity of modeling and to reduce the state space, we abstract away from port numbers for communication between switches, and use switch identifiers instead. For instance, while flow tables are used to map packets to ports to forward to in the real system, our flow tables map packets to switch identifiers except when the outgoing port is an Access-port. This is without loss of generality since a switch identifier determines the port to which it is connected and vice versa (once the topology between switches is defined). Moreover, as mentioned in the beginning of this section, we omit outgoing packet queues, and assume that sending a packet consists in writing directly in the incoming packet queue of the recipient switch.

The automaton contains for each switch v ∈ Sw the following components:

• ping packet forwarding rules pfwd v : Dev×Dev → Sw∪ Pts∪{⊥} that is a partial function which, for a given ping packet ping(x, y) from device x to device y, assigns a switch or an Access-port to forward to; • MAC learning packet forwarding rules mfwd v : Dev → 2 Sw which gives the set of switches to which to forward the MAC learning packet received from given device; • a data packet queue dque v of type Seq(MacPkts ∪ PingPkts) to store packets received from other switches; • and a control packet queue cque v of type Seq(Rules) that stores rule packets coming from the controller. The switches receive MAC learning or ping packets from devices (packets of the form (x, v, p, m)) which are put to dque v . They forward MAC learning packets they have received to the controller (packets of the form ((v, cont(v)), (p, mac(x)))), and receive new rule updates from the controller (packets of the form (cont(v), v, r)), which are put into cque v .

Initially, pfwd v is empty, and mfwd v maps all devices to the set of neighboring switches of the same domain, that is,

mfwd v (x) = {v ∈ Sw i | cont(v) = cont(v ) ∧ (v, v ) ∈ E} for all x ∈ Dev.
Moreover, all queues dque v and cque v are empty at the initial state.

When processing a MAC rule, the process pops a packet (x, p) from the queue cque v , updates and triggers its mfwd v function to forward MAC learning packets for device x to all neighboring v switches. Similarly, when processing a ping rule (x, y, p), the flow table pfwd v function is updated and triggered so that ping packets from x to y are forwarded to p.

The process forwards MAC learning packets (p, mac(x)) to all neighbor switches v (except the switch p where the packet comes from) in mfwd v (x), but it also forwards it to the controller, via the synchronizing transition (with label ((v, cont(v)), (p, mac(x))).

When a root switch receives a MAC learning packet from another root switch (i.e. of another domain), the former only forwards the packet to its domain as per the previously described split horizon principle in order to avoid loops.

Forwarding ping packets are internal transitions. A packet ping(x, y) is forwarded by pfwd v (x, y) if this value is defined otherwise the packet is dropped. Transitions for A Sw are defined as follows.

Receiving a packet from the controller: q

((cont(v),v),r)? ---------→ q [cque v ← cque v • r]
, for all r ∈ Rules Receiving a MAC learning packet from a device: q

(x,v,p,mac(x))? ---------→ q [dque v ← dque v • (p, mac(x))]), for all x ∈ Dev, p ∈ Pts.
Receiving a ping packet from a device: q

(x,v,p,m)? -------→ q [dque v ← dque v • m]), for all x ∈ Dev, p ∈ Pts, m ∈ PingPkts, Processing a MAC rule: q [cque v = (x, v ) • cque v ] τ -→ q [mfwd v ← mfwd v [x → mfwd v (x) ∪ {v }]],
Processing a ping rule:

q [cque v = (x, y, p) • cque v ] τ -→ q [pfwd v ← pfwd v [(x, y) → p], cque v ← cque v ], for all x, y ∈ Dev, p ∈ Pts ∪ Sw.
Forwarding a MAC learning packet:

q dque v = (p, mac(x)) • dque v ((v,cont(v),(p,mac(x)))! --------------→ q dque v ← dque v , ∀v ∈ S , dque v ← dque v • (v, mac(x)) , where p ∈ Pts ∪ Sw; if p is not a root switch root j , then S = mfwd v (x) \ {p}, else S = mfwd v (x) ∩ Sw i with i = j.
Forwarding a ping (to OVSs):

q dque v = ping(x, y) • dque v τ -→ q dque v ← dque v • ping(x, y), dque v ← dque v , for all v = pfwd v (x, y) ∈ Sw,
Forwarding a ping (to devices): q dque v = ping(x, y) • dque v (y,v,p,ping(x,y)! ----------→ q dque v ← dque v , for all p = pfwd v (x, y) ∈ Pts, Note that in our model, packet communication between switches is modeled by directly writing in the packet queues of receiving switches.

The state space of the controllers also have Boolean variables toggle to indicate whether a ping update message has been sent to switches already.

3) Automaton for Controllers: We define automaton A Cont that describes the behaviors of the entire control plane.

The state space contains for each controller c i the following components:

• a device relative position function rpos i of type Dev × Sw j Pts∪Sw∪{⊥} which gives the position of a given device at the given switch as known to the controller c i , that is, the port from which the MAC learning packet from the device is received and to which ping packets for the device are to be forwarded at that switch.

• a device information function dinfo i of type Dev {1, . . . , k} × 2 VS which stores the domain and Virtual Spaces to which each device belongs; • a queue cdque i of type Seq(Sw i × Pts × MacPkts) that stores packets that arrive from the data plane,

• and a queue mque i of type Seq(ManPkts) that stores packets that arrive from the management plane. Initially, partial functions rpos i and dinfo i , and both queues are empty.

Packets that come from the management plane are put in mque i , while MAC learning packets from the data plane are put in cdque i . When processing a MAC learning packet (v, p, mac(x)), the controller updates its rpos i function to store the relative position p of the device x at a given switch v. When processing a packet (x, dom, V ) from the management plane, the controller updates its dinfo i function to store the fact that device x belongs to domain dom and VS V . Furthermore, the controller sends ping rule updates of the form (x, y, p) to the switches whenever devices x and y belong to a common VS, and rpos i (y, v) = p. This ensures that ping packets with destination y be forwarded to p at switch v. Finally, the controller also sends MAC learning rule updates to root switches. It sends the rule (x, root j ) to switch root i whenever device x is known to belong to domain i and there exists some device y in domain j which share a common VS with x. This ensures that MAC learning packets will be forwarded from domain i to domain j.

The transitions of A Cont are defined as follows.

Receiving a packet from the management plane: q

(mani,ci,(x,dom,V ))? -------------→ q [mque i ← mque i • (x, dom, V )] for all x ∈ Dev, 1 ≤ dom ≤ k, V ⊆ VS.
Receiving a MAC packet from the data plane: q

((v,ci),(p,mac(x)))? ------------→ q [cdque i ← cdque i • (v, p, mac(x))], for all x ∈ Dev, v ∈ Sw i , p ∈ Pts ∪ Sw.
Processing a Mac learning packet (from IOT port):

q cdque i = (v, p, mac(x)) • cdque i (ci,mani,x)! -------→ q rpos i ← rpos i [(x, v) → p], cdque i ← cdque i , toggle = false, for all v ∈ Sw i , p ∈ Pts.
Processing a Mac learning packet (from Non-IOT port):

q cdque i = (v, p, mac(x)) • cdque i τ -→ q rpos i ← rpos i [(x, v) → p], cdque i ← cdque i , toggle = false, for all v ∈ Sw i , p ∈ Sw.
Processing a packet from man i :

q [mque i = (x, dom, V ) • mque i ] τ -→ q [dinfo i ← dinfo i [x → (dom, V )], mque i ← mque i ], toggle = false, for all x ∈ Dev, 1 ≤ dom ≤ k and V ⊆ VS.
Sending ping rule updates to switches:

q [toggle == false] (ci,v,(x,y,p))! ---------→ q [toggle = true] for all x, y ∈ Dev, v ∈ Sw i , rpos i (y, v) = p = ⊥, and writing dinfo i (x) = (j x , V ), dinfo i (y) = (j y , V ) and V ∩ V = ∅.
Sending MAC rule update to root i : q (ci,rooti,(x,rootj ))! -----------→ q for all x ∈ Dev such that rpos i (x, root i ) = ⊥ ∧ dinfo i (x) = (i, V ), and there exists y ∈ Dev s.t. dinfo i (y) = (j, V ) with j = i and V ∩ V = ∅.

4) Automaton for Managers: We define automaton A man that describes the behaviors of the entire management plane. The state space contains for each management node man i the following components:

• a mapping function dinfo i : Dev → {1, . . . , k} ∪ {⊥} determining the domain in which the device is connected. • a packet queue cque i that stores packets that come from c i ; • and a queue mque i for packets from other management nodes. Initially, both queues are empty and dinfo i maps all devices to ⊥.

The management node man i learns about the domains to which devices belong through packets received from the controller c i , and forwards this information to all other management nodes. More precisely, packets sent by the controllers are put in the queues cque i . When processing a controller packet for device x ∈ Dev, the manager man i sends the packet (x, i) to all other managers informing them that device x belongs to domain i. This helps all management nodes to eventually have full information on the domain where each device is located. Moreover, the management node man i sends to the controller c i the VSes to which each known device belongs by sending packets of the form (x, dom, V ) where x is a device, dom its domain, and V the set of VSes to which the device x belongs. The transitions of A man are defined as follows.

Receiving controller packet: q

(ci,mani,x)? -------→ q [cque i ← cque i • x]. where x ∈ Dev Processing a controller packet: q [cque i = x • cque i ] τ -→ q ∀j = i, mque j ← mque j • (i, x), dinfo i ← dinfo i [x → i], cque i ← cque i . where x ∈ Dev and 1 ≤ j ≤ k.
Processing a management packet:

q [mque i = (j, x) • mque i ] τ -→ q [dinfo i ← dinfo i [x → j], mque i ← mque i ].
Sending device information to controller: q (mani,ci,(x,j,V ))! -----------→ q for all x ∈ Dev, 1 ≤ j ≤ k such that dinfo(x) = j and V = VS(x).

V. FORMAL VERIFICATION

During the following work, we use linear temporal logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] to specify different system properties including the ones that we want to verify. LTL is build over propositional logic (based on Boolean operators ¬,∨,∧) by adding the notion of discrete (i.e natural number) timeline and temporal operators such as the following { , ♦ } just to name the ones we use here:

• ψ means ψ is True in all future moments • ♦ψ means ψ is True in some future moments LTL formulas are built over a finite set of propositional variables referred to as Atomic Propositions (AP) combined with aforementioned Boolean and temporal operators. Temporal operators can be nested. For instance ♦φ refers to executions in which at all moments, there is a moment in future where φ holds; thus, φ holds at infinitely many points in time. Formula ♦ φ refers to executions in which there is a moment in time after which φ holds at all positions; thus φ becomes an invariant after a while. We use the finite trace semantics of LTL [START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF] without next operators denoted by LTL f \ X.

A. Property Specifications

We verify two important properties of our platform. The first is a safety property, called as the isolation property. It states that only devices that belong to a common VS can exchange ping packets and a device not belonging to a particular VS cannot eavesdrop ping packets exchanged among that VS group. This can be expressed in LTL as follows.

Isolation =

x,y∈Dev, VS(x)∩VS(y)=∅ ping(x, y) ∈ rpings y x,y,z∈Dev, z =y ping(x, y) ∈ rpings z .

This LTL formula thus describes the set of executions which never enter a state where a packet ping(x, y) with VS(x) ∩ VS(y) = ∅ is received, and no device can eavesdrop the packet which as to be received by different devices.

The second property is called as the connectivity property.

It states that whenever a ping packet is sent to a device that belongs to a same VS group, the packet is eventually received; however this property only holds after some point in time, that is, when the MAC learning algorithm has finished. So the SDN platform eventually allows a common VS group to exchange the data packets among themselves. This can be expressed in LTL as follows:

Connect = x,y∈Dev VS(x)∩VS(y) =∅ ♦ ping(x, y) ∈ spings ∧ ♦ping(x, y) ∈ rpings y .
In our work we consider two scenarios. In the no-mobility scenario, devices do not change their respective position once they are connected to an Access-port. In the mobility scenario, devices can change their position at any time.

The first scenario called as Nomobility can be expressed in LTL as follows:

Nomobility = x∈Dev,v∈Sw, p∈Sw∪Pts (v, p) = pos(x) → (v, p) = pos(x)

B. Compositional Reasoning

We present here a compositional reasoning methodology which allows one to model check a system by decomposing the problem into simpler verification tasks on each of its components. Such compositional techniques appeared early in the model checking community [START_REF] Jones | Specification and design of (parallel) programs[END_REF]- [START_REF] Stark | A proof technique for rely/guarantee properties[END_REF]. We also refer the reader to [START_REF] Clarke | Handbook of model checking[END_REF] where existing rules and algorithms are summarized.

Given an automaton A and LTL formulas φ, ψ, let the triple φ A ψ denote A |= φ → ψ. Intuitively, φ represents the assumption we make on the environment of A, while ψ is the guarantee that A gives provided that the environment satisfies φ. We state the main theorem we use as follows.

Theorem V.1. Consider automata A 1 , A 2 with atomic propositions AP 1 , AP 2 and alphabets Σ 1 , Σ 2 , and LTL f \X formulas

φ 1 , φ 2 , φ 3 with Σ φ1 ⊆ Σ 1 , Σ φ2 = Σ 1 ∩ Σ 2 , and Σ φ3 ⊆ Σ 2 .
We have the following rule.

φ 1 A 1 φ 2 φ 2 A 2 φ 3 φ 1 A 1 A 2 φ 3 .
Thus, in order to prove φ 1 A 1 A 2 φ 3 it suffices to find a formula φ 2 and prove the two assertions φ 1 A 1 φ 2 and φ 2 A 2 φ 3 as per the previous theorem. A proof of this theorem for safety properties can be found in [START_REF] Clarke | Handbook of model checking[END_REF]. Our formulas are general LTL f \ X formulas in the finite trace semantics. However, in our model of the SDN protocol, all executions eventually stop so that we can encode all our formulas as safety conditions using the Promela keyword timeout (which detects the end of an execution). For completeness, we do provide a proof of this theorem for general LTL f \ X formulas which can be applied to general models. This proof as follows.

The language of A denoted as L(A) := { σ | σ ∈ (Σ) * ∧ ∅ = q 0 ∆ * (σ) ⊆ Q}, where q 0 ∆ * (σ) is the extended transition of ∆ transition in A starts from the initial state q 0 of automaton A.

For given alphabets Σ, Σ , and sequence σ ∈ Σ * , we denote by σ ↓ Σ the projection σ on Σ which consists in removing the letters in Σ \ Σ . The projection over Σ can be naturally extended for the language of an automaton A by

L(A) ↓ Σ = {σ ↓ Σ | σ ∈ L(A) }.
Condition V.1. When we consider the synchronized product of two automata A 1 , A 2 , we always assume that {Sync(σ

) | σ ∈ Σ 1 ∩ Σ 2 } = AP 1 ∩ AP 2 .
LTL f \X is the fragment of linear temporal logic without the next operator and defines stuttering-invariant properties [START_REF] Peled | Stutter-invariant temporal properties are expressible without the next-time operator[END_REF], while the subscript f refers to the fact that we interpret the formulas on finite words [START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF]. For any LTL f \ X formula φ over atomic propositions AP, let A φ be an automaton satisfying L(A φ ) = {w ∈ AP * | w |= φ}. Such an automaton can be constructed by [START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF]. We make however the following modification: whenever a state of A φ contains a predicate of the form Sync(σ), we label all incoming transitions by σ. Thus, if we denote by AP φ the set of atomic predicates referred to by φ, the alphabet of

A φ is Σ φ = {σ | Sync(σ) ∈ AP φ }.
For an automaton A := Q, q 0 , Σ ∪ {τ }, ∆, AP, L , a finite run of a given automaton

A is q 0 σ1 -→ q 1 σ2 -→ ...q n-1 σn --→ q n for some n ∈ N s.t ∀i ∈ [1, .., n], q i-1 σi -→ q i ∈ ∆.

And denote set of possible run of an automaton A as Run(A).

For a given finite run = q 0 σ1 -→ q 1 σ2 -→ ....q n-1 σn --→ q n ∈ Run(A), define seq of run as seq(run) := σ 1 σ 2 ...σ n .

Note that for any given finite run from a given automaton A i.e run ∈ Run(A), the corresponding seq belongs in the language of A, i.e seq(run) ∈ L(A). Definition V.1. For a given finite run = q 0 σ1 -→ q 1 σ2 -→ ...q n-1 σn --→ q n ∈ Run(A), define trace of such run as trace(run) = L(q 0 )L(q 1 )L(q 2 )...L(q n ) ∈ AP * .

Let us define a trace set for an automaton A as Tr(A) := {trace(run) | run ∈ Run(A)} ⊆ AP * . For w ∈ Tr(A), define run w = { run | trace(run) = w ∧ run ∈ Run(A) }.

Definition V.2. Consider the synchronized product of two automata A 1

A 2 , and run = (q 0,1 , q 0,2 ) σ1 -→ (q 1,1 , q 1,2 ), ..., σn --→ (q n,1 , q n,2 ) ∈ Run(A 1 A 2 ). The projection of such a run over Σ i for some i ∈ [START_REF] Boussard | Softwaredefined lans for interconnected smart environment[END_REF][START_REF] Holzmann | The SPIN model checker: Primer and reference manual[END_REF] is run ↓

Σ i := q 0,i σ 1 -→ q 1,i , ..., σ n --→ q n,i such that for all j ∈ [1, .., n] • If σ j ∈ Σ i and q j-1,i σj -→ q j,i ∈ ∆ i then σ j = σ j • If σ j ∈ Σ i then q j-1,i τ -→ q j,i ∈ ∆ i and σ j = τ
Observe that from the synchronized product definition, it is clear that for any given run ∈ Run(A 1 A 2 ), and

A = {Sync(σ)|σ ∈ Σ 1 ∩ Σ 2 }, L 1 (q j,1 ) ∩ A = L 2 (q j,2 ) ∩ A and in fact |L 1 (q j,1 ) ∩ A| = |L 2 (q j,2 ) ∩ A| ≤ 1.
The above definition can be extended to runs of products of arbitrary numbers of automata. For an example, if a run as in the form run = (q 0,1 , q 0,2 , q 0,3 ) σ1 -→ ..... σn --→ (q n,1 , q n,2 , q n,3 ), such that ∀j ∈ [0, 1, .., n], and ∀i ∈ [1, 2, 3], q j,i ∈ Q i and run ↓ (Σ 1 , Σ 2 ) refer to projection of the run to (q 0,1 , q 0,2 )

σ 1 -→ ..... σ n --→ (q n,1 , q n,2
) and each σ j defined as in above definition. Lemma V.1. For all automata A 1 , A 2 , and run

∈ Run(A 1 A 2 ), run ↓ Σ i ∈ Run(A i ) for i ∈ {1, 2}.
Proof. Its trivial from the definition V.2 Lemma V.2. For all automata A and w ∈ Tr(A), there exists run ∈ Run(A) such that trace(run) = w and seq(run) ∈ L(A).

Proof. By definition. Definition V.3. For given atomic predicates sets AP, AP and given sequence w ∈ AP * , w ↓ AP is the restriction of sequence w to AP . Lemma V.3. For a given LTL f \ X formula φ and respective model A φ , for an atomic predicates set AP, AP φ ⊆ AP, and w ∈ AP * , if w ↓ AP φ φ, then there exists a run ∈ Run(A φ ) so that trace(run) = w ↓ AP φ .

The above lemma also follows by definition. Lemma V.4. Consider an atomic predicates set AP and a LTL f \ X formula φ formed over atomic predicates set AP φ ⊆ AP. For all traces w ∈ AP * , w |= φ if, and only if w ↓ AP φ |= φ.

Proof. This is immediate from the semantics of LTL since atomic propositions in AP \ AP φ do not influence the satisfaction.

Definition V.4. Given any two runs run 1 and run 2 and atomic predicates set AP, if trace(run 1 ) ↓ AP = trace(run 2 ) ↓ AP then these two runs are equivalent with respect to AP which is denoted as run 1 ≡ AP run 2 .

For our theorem, we redefine the semantics of the triples φ 1 A φ 2 as follows.

Definition V.5. For an automaton A and LTL f \ X formulas φ 1 and φ 2 with predicate alphabets AP φ1 , AP φ2 ⊆ AP and A φ1 and A φ2 , Σ φ1 , Σ φ2 ⊆ Σ, we define φ 1 A φ 2 as ∀run ∈ Run(A φ1 A), trace(run ↓ Σ φ1 ) φ 1 → trace(run ↓ Σ) φ 2 Remark V.1. When considering compositional triples of the form φ 1 A 1 φ 2 and φ 2 A 2 φ 3 , with the intention of showing φ 1 A 1 A 2 φ 3 , we will require that Σ φ2 = Σ 1 ∩ Σ 2 . Let us recall some simple observations. For all run ∈ Run(A φ1 A 1 A 2 ) we have, by lemma V.1, run ↓ Σ 1 ∈ Run(A 1 ), and run

↓ Σ φ1 ∈ Run(A φ1 ). If φ 1 A 1 φ 2 then trace(run ↓ Σ φ1 ) φ 1 implies trace(run ↓ Σ 1 ) φ 2 and assume for a given run ∈ Run(A φ1 A 1 A 2 ), trace(run ↓ Σ φ1 )
φ 1 then by lemma V.3 there exists a run ∈ Run(A φ2 ) such that run ↓ Σ 1 ≡ AP φ 2 run and by lemma V.2 seq(run ↓ Σ 1 ) ↓ Σ φ2 = seq(run ) ∈ L(A φ2 ). Lemma V.5. Consider automata A 1 , A 2 and formulas φ 1 , φ 2 satisfying Σ φ2 = Σ 1 ∩Σ 2 . Assume that φ 1 A 1 φ 2 holds. For all run ∈ Run(A φ1 A 1 A 2 ), there exists run ∈ Run(A φ2 ) and run" ∈ Run(A φ2 A 2 ) which satisfy run" ↓ Σ 2 = run ↓ Σ 2 and run" ↓ Σ φ2 = run .

Proof. Observe that run can be obtained as in the previous remark.

Without loss of generality hide all the τ transition in all the runs i.e if a run = run 3 σ -→ (q) τ -→ (q ) σ -→ run 4 then we work out only for run 3 σ -→ (q ) σ -→ run 4 We construct such a run" by the length of the runs, we will recall one property which we will use in our construction, for a given run ∈ Run(A 1 A 2 ), by remark V.1 |run | ≤ |run ↓ Σ 2 | because all the common alphabets in A 1 and A 2 fired together in A 1 A 2 then those common alphabets (Σ 1 ∩ Σ 2 ) fired together in the run ↓ Σ 1 is captured in A φ2 ( i.e run ≡ AP φ 2 run ↓ Σ 1 ). So that seq(run

) = seq(run ↓ Σ 2 ) ↓ Σ φ2 . • Simple case |run 1 = run ↓ Σ 2 | = 1 and |run | = 1, run 1 = q 0,2 σ1 -→ q 1,2 ∈ Run(A 2
) and run = q 0,φ2

σ 1 -→ q 1,φ2 ∈ Run(A φ2 ) -case σ 1 = σ 1 if this is the case then σ 1 ∈ Σ 1 ∩ Σ 2
then the respective run" will be (q 0,φ2 , q 0,2 )

σ1=σ 1 ----→ (q 1,φ2 , q 1,2 ) ∈ Run(A φ2 A 2 ) -case σ 1 = σ 1 ,
this can't be a case, since it is not satisfying seq(run ) = seq(run ↓ Σ 2 ) ↓ Σ φ2 .

• General case: here we will construct a run" for given run and run ↓ Σ 2 w.l.o.g seq(run 1 = run ↓ Σ 2 ) = σ 1 σ 2 ...σ m and seq(run ) = σ i1 σ i2 ...σ in where n ≤ m and we know that seq(run ↓ Σ 2 ) ↓ Σ φ2 = seq(run ). j 1 ∈ [1, .., m] is minimum index number, such that σ j1 = σ i1 , and corresponding run up to executing the σ i1 alphabet looks like run 1j 1 = q 0,2 σ1 -→ ...

σj 1 -1 ----→ q j1-1,2 σj 1
--→ q j1,2 and run 1 = q 0,φ2 σi 1

--→ q 1,φ2 then construct run" j1 = (q 0,φ2 , q 0,2 ) σ1 -→ (q 0,φ2 , q 1,2 )...

σj 1 -1 ----→ (q 0,φ2 , q j1-1,2 ) σj 1 =σi 1 -----→ (q 1,
φ2 , q j1,2 ). Now find a minimum j 2 ∈ [j 1 + 1, m] such that σ j2 = σ i2 and construct run" j2 which we do repeatedly until for j n we will get run" jn and then extent run" jn by just firing the alphabets from σ jn+1 , ..σ m we will get run". If we check this constructed run it does satisfies run" ↓ Σ 2 = run ↓ Σ 2 = run 1 and run" ↓ Σ φ2 = run .

The theorem V.1 can be stated with above conditions as follows, Theorem V.2. For all automata A 1 and A 2 , and

LTL f \ X formulas φ 1 , φ 2 , φ 3 using the atomic propositions in AP φ1 ⊆ AP 1 , {Sync(σ) | σ ∈ Σ 1 ∩ Σ 2 } ⊆ AP φ2 ⊆ AP 1 , and AP φ3 ⊆ AP 2 , Σ φ1 ⊆ Σ 1 , Σ φ2 = Σ 1 ∩Σ 2 ,
and Σ φ3 ⊆ Σ 2 , the following inference rule holds.

φ 1 A 1 φ 2 φ 2 A 2 φ 3 φ 1 A 1 A 2 φ 3

Proof. Consider any w ∈ Tr(A φ1

A 1 A 2 ), and run ∈ run w , and assume that trace(run ↓ Σ φ1 ) φ 1 . We need to prove that trace(run ↓ Σ 2 ) φ 3 .

By lemma V.1 ∀run ∈ run w , ( run

↓ (Σ φ1 , Σ 1 ) ) ∈ Run(A φ1
A 1 ) and by premise (

φ 1 A 1 φ 2 ) trace(run ↓ Σ φ1 ) φ 1 implies trace(run ↓ Σ 1 ) φ 2 .
By lemma V.2 and lemma V.3 there exists a run ∈ Run(A φ2 ) s.t trace(run ↓ Σ 1 ) ↓ AP φ2 = trace(run ) and by lemma V.1 run ↓ Σ 2 ⊆ Run(A 2 ).

It is easy to observe that there is a run" ∈ Run(A φ2 A 2 ) by lemma V.5 such that run" ↓ Σ 2 = run ↓ Σ 2 and run" ↓ Σ φ2 = run .

By premise ( φ 2 A 2 φ 3 ) trace(run" ↓ Σ φ2 ) φ 2 implies trace(run" ↓ Σ 2 ) φ 3 . I.e trace(run ↓ Σ 2 ) ↓ AP φ3 φ 3 then by lemma V.4 trace(run ↓ Σ 2 ) φ 3 .

We argue that compositional reasoning is particularly well adapted for verifying SDN protocols. In fact, SDN platforms are distributed systems made of well-separated components, which are the management plane, the controller plane and the data plane. In order to meet our global specifications of isolation and connectivity, each plane has to satisfy a certain property. One of the sources of complexity in verification comes from the fact that several planes are considered in the model. Compositional reasoning allows us to verify properties of each plane separately, and combine these rules to infer the specification for the global system. We explain the application of Theorem V.1 in the next section. To use Theorem V.1 we need to formally state the specifications for each components in LTL. Finding these properties requires domain knowledge. In fact, one needs to understand with which intentions the system was designed in order to write these formulas.

The management plane and control plane should work together to satisfy the following requirement:

I 1 = 1≤i =j≤k,x,x ∈Dev VS(x)∩VS(x ) =∅ v∈Swi,v ∈Swj p,p ∈Pts pos(x) = (v, p) ∧ pos(x ) = (v , p ) ∧(rpos i (x, root i ) = ⊥) → ♦Sync(c i , root i , (x, root j )) .
The above formula says that whenever devices x and x are respectively connected at switch-port pairs (v, p) and (v , p ) in respectively domains i and j, if the root switch of domain i has received a MAC learning packet originated from device x, then eventually the root switch will receive a MAC update rule from the controller to forward MAC packets of device x towards root j . This I 1 captures the fact that the control plane sends appropriate MAC rule updates to the root switch of its domain, thus to the data plane.

I 2 = 1≤i≤k,x,x ∈Dev VS(x)∩VS(x ) =∅ v,v ∈Sw,p,p ∈Pts u∈Swi,q,q ∈Pts∪Sw pos(x) = (v, p) ∧ pos(x ) = (v , p ) ∧(rpos i (u, x) = q) ∧(rpos i (u, x ) = q ) → ♦Sync(c i , u, (x, x , q )) .
The above formula states that, given devices x, x connected at (v, p) and (v , p ) respectively, if another switch u has received and forwarded MAC learning packets to the controller witnessed by (rpos i (u, x) = q) ∧ (rpos i (u, x ) = q ), then a ping update rule will eventually be sent to switch u to forward packets ping(x, x ) to q . Thus, I 2 expresses that the control plane sends appropriate ping rule updates to all the switches and thus to the data plane of its domain.

The above requirements should be satisfied jointly by the management and control planes, that is, we would like to establish that true A man A Cont I 1 ∧ I 2 should be true. However, this check can still be costly for large topologies. Therefore, we apply again Theorem V.1 to check this compositionally. We need to introduce another intermediate formula I 3 between the management plane and controller plane. This captures that whenever a management node man i receives information about a device's position from its controller c i , eventually, all management nodes man j forward this information to their respective controller c j . Thus, the information about a device of domain i is eventually shared with the controller of other domains j.

I 3 = 1≤i≤k,x∈Dev j∈[1,..,k] (dinfo i (x) = ⊥) → ♦Sync(man j , c j , (x, dinfo i (x), VS(x)))
So we can check the satisfaction of true A man A Cont I 1 ∧I 2 by verifying true A man I 3 , and

I 3 A Cont I 1 ∧ I 2 .
Complete description of experimental details are provided in [START_REF] Majith | Open access Repository for "Compositional model checking of an SDN platform[END_REF].

VI. NO-MOBILITY SCENARIO VALIDATION

Let us call the Isolation, Connect, and Nomobility as mentioned in section 4.4 as φ I , φ C and ψ respectively. Recall the intermediate formula I 1 , I 2 , and I 3 We are going to verify, the specified SDN platform in section 3 and 4 satisfies the Isolation and Connect properties under the assumption of Nomobility property. We are going to compare the usage of Compositional Reasoning (CR) in verifying the SDN platform over the monolithic approach. Monolithic approach consists in verifying the entire system i.e checking whether true A man A Cont A Sw

A Dev ψ → φ I ∧ φ C is true or false. Compositional rule method 1 (CR method 1) consists in splitting the control plane from the data plane and thus in verifying separately the two automata: true A man A Cont I 1 ∧ I 2 , and

I 1 ∧ I 2 A Sw A Dev ψ → φ I ∧ φ C .
Compositional rule method 2 (CR method 2) consists in further splitting the management plane from the control plane and checking three triples: true A man I 3 , I 3 A Cont I 1 ∧ I 2 , and

I 1 ∧ I 2 A Sw A Dev ψ → φ I ∧ φ C .
The results for various sizes of the SDN platform topology and the three methods are shown in Table I. For a given size of SDN platform, we checked all possible SDN constrained topologies as mentioned in Section 3 and 4 and for all possible random choices carried by the devices to connect to their Access-port positions. This is the main reason for large memory usage and CPU time spent as indicated in Table I. Within the Nomobility condition, once the device has selected its position and sent its first MAC learning packet, it waits for a timeout. After the first timeout, it sends a second MAC learning packet and waits for the second timeout. After the second timeout, it sends ping packets to all other devices. In this scenario we check that devices sharing a common VS can receive ping packets from each other (i.e. Connect property), and that devices not belonging to this particular VS cannot receive the ping packets from the group and vice versa (i.e. Isolation property). In order to test these Isolation and Connect properties we create the following set of VSes, VS = { {d 1 , d 2 }, {d 3 }}, where {d 1 , d 2 } is one VS containing devices d 1 and d 2 and {d 3 } the other VS containing a single device d 3 . We verify that d 3 cannot receive ping packets from devices in {d 1 , d 2 } and vice-versa in order to assert that the SDN platform satisfies the Isolation property. We also verify that eventually d 1 and d 2 can receive ping packets of one another to assert that the SDN platform satisfies the Connect property. For the particular case of no-mobility, the SDN platform satisfies both Isolation and Connect properties. To shortly capture the SDN platform architecture we adopt for the rest of the document the following notations. We denote by n, (X, Y, Z) the set of topologies with n domains (1 ≤ n ≤ 3 in our case), where (X,Y,Z) refers to the number of OVSes in each domain. For the single domain with 3, 4, and 5 switches there are respectively two, four and five possible data plane topologies since we restrict to trees. For the case of two domains (n = 2), the possibilities are (2, 1, -), (3, 1, -), (2, 2, -), and (3, 2, -); in this case, there are, respectively, one, two, one, and two possible data plane topologies. With three domains (n = 3), the possibilities are (1, 1, 2) and (1, 1, 3), in which case there are one and two possible data plane topologies respectively. In our experiments, we enumerate all topologies that match a given template (X, Y, Z) to check exhaustively all possible scenarios. Therefore, the cases with larger numbers of topologies take more time to check.

We ran our experiments on an Intel i7 processor with 13GB of available RAM. Table I compares the monolithic and two compositional approaches, called Method 1 and Method 2, with respect to CPU time and memory usage on SDN topologies of varying sizes. While the monolithic approach fails to scale above trivial topologies, compositional methods helped us to complete the verification process up to 3 domains in our experiments. However, we still fail to complete the verification process for one domain with 6 switches with both CR methods. The bottleneck during this experiment was checking

I 1 ∧ I 2 A Sw A Dev φ I ∧ φ C .
CR method 1 and method 2 provide the same performance up to 2 domains. When the number of domain is 3, CR method 2 gives advantage over the RAM usage and CPU time. Within CR method 1, for 3 domains, much of its CPU and RAM resources are consumed in checking true A man A Cont I 1 ∧I 2 . Thanks to the additional decomposition between the management plane and the control plane, CR method 2 provides us with better performance. Here the majority of CPU and RAM resources are consumed in checking

I 1 ∧ I 2 A Sw A Dev ψ → φ I ∧ φ C .
The sizes of state space produced in the monolithic method reaches the order of 10 6 for two switches in a single domain, while the compositional approaches produce around 10 4 states for the same architecture. However, the compositional approaches still can not manage the model with 6 switches in a single domain and go out of memory.

VII. ISSUE WITH DEVICE MOBILITY

We now present an interesting part of our formal verification experiments. In the last section, we found that the studied SDN platform does satisfy the required specifications, namely the isolation property and the connectivity property. What if we allow devices to move freely but still use the data plane service to exchange packets? Given this freedom, devices can select their new positions wherever and whenever they want.

This freedom makes the SDN system vulnerable w.r.t. the data isolation property. We identified an error, that is, an execution which violates the isolation property. We can produce the error simply with our monolithic model checking for one domain and two switches, that is, true A man A Cont A Sw A Dev φ I is violated, where φ I the Isolation property.

We find this error by considering VS = {{d 1 , d 2 }, {d 3 }} and the following mobility scenario: once first MAC learning packets are exchanged and ping rules are updated, devices d 2 and d 3 swap their respective Access-port. After the mobility events, Spin raises an Isolation violation reporting that device d 3 receives a ping packet send by d 1 to d 2 .

A. Network Slice Isolation Violation SPIN reveals a counterexample trace but does not give the probability of its occurrence. In this section, we discuss an illustrative scenario to derive an estimation of the probability.

Let's consider δ as the minimum time needed by the controller to receive a given data plane packet and to respond with a new set of rules to the originating switch (due to the controller queues cdque and mque). Further, let's call as the time needed by the switch to inform the controller about the possible reconfiguration of the data plane network topology (due to switch queues cque and dque). Finally, let's consider λ as the average number of data packets exchanged per time unit by the switch and devices in the data plane. With the SDN platform made of a single domain k = 1, we have the controller c in the control plane, and three devices {d 1 , d 2 , d 3 } and one switch sw which has three ports {1, 2, 3} in the data plane. Initially devices d 1 , d 2 , d 3 are connected respectively to the ports 1, 2, 3 of switch sw. The management plane applies the following VS of devices {{d 1 , d 2 }, {d 3 }} where {d 1 , d 2 } forms one VS and {d 3 } is lonely device in another VS. The controller has to ensure that the set of rules it forwards to the data plane (i.e to the switch sw) prevent devices d 3 from receiving packets exchanged between d 1 and d 2 . After receiving MAC learning packets from the switch sw, the controller c forwards ping rules to the latter, enforcing that packets from the port 1 should be delivered to port 2 and those from port 2 should be delivered to port 1 and any data packet from the port 3 should be dropped. When the data plane topology undergoes a transition, such as d 2 and d 3 are exchanging their respective position, it takes the controller c a time interval of (δ + ) before being aware of the new situation and actually enforcing new rules. During this lap of time, there are possible scenarios of device d 3 being able to receive packets exchanged between devices d 1 and d 2 . For instance, device d 3 occupies now the port 2 of the switch sw and devices d 1 , d 2 occupy respectively ports 1, 3. Due to the communication delay between the switch and the controller, the chance (probability) of device d 3 receiving ping packets delivered by d 1 to d 2 is in the order of O(λ × (δ + )). We are able to reproduce such an Isolation violation with the network simulator called as GNS3. Thus, the probability of the Isolation violation occurrence is roughly proportional to the packet data rate (i.e. λ) and the overall latency (i.e. (δ + )) between the domain controller and the switch, called as the control link latency. The first proportionality means that higher bandwidth data paths require faster control plane or smaller control link latency. However, the latter has its own limitation and is very dependent on the SDN architecture. On the studied SDN platform, the controller is centralized so that there is a one-to-one mapping between the controller and the manager in a given domain. This allows for simplifying the synchronization of user's intents and device identity between the two components. Unfortunately, this centralization could induce important control link latency. First, it's about communication delay. As uplink communications from different switches within the domain are aggregated when they arrive at the controller, the bandwidth required becomes higher and higher as the number of controlled switches and the number of connected devices increase. Congestion at the controller incoming link could occur if the link was not correctly dimensioned -e.g. a massive arrival of new devices into the data network leads to a massive arrival of MAC-Learning-related PacketIn messages at the controller. Second, it's about processing delay. If the controller was limited in terms of processing power, then its incoming queues could fill up leading to excessive delay and even to loss of control messages (i.e. infinite delay). Furthermore, this also illustrate the fact that the order in which the reading of of messages is important for safety properties for SDN platform.

B. Local Controller Solution

In order to work around previous control link latency issues, one possible solution consists in implementing a hierarchical controller architecture with a new controller embedded together with each switch that we call as local controller in addition to the existing centralized controller that we call as the central controller. Figure 2 illustrates such a controller hierarchical architecture. The local controller role simply consists in blocking any outgoing traffic towards a port (e.g. port 2) when the existing device (e.g. d 2 ) is disconnecting from this port (e.g. a port down status message sent to controllers). It maintains such a blocking rule until a new device (e.g. d 3 ) is connected to the port and MAC learning messages from this device are processed by the central controller and new forwarding rules related to the new device are received by the switch. In order to ensure new rules are actually received by the switch, the local controller is implemented as an OpenFlow proxy between the switch and the central controller.

As the local controller is colocated with the switch, we can assume a zero control link latency between the two.

Moreover, the number of devices the local controller should deal with is smaller than the one the central controller is dealing with by the order of magnitude the number of switches. The variability of control message rate is to be smaller from the local controller perspective, which leads to an easier engineering in terms of processing resources. Such a local controller can be modeled by an automata as A loc.Cont .

C. Local Controller Solution Validation

In this section, we verify that the proposed local controller solution satisfies the Isolation property, i.e true A man A Cont A Sw A loc.Cont A Dev φ I , where φ I is the Isolation

VIII. CONCLUSION

In this document we have demonstrated that it is possible to fully model an SDN architecture including the entire 3 planes, namely the data plane, the control plane and the management plane. It is also possible to include device connectivity and mobility. Although state space can rapidly explode, it is still possible to validate a complex SDN architecture based on a minimum representative model of it.

Within this framework, we have shown that compositional model checking is well-adapted for verifying SDN architectures. It allows one to verify the whole system while verifying each individual component of it. The decomposition of an SDN architecture can be performed, as an illustrative experiment, vertically between planes. This provides more scalability especially when complexity becomes high.

We have demonstrated that it is possible to verify that users' intents are correctly enforced on the data plane in the form of network slices using model checking. There is a need however to develop an automatic framework to translate high-level intents to concrete network policies in a generic way.

Finally, we have discussed on the trade off between a centralized architecture and a more distributed one and have set up an architecture proposition with regards to network slice isolation issue related to control message transmission latency. Indeed, most of SDN architecture advocates for a centralized controller as this optimizes the interaction with applications and simplifies the related algorithms. This may lead however to some important issues such as the network slice isolation violation revealed in this document. The probability of such an issue is likely to be exacerbated when operating at high data rate. A hierarchical architecture such as the one we propose can solve the issue.

In order to complete this work, we plan to introduce formal synthesis methods aiming at automatically synthesizing the local SDN controller algorithm with regards to some set of safety constraints as tackles in [START_REF] Kalyon | Symbolic supervisory control of distributed systems with communications[END_REF]. Other directions are to abstract the system so that traditional supervisory control synthesis of reactive systems can be applied [START_REF] Ayeb | Towards an Autonomic and Distributed Device Management for the Internet of Things[END_REF].

Fig. 1 .

 1 Fig. 1. SDN Platform Description

Fig. 2 .

 2 Fig. 2. Local Controller Architecture

TABLE I MONOLITHIC

 I VS COMPOSITIONAL APPROACHES (WITH NO-MOBILITY)

  Table II provides a synthetic view of these experimental data. n domains, (X, Y, Z) Switches Compositional reasoning rule I1 ∧ I2 A Sw A loc.Cont A Dev φ I true A man A Cont I1 and true A man A Cont I2 Total Computation time Maximum RAM memory used 1, (1, -, -)

		4.8sec	188 MB
	1, (2, -, -)	8.4sec	224 MB
	1, (3, -, -)	1min 2sec	448 MB
	1, (4, -, -)	6min 22sec	982 MB
	1, (5, -, -)	1hr 5min 8sec	7245 MB
	2, (1, 1, -)	11sec	214 MB
	2, (2, 1, -)	33sec	395 MB
	2, (3, 1, -)	3min 10.3sec	865 MB
	2, (2, 2, -)	96.5sec	848 MB
	2, (3, 2, -)	25min 13sec	6327 MB
	3, (1, 1, 1)	19min 9.8sec	4291 MB
	3, (1, 1, 2)	36min 44.39sec	6981 MB
	3, (1, 1, 3)	1hr 24min 3.45sec	12254 MB
		TABLE II
	LOCAL CONTROLLER PROPOSAL VALIDATION USING CR METHOD
		(MOBILITY SCENARIO)