[Docs] [txt|pdf] [Tracker] [Email] [Diff1] [Diff2] [Nits]

Versions: 00 01 02 03

Network Working Group                                           M-K. Shin
Internet-Draft                                                   K-H. Nam
Intended status: Informational                                       ETRI
Expires: December 2012                                            M. Kang
                                                                  J. Choi
                                                                 Korea U.
                                                            June 29, 2012

        Formal Specification for Software-Defined Networks (SDN)
                 draft-shin-sdn-formal-specification-01

Abstract

   This document discusses formally verifiable networking framework for
   software-defined networks (SDN). In SDN, incomplete or malicious
   programmable entities could cause break-down of underlying networks
   shared by heterogeneous devices and stake-holders. Formally
   verifiable networking can provide a logic-based framework to unify
   the design, specification, verification, and implementation of SDN.
   This framework describes formal specification and verification
   process for SDN. In addition, we present two examples of formal
   specification for a part of SDN using a process algebra called
   Algebra of Communicating Shard Resources (ACSR) and Z specification
   language.

Requirements Language

   The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT",
   "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this
   document are to be interpreted as described in RFC 2119 [RFC2119].

Status of this Memo

   This Internet-Draft is submitted to IETF in full conformance with the
   provisions of BCP 78 and BCP 79.

   Internet-Drafts are working documents of the Internet Engineering
   Task Force (IETF), its areas, and its working groups.  Note that
   other groups may also distribute working documents as Internet-
   Drafts.

   Internet-Drafts are draft documents valid for a maximum of six months
   and may be updated, replaced, or obsoleted by other documents at any
   time.  It is inappropriate to use Internet-Drafts as reference
   material or to cite them other than as "work in progress."

   The list of current Internet-Drafts can be accessed at
   http://www.ietf.org/ietf/1id-abstracts.txt.



Shin et al.,             Expires December 2012                  [Page 1]

Internet-Draft        Formal Specification for SDN         June 29, 2012


   The list of Internet-Draft Shadow Directories can be accessed at
   http://www.ietf.org/shadow.html.

   This Internet-Draft will expire on September 1, 2012.

Copyright Notice

   Copyright (c) 2012 IETF Trust and the persons identified as the
   document authors.  All rights reserved.

   This document is subject to BCP 78 and the IETF Trust's Legal
   Provisions Relating to IETF Documents
   (http://trustee.ietf.org/license-info) in effect on the date of
   publication of this document.  Please review these documents
   carefully, as they describe your rights and restrictions with respect
   to this document.  Code Components extracted from this document must
   include Simplified BSD License text as described in Section 4.e of
   the Trust Legal Provisions and are provided without warranty as
   described in the Simplified BSD License.


Table of Contents

   1. Introduction ....................................................3
   2. Formally Verifiable Networking Framework for SDN ................3
   3. Formal Specification for SDN ....................................4
   4. Examples ........................................................6
     4.1 Formal Specification of SDN using ACSR  ......................6
     4.2 Formal Specification of SDN using Z ..........................8
     4.3 Subtle Ambiguities Discovery and Correctness Verification ....9
   5. Security Considerations ........................................10
   6. Acknowledgements ...............................................10
   7. References .....................................................10
     7.1 Normative References ........................................10
     7.2 Informative References ......................................10
   Authors' Addresses ................................................12















Shin et al.,             Expires December 2012                  [Page 2]

Internet-Draft        Formal Specification for SDN         June 29, 2012


1. Introduction

   Software-defined networking (SDN) is emerging and intensively
   discussed as one of the most promising technologies to introduce
   network virtualization within data centers, enterprise networks,
   mobile networks, etc. [I-D.nadeau-sdn-problem-statement],[b-
   OpenFlow]. SDN is defined as a new networking approach which enables
   network operators and/or application/service providers to add their
   own processing, control, program, etc. through open network
   interfaces and network abstraction into their networks that they can
   control and manage the slicing and virtualization of the networks.
   With SDN, network operators and application/service providers can
   introduce a new capability easily by writing a simple software
   program.

   To design and implement networks that conform to the design goals of
   SDN network topology, the structure and behavior of the networks need
   to be formally specified to prevent from misinterpreting of the
   intended meanings and to avoid inconsistency in the networks.
   Furthermore, SDN networks can be used for safety-critical systems
   such as avionic and automotive systems, nuclear power plants, and
   medical devices, and those systems should be verified to guarantee
   their reliability and security properties, otherwise catastrophic
   disaster could be occurred. Other areas that the SDN networks can be
   applied, such as private clouds and data centers, also benefit from
   formal specification and analysis since any inconsistencies in the
   systems and unexpected errors that could not be caught during design
   process can result in network breakdown or system failure, which can
   lead to tremendous commercial loss [b-Nam12].

   This document discusses formally verifiable networking framework for
   SDN. Formally verifiable networking can provide a logic-based
   framework to unify the design, specification, verification, and
   implementation of SDN.  This framework presents formal specification
   and verification process for SDN.


2. Formally Verifiable Networking Framework for SDN

   SDN network operators and application/service providers can introduce
   a new capability by writing a simple software program. In SDN,
   incomplete or malicious programmable entities could cause break-down
   of underlying networks shared by heterogeneous devices and stake-
   holders. Formally verifiable networking in SDN can reduce any
   inconsistency or misunderstanding of the meaning of components and
   mechanisms because formal specification removes ambiguity in the
   informal specifications. Furthermore, formal specification can be
   applied to verification methods such as theorem proving, process



Shin et al.,             Expires December 2012                  [Page 3]

Internet-Draft        Formal Specification for SDN         June 29, 2012


   algebraic analysis, model checking, and static analysis.

   Figure 1 illustrates an overview of the formally verifiable
   networking framework for SDN, which consists of the three components,
   formal specification, verification methods, and implementation. SDN
   network operators and application/service providers design an
   abstract network model (e.g., virtual network topology) of desired
   properties informally. After then, the SDN network operators and
   application/service providers write down formal specification for the
   properties, which finally verifies that implementation (e.g., SDN
   control software) satisfies these properties.

   In general, traditional methods of realizing network protocols and
   devices are based on community agreements of informal specification
   of such mechanisms. As depicted in Figure 1, those processes can be
   improved by applying formal methods in the development process of
   SDN. Targets of specification can range from conceptual model of
   components or mechanisms for SDN, logical switch/router models,
   network protocols, user-defined topologies of virtual networks, and
   so on. Informal specification of those targets can be encoded in
   formal specification languages that can best reflect the features of
   targets among the existing methods for formal specification. The
   formal specification can be textual form or graphical representation
   only if their semantics are defined formally and unambiguously. Once
   the specifications are described formally, system and protocol
   designer can check the existence of inconsistencies and possible
   errors in the specification with the help of formal methods experts
   or supporting tools. Any type of formal verification methods can be
   applied to this validation and verification process while each has
   pros and cons for this purpose. One may use theorem proving such as
   HOL, Isabelle, Coq, PVS with the help of assistant tools and experts,
   others can take advantage of full automation of this process by
   specifying important properties in temporal logics and feed them into
   model checking tools such as SPIN and SMV [b-Nam12].


3. Formal Specification for SDN

   We discuss formal specifications about virtual network topology of
   SDN. The two researches that are most closely related to our work are
   NetCore [b-NetCore12] and NDlog [b-NDlog11]. But each has different
   perspectives. NetCore, the Network Core Programming Language, is a
   high-level and declarative language for expressing packet-forwarding
   policies and has a formal semantics. Network Datalog (NDlog) is
   distributed recursive query language used for querying network
   graphs.





Shin et al.,             Expires December 2012                  [Page 4]

Internet-Draft        Formal Specification for SDN         June 29, 2012


                               +----------- 0.Design abstract
                               |              network model using
                               v              informal specifications
                       +---------------+     (e.g., virtual network
                       |   1.Formal    |      topology etc.)
                       | specification |
                       +---------------+
                               |
                               v
                       +---------------+  +--------+
                       |               +--| Model  | ...
                       | 2.Verification|  |checking|
                       |    methods    |  +--------+
                       |               |  +--------+
                       |               +--|Theorem | ...
                       +---------------+  |proving |
                               |          +--------+
                               v
                     +-------------------+
                     | 3.Implementation  |
                     | (control software)|
                     +-------------------+
                               ^
                               |
                               v
                    .---------------------.
                   /                       \
                  /      SDN Data plane     \
                  ' (heterogeneous devices, '
                  \       switches, etc.    /
                   `-----------------------'

         Figure 1 Formally verifiable networking framework for SDN

   We consider developing a new formal specification language to
   accommodate various requirements of SDN networks and properties, if
   necessary. At this moment, we use process algebra ACSR (Algebra of
   Communicating Shard Resources) [b-ACSR95] and Z specification
   language formally, as examples. To provide a correct and efficient
   solution for forwarding packets on the SDN, ACSR can express
   processes running concurrently and communicating switches and a
   controller. Forwarding packets can be modeled as prioritized
   synchronization of events in ACSR. In addition, Z specification for
   SDN is focused on each switch and controller for emphasis on their
   functionality. Based on this, we are researching to verify the OF/SDN
   through the analysis of the requirement for OpenFlow.





Shin et al.,             Expires December 2012                  [Page 5]

Internet-Draft        Formal Specification for SDN         June 29, 2012


4. Examples

4.1 Formal Specification of SDN using ACSR

   This clause describes an example of ACSR specification of SDN. In our
   process algebraic approaches, network entities are represented by
   processes in ACSR.

   ACSR is a formal specification and verification methods for behavior
   modeling using concepts of processes, resources, events, and
   priorities. ACSR, like other process algebras, consists of (1) a set
   of operators and syntactic rules for constructing process; (2) a
   semantic mapping which assigns meaning or interpretation to
   processes; (3) a notion of equivalence or partial order between
   process; and (4) a set of algebraic laws that allows syntactic
   manipulation of processes. ACSR uses two distinct action types to
   model computation: time and resource-consuming actions, and
   instantaneous events.

   ACSR distinguish two types of actions: those which consume time, and
   those which are instantaneous. Timed actions may require access to
   system resources, e.g., network bandwidth etc. In contrast,
   instantaneous actions provide a synchronization mechanism between
   concurrent processes. In this document, we use only instantaneous
   action to model SDN.

   Packet forwarding is specified as event sending and receiving. Packet
   matching with rules are represented by synchronization between input
   and output events. We provide a demonstration of ACSR specification
   of an example virtual networks.

   Let the example virtual networks have a topology shown in Figure 2.
   The topology consists of a single switch and three hosts (H1, H2, and
   H3).

                           --------
                     +--->| Switch |---+
                     |     --------    |
                     |        |        |
                     |        v        v
                   ----     ----     ----
                  | H1 |   | H2 |   | H3 |
                   ----     ----     ----

              Figure 2 Example virtual topology


   An abstract view point is used to model packets by abstracting out



Shin et al.,             Expires December 2012                  [Page 6]

Internet-Draft        Formal Specification for SDN         June 29, 2012


   all detailed data in the packets. We assume that there are several
   types of packets forwarded between nodes in the networks as follows:

        +---------+----------+---------------------------+
        |  Sender | Receiver |      Types of packets     |
        +---------+----------+------------------------- -+
        |    H1   |  Switch  | packet1, packet2, packet3 |
        |  Switch |    H2    |          packet4          |
        |  Switch |    H3    |      packet5, packet6     |
        +---------+----------+---------------------------+

   We also assume that there are three types of rules in switch which
   are rule1, rule2 and rule3. Packets are matched to rules in the way
   as follows. The larger number indicates the higher priority. Note
   that packet1 can be matched to both rule2 and rule3 and packet2 can
   be matched to both rule2 and rule3.

       +--------------------------------------------------------+
       | Rule | Priority | Packets matched | Action on matching |
       +--------------------------------------------------------+
       |rule1 |     4    |     packet1     |        action1     |
       |rule2 |     3    |     packet1     |        action2     |
       |rule2 |     3    |     packet2     |        action2     |
       |rule3 |     6    |     packet2     |        action3     |
       |rule3 |     6    |     packet3     |        action3     |
       +--------------------------------------------------------+

       +-------------------------------------------------+
       | Action  |             Description               |
       +-------------------------------------------------+
       | action1 | output packet4 to H2 through outPort1 |
       | action2 | output packet5 to H3 through outPort2 |
       | action3 | output packet6 to H3 through outPort2 |
       +-------------------------------------------------+

   The process 'Network' represents the example system being specified.
   'Network' consists of H1, H2, H3, and Switch, which are composed
   using the parallel operator because they are running in parallel and
   interacting each other. The specification of the process 'System' is
   as follows:


    Network = (H1||H2||H3||Switch)
              \{inPort,outPort1,outPort2,activatingRule1,
              activatingRule2,activatingRule3};

   In an example topology in Figure 2, we assume that there are three
   hosts which are specified as ACSR processes 'H1', 'H2' and 'H3'. H1



Shin et al.,             Expires December 2012                  [Page 7]

Internet-Draft        Formal Specification for SDN         June 29, 2012


   transmits to Switch packets such as packet1, packet2, and packet3. H2
   receives packets such as packet1 and packet3. H3 receives packets
   such as packet1 and packet2.


    H1 = (inPort!1,1).(inPort!2,1).(inPort!3,1).Host1;
    H2 = (outPort1?packet,1).Host2;
    H3 = (outPort2?packet,1).Host3;

   The switch in the example network consists of 'InputModule',
   'FlowTable', and 'OutputModule'. The specification of 'Switch',
   'InputModule', FlowTable', and 'OutputModule' are as follows:

    Switch = (InputModule||FlowTable(1,1,0)||OutputModule)
             \{rule1,rule2,rule3,rule0,action1,action2,action3};

    InputModule = (inPort?packet, 1).(
      cket = 1) -> ((rule1!,1).InputModule + (rule2!,1).InputModule)
      + (packet = 2) -> ((rule2!,1).InputModule + (rule3!,1).InputModule
      + (packet = 3) -> (rule3!,1).InputModule
      + (rule0!packet,0).InputModule
      );

    FlowTable(r1,r2,r3) =
    (r1 = 1) -> (rule1?,4).(action1!,99).FlowTable(r1,r2,r3)
        + (r2 = 1) -> (rule2?,3).(action2!,99).FlowTable(r1,r2,r3)
        + (r3 = 1) -> (rule3?,6).(action3!,99).FlowTable(r1,r2,r3)
        + (activatingRule1?,99).FlowTable(1,r2,r3)
        + (activatingRule2?,99).FlowTable(r1,1,r3)
        + (activatingRule3?,99).FlowTable(r1,r2,1);
        + (rule0?packet,0).('requestRuleForPacket?packet,99).
                                        FlowTable(r1,r2,r3);

    OutputModule = (action1?,999).(outPort1!4, 1).OutputModule
              + (action2?,999).(outPort2!5, 1).OutputModule
              + (action3?,999).(outPort2!6, 1).OutputModule;

   We describe a portion of formal specification of the informal SDN
   specification using ACSR. ACSR can express processes running
   concurrently and communicating the switches and controller.
   Forwarding packets can be modeled as prioritized synchronization of
   events in ACSR. But the disadvantages of ACSR is that it is hard to
   categorize classification of data packets.

4.2. Formal Specification of SDN using Z

   This clause describes an example of the Z specification for SDN that
   is comprised of lots of switches and a controller managing them. In



Shin et al.,             Expires December 2012                  [Page 8]

Internet-Draft        Formal Specification for SDN         June 29, 2012


   this specification, we focus on each one switch and controller for
   emphasis on their functionality of them. For an example, switch keeps
   a flowtable for handling input packets. This table has a fulfillment
   action for some packets, and can be modified by the controller

    Table_Type == HEADER_FIELD x N x F ACTION_TYPE

   The table is made up of a packet header, applied counter and actions.
   The counter plays a role of priority, so when one packet matches more
   than two elements, actions having a higher counter value will be
   applied.

    PORT ::= port1 | port2 | port 3 | port 4
    PORT_STATUS ::= active | inactive

   Switch also has ports for input or output and each port has a state (
   active or inactive ). In this specification, we assume that the
   switch has four ports.

    ACTION ::= Forward | Enqueue | Drop | Modify_Field
    OPTIONAL_ACTION ::=ALL | CONTROLLER | LOCAL | TABLE | IN_PORT | NONE
    ACTION_TYPE: ACTION <-> OPTIONAL_ACTION
    ACTION_TYPE Forward = {ALL, CONTROLLER, LOCAL, TABLE, IN_PORT}
    ACTION_TYPE Enqueue = NONE
    ACTION_TYPE Drop = NONE
    ACTION_TYPE Modify_Field = NONE

   Actions stored in table are Forward, Enqueue, Drop and Modify Field,
   and forward action has four optional actions, ALL (meaning
   broadcast), LOCAL (multicast), IN PORT (unicast) and Controller (to
   controller).

    forwardToController
    headerNoMatchAction
    packet: PACKET_TYPE
    packet.header =packet?.header
    packet.contents=packet?.contents
    packet.action={(Forward, CONTROLLER)}
    controller.packet={packet}

   Z specification for SDN is focused on each switch and controller for
   emphasis on their functionality and it is possible of limited
   verification for SDN using Z specification. It can specify forwarding
   packets in limited hosts and switches, but it is difficult to specify
   various states of large networks in the real-world.


   4.3 Subtle Ambiguities Discovery and Correctness Verification



Shin et al.,             Expires December 2012                  [Page 9]

Internet-Draft        Formal Specification for SDN         June 29, 2012


   We could find the overlooked subtleties in SDN networks during
   transforming from the topology and properties to ACSR and Z
   specification. Once a formal specification is made, it can be used
   for validating the network topology.

   For example, in order to prove that the correctness of the ACSR and Z
   specifications, we can show that the specification has no deadlock.
   If the specification has no deadlock, we can claim that the network
   topology runs forever without any stop, which means the packet flow
   is well modeled.


5.  Security Considerations

   TBD


6. Acknowledgements

   The authors would like to thank theory and formal methods lab members
   in Korea University for their process algebraic specification
   support.


7.  References

7.1.  Normative References

   [RFC2119]  Bradner, S., "Key words for use in RFCs to Indicate
              Requirement Levels", BCP 14, RFC 2119, March 1997.


7.2.  Informative References

   [I-D.nadeau-sdn-problem-statement] Nadeau, T., and P. Pan, "Software
              Defined Network (SDN) Problem Statement", draft-nadeau-
              sdn-problem-statement-00 (work in progress), September
              2011.

   [b-OpenFlow] OpenFlow Switch Specification 1.3,
              https://www.opennetworking.org/.

   [b-Kang12] M. Kang et al., Formal Specification for Software-Defined
              Networks (SDN), CFI'12 (submitted), 2012.

   [b-Nam12] K-H. Nam, et al., Draft Document of Y.FNsdn-fm
              "Requirements of formal specification and verification
              methods for software-defined networking, ITU-T (work in



Shin et al.,             Expires December 2012                 [Page 10]

Internet-Draft        Formal Specification for SDN         June 29, 2012


              progress), 2012.

   [b-NetCore12] C. Monsanto, N. Foster, R. Harrison,and D. Walker, A
              Compiler and Runtime System for Network Programming
              Languages, POPL Jan.2012. To appear.

   [b-NDlog11] A. Wang, L. Jia, C. Liu, B. Loo, O. Sokolsky, and P.
              Basu, Formally Verifiable Networking,2011.

   [b-ACSR95] J. Choi, I. Lee, and H. Xie, The Specificatoin and
              Schedulability Analysis of Real-Time Systems Using ACSR,
              16th IEEE Real-Time Systems Symp.(RTSS'95), Dec. 1995.







































Shin et al.,             Expires December 2012                 [Page 11]

Internet-Draft        Formal Specification for SDN         June 29, 2012


Authors' Addresses

      Myung-Ki Shin
      ETRI
      161 Gajeong-dong Yuseng-gu
      Daejeon, 305-700
      Korea

      Phone: +82 42 860 4847
      Email: mkshin@etri.re.kr


      Ki-Hyuk Nam
      ETRI
      161 Gajeong-dong Yuseng-gu
      Daejeon, 305-700
      Korea

      Phone: +82 42 860 5729
      Email: nam@etri.re.kr


      Miyoung Kang
      Korea University
      Anam-dong, Seongbuk-gu
      Seoul, 136-713
      Korea

      Phone: +82 2 3290 3200
      Email: mykang@formal.korea.ac.kr


      Jin-Young Choi
      Korea University
      Anam-dong, Seongbuk-gu
      Seoul, 136-713
      Korea

      Phone: +82 2 3290 3200
      Email: choi@formal.korea.ac.kr











Shin et al.,             Expires December 2012                 [Page 12]


Html markup produced by rfcmarkup 1.109, available from https://tools.ietf.org/tools/rfcmarkup/