Network Working Group M-K. Shin Internet-Draft S. Lee Intended status: Informational ETRI Expires: October 2014 February 12, 2014 Formal Verification for Software-Defined Networks (SDN) draft-shin-sdnrg-formal-verification-00 Abstract 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 verified to prevent from misinterpreting of the intended meanings and to avoid inconsistency in the networks. This document discusses basic requirements, framework, and case studies of formal verification for SDN. 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. The list of Internet-Draft Shadow Directories can be accessed at http://www.ietf.org/shadow.html. Shin et al., Expires October 2014 [Page 1] Internet-Draft Formal Specification for SDN February 12, 2014 This Internet-Draft will expire on September 1, 2013. 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. SDN Discussion and Assumption ...................................3 3. Basic Requirements of SDN Application Verification ..............4 4. Formal Verification Framework for SDN ...........................5 5. Case Study : Formal Language - pACSR ...........................5 6. Case Study : Case Study : Symbolic Verification and Properties ..7 6. Security Considerations .........................................8 7. Acknowledgements ................................................8 8. References ......................................................8 8.1 Normative References .........................................8 8.2 Informative References .......................................8 Authors' Addresses ................................................10 Shin et al., Expires October 2014 [Page 2] Internet-Draft Formal Specification for SDN February 12, 2014 1. Introduction Software-defined networking (SDN) is defined as a technology to enable network operators to directly control and manage their networks and resources to best serve their needs by writing simple software. In SDN world, it becomes important to verify the safety properties of SDN using formal method before the deployment of SDN applications. This document discusses basic requirements, framework, and case studies of formal verification for SDN. 2. SDN Discussion and Assumption SDN architectural issues are not fully investigated yet, because it is very hard to build a single SDN architecture to accommodate and harmonize various requirements from network operators, application/service providers and vendors' perspectives. In this document, it is assumed that SDN has three-tier architecture as illustrated in Figure 1. +----+ +----+ +----+ Tier-3 |SDN | |SDN | |SDN | |Apps| |Apps| |Apps| .... | | | | | | +----+ +----+ +----+ - - - - - - - - - - - - - - Open Interface Tier-2 +------------------------------+ | SDN Control Software | +------------------------------+ - - - - - - - - - - - - - - Open Interface +--------+ +--------+ +--------+ Tier-1 | SDN | | SDN | | SDN | ... | Devices| | Devices| | Devices| +--------+ +--------+ +--------+ Figure 1 Three-Tier Architecture for SDN o Tier-1 : Forwarding entities and any software/hardware components comprising of them o Tier-2 : Control and management entities for the Tier-1 o Tier-3 : Applications and services that take advantage of the infrastructures based on Tier-1 and Tier-2. Shin et al., Expires October 2014 [Page 3] Internet-Draft Formal Specification for SDN February 12, 2014 3. Basic Requirements of SDN Application Verification Formal methods for SDN can fit in any of those Tiers or in between two Tiers as shown in Figure 1. Key requirements of applying formal methods to SDN can be identified as follows: R1. Programmable network devices can be customized in software or hardware, or combination of them, depending on the requirements from network operators to produce optimal solution for their uses. Formal methods for SDN can help guarantee that the design and the implementation of programmable network devices conform to the standards, correctness and safety properties. R2. Network operators in SDN can check consistency and safety of their network configurations and virtual/physical topologies by formally verifying their configuration against any properties to be satisfied with such as: - No loops and/or blackholes in the network. - No rule or behavior conflicts between multiple applications in a controller software - Logically different networks cannot interfere with each other (e.g., traffic isolation). - New or update configurations conforms to properties of the network and do not break consistency of existing networks (e.g., dynamic network update). R3. Support of formal semantics in languages, APIs, and underlying protocols for SDN - Languages that interface with control and management entities should have formal semantics to avoid any confusion in the interpretation of underlying mechanism and/or network configuration. - Description of programmable network devices' behavior such as switches, and protocols for controlling those devices, need to be proved safe and consistent to provide stable foundation of the SDN application and services. R4. Support of conceptual models to reason about networks defined, configured, implemented by software and hardware for SDN more precisely. - Timing models that capture essential properties and behaviors of packet flows and data traffic in SDN-based networks. - Formalisms that reflect networks and systems behaviors. - High-level programming languages and tools (e.g., compiler, debugger, etc.) based on the conceptual model can be developed. Shin et al., Expires October 2014 [Page 4] Internet-Draft Formal Specification for SDN February 12, 2014 4. Formal Verification Framework for SDN In this clause, we present a formal verification framework for SDN. in this framework, a set of toolset including SDN language compiler and verifier, etc. on top of SDN control software. Figure 2 illustrates formal verification framework for SDN applications. +----+ +----+ +----+ Tier-3 |SDN | |SDN | |SDN | |Apps| |Apps| |Apps| .... | | | | | | +----+ +----+ +----+ - - - - - - - - - - - - - - Open Interface +------------------------------+ | +-------------+ +----------+ | | |SDN languages| | Verifier | | | +-------------+ +----------+ | | +--------------------------+ | | | SDN compilers | | | +--------------------------+ | Tier-2 +------------------------------+ | SDN Control Software | +------------------------------+ - - - - - - - - - - - - - - Open Interface +--------+ +--------+ +--------+ Tier-1 | SDN | | SDN | | SDN | ... | Devices| | Devices| | Devices| +--------+ +--------+ +--------+ Figure 2 SDN formal language and verification tools 5. Case Study : Formal Language - pACSR There have been continuous efforts and progresses regarding the research on the formal verification for SDN. However, we observe that there are still issues to make these works practical. First, semantics to abstract consistent network updates should be embedded into SDN protocols. Also, the notion of SDN resource (e.g., OpenFlow's flow table) in a formal language should be suited to model time consumed concurrently by the each SDN devices. Lastly, its verification method should be enough to be scalable with a number of large and complex SDN resources and devices. The novel aspect of our approach is to add semantics transparently into SDN operations with timed process algebra. In case of OpenFlow protocol, with the global flow table and DBs maintained by a logically-centralized controller, the flow table's behaviors and its status can be dynamically Shin et al., Expires October 2014 [Page 5] Internet-Draft Formal Specification for SDN February 12, 2014 translated with minimum semantics in our Packet Algebra of Communicating Shared Resources (pACSR) language and analyzed automatically, all within a process-algebraic and symbolic verification framework. Our work is a step toward such an integration, which helps to verify and debug SDN applications by making the timed process algebra - pACSR a useful formalism for supporting the development of reliable SDN applications. In addition, the newly-added semantics is transparent to both SDN application (e.g., C, Java, etc.) programmers and operators so the underlying verification process is hidden to them and there is no burden to understand the details of formal verification method by them. ACSR is a formal language for behavior modeling using concepts of processes, resources, events, and priorities, which was originally developed for the formal verification of real-time embedded systems and CPS (Cyber Physical Systems). In both CPS and SDN, software is the key because it's the software that determines system and network complexity. So, there are the same issues on how to model and abstract their real-time, concurrent behaviors and feedback controls. ACSR, like other process algebras, consists of a set of operators and syntactic rules for constructing process; a semantic mapping which assigns meaning or interpretation to processes; a notion of equivalence or partial order between process; and 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. In this document, pACSR (Packet ACSR, pronounced as "pacser") extends the process algebra ACSR by allowing network packets to be communicated along network ports to describe SDN protocols' behaviors. In pACSR, values passed through ports are network packets (packet passing) and packets can also be passed as parameters for process. The following pACSR description shows a simple example of semantics with packet passing and parameterized process with packet, which could be seamlessly added in the global flow table's behaviors managed by OpenFlow controller. P(x) := matchSrcPacket(x,field) -> port!x.nil S := port?y.nil Sys := (P(x) || S)/{port} P(x) represents a process that has packet x as a parameter. Once process P gets a packet x, it checks with a predefined predicate matchSrcPacket(). If the condition in a match field of packet x is satisfied, process P sends packet x through port which is represented as port!x. After the egress of packet x, process P becomes nil. Otherwise, it becomes nil also in this example. In case of process S, it gets packet through port and names it as y and becomes nil. Shin et al., Expires October 2014 [Page 6] Internet-Draft Formal Specification for SDN February 12, 2014 Process Sys represents parallel composition of P(x) and S, that is process P(x) and S are running in parallel. pACSR has other features such as predefined predicates (PP) and predefined functions (PF). The term matchSrcPacket in example above is the PP. There could be many predicates predefined as need as long as they don't have side effects. 6. Case Study : Symbolic Verification and Properties Since pACSR is the fundamental formal language for the verification framework, it needs to be analyzed symbolically during symbolic verification stage. So, pACSR language compiler and symbolic verification toolset are placed between a SDN controller and set of devices. The global flow table managed by a centralized controller is dynamically translated into pACSR description in an event-driven way, by the pACSR generator to capture the semantics of OpenFlow's flow table. The property verifier reads pACSR description and internally generates symbolic transition graph (STG) from pACSR description. Then symbolic verification algorithm for a given property will be applied onto STG and the Boolean expression is generated as a verification result that should be satisfied for the verified property to be valid. The verification properties could be classified as follows : o Basic network properties - No loop - No blackhole (e.g., packet loss) - Performance checking - Security holes, etc. o SDN-specific properties - OF rule consistency between multiple applications - Dynamic info/statistics consistency (e.g., flow, port, QoS, etc.) - Consistency with legacy protocols (e.g., STP) This verification framework is naturally suited to model SDN, since pACSR is expressive enough to represent timed process and real-time software behaviors. So it can model packet passing between switches concurrently so that it allows to model flow tables naturally. The notion of resource in pACSR is also well suited to model time consumed by the each switches. Furthermore, the PP and PF allows pACSR to model the relatively complex behavior of SDN switches. Due to the fact that the complexity caused by complex behavior of switches are described using PP and PF, the state explosion problem occurring during resolution of parallel composition and the notion of choice operation tends to be reduced. With our proposed approach, the Shin et al., Expires October 2014 [Page 7] Internet-Draft Formal Specification for SDN February 12, 2014 complexity of parallelism and the complexity of verification algorithm are separated in the sense that the parallelism is handled by process algebraic formal language, pACSR, and verification only need to be based on graph theoretic algorithms. We have developed an early prototype to support the pACSR description and its symbolic verification as a kind of application/toolset on top of FloodLight controller. We believe that this toolset will allow us to experimentally evaluate the effectiveness of our approach with a number of large scale SDN systems. We also think other SDN and NFV protocols, such as I2RS, segment routing, NFV forwarding graph and service functions chains, could be also similarly represented and verified by abstracting and adding these-like semantics according to their protocol behaviors. 6. Security Considerations TBD 7. Acknowledgements The authors would like to thank theory and formal methods lab members in Korea University for their process algebraic specification support. 8. References 8.1. Normative References [RFC2119] Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels", BCP 14, RFC 2119, March 1997. 8.2. Informative References [b-Nate11] N. Foster, R. Harrison, M. L. Meola, M. J. Freedman, J. Rexford, and D. Walker, Frenetic:A High-Level Language for OpenFlow Networks, ICFP, 2011. [Frenetic] Frenetic project http://frenetic-lang.org/index.php [b-Kang12] M. Kang et al., Formal Specification for Software-Defined Networks (SDN), CFI'12, 2012. [b-Yi13] J. Yi, et al., Draft Recommendation of Y.FNsdn-fm "Requirements of formal specification and verification methods for software-defined networking, ITU-T (work in Shin et al., Expires October 2014 [Page 8] Internet-Draft Formal Specification for SDN February 12, 2014 progress), 2013. [b-Kwak98a] H. Kwak, J. Choi, I. Lee, and A. Philippou. Symbolic weak bisimulation for value-passing calculi. Technical Report, MS-CIS-98-22, Department of Computer and Information Science, University of Pennsylvania, 1998. [b-Kwak98b] H. Kwak, I. Lee, A. Philippou, and J. Choi, Symbolic Schedulability Analysis of Real-time Systems, In IEEE Real-Time Systems Symposium, December 1998. [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 October 2014 [Page 9] Internet-Draft Formal Specification for SDN February 12, 2014 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 Seungik Lee ETRI 161 Gajeong-dong Yuseng-gu Daejeon, 305-700 Korea Phone: +82 42 860 1483 Email: seungiklee@etri.re.kr Shin et al., Expires October 2014 [Page 10]