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]