Internet DRAFT - draft-shin-sdn-formal-specification
draft-shin-sdn-formal-specification
Network Working Group M-K. Shin
Internet-Draft K-H. Nam
Intended status: Informational ETRI
Expires: October 2013 M. Kang
J. Choi
Korea U.
February 15, 2013
Formal Specification Framework for Software-Defined Networks (SDN)
draft-shin-sdn-formal-specification-03
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
languages.
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 October 2013 [Page 1]
Internet-Draft Formal Specification for SDN February 15, 2013
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. SDN Discussion and Assumption ...................................3
2.1 Requirements for SDN Programming .............................4
3. Formally Verifiable Networking Framework for SDN ................5
4. Formal Specification and Verification for SDN ...................6
5. Examples ........................................................7
5.1 Formal Specification of SDN using ACSR ......................7
5.2 Formal Specification of SDN using Z .........................10
5.3 Subtle Ambiguities Discovery and Correctness Verification ...12
6. Security Considerations ........................................12
7. Acknowledgements ...............................................12
8. References .....................................................12
8.1 Normative References ........................................12
8.2 Informative References ......................................13
Authors' Addresses ................................................14
Shin et al., Expires October 2013 [Page 2]
Internet-Draft Formal Specification for SDN February 15, 2013
1. Introduction
Software-defined networking (SDN) is emerging and intensively
discussed as one of the most promising technologies to make networks
programmable and flexible and 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 so that they can directly control and manage
their networks and resources to best serve their customers' needs.
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. SDN Discussion and Assumption
SDN architectural issues are not fully investigated yet, because it
is very difficult to build a single SDN architecture to accommodate
and harmonize various requirements from network operators,
application/service providers and vendors' perspectives. Therefore,
it is assumed that SDN has three-tier architecture as illustrated in
Figure 1.
Shin et al., Expires October 2013 [Page 3]
Internet-Draft Formal Specification for SDN February 15, 2013
+----+ +----+ +----+
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.
2.1 Requirements for SDN Programming
This document presents initial thoughts on requirements of SDN
application programming.
R1: Guarantee that the design and implementation of SDN devices
conforms to the standards, correctness and safety properties.
R2: Check consistency and safety of their network configurations
and virtual and physical topologies against any properties to
be satisfied with such as:
- No loops and/or blackholes in the network
- 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., network updates)
R3: Support formal semantics in high-level languages, APIs and
underlying protocols for SDN
- Properties that need to be satisfied with by the SDN should
be described in notations with formal semantics
R4: Support conceptual models to reason about networks defined,
configured, implemented by software and hardware for SDN more
precisely.
- Timing models that capture essential properties and
Shin et al., Expires October 2013 [Page 4]
Internet-Draft Formal Specification for SDN February 15, 2013
behaviors of packet flows and data traffic in
- Formalisms that reflect networks and systems behaviors
- Diverse languages and tools based on the conceptual model
3. 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
algebraic analysis, model checking, and static analysis.
Figure 2 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 2, 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
Shin et al., Expires October 2013 [Page 5]
Internet-Draft Formal Specification for SDN February 15, 2013
specifying important properties in temporal logics and feed them into
model checking tools such as SPIN and SMV [b-Nam12].
+----------- 0.Design abstract
| network model using
v informal specifications
+---------------+ (e.g., virtual network
| 1.Formal | topology etc.)
| specification |
+---------------+
|
v
+---------------+ +--------+ +---------+
| +--| Model | |Invariant| ...
| 2.Verification| |checking| |checker |
| methods | +--------+ +---------+
| | +--------+
| +--|Theorem | ...
+---------------+ |proving |
| +--------+
v
+-------------------+
| 3.Implementation |
| (control software)|
+-------------------+
^
|
v
.---------------------.
/ SDN Data plane \
' (heterogeneous devices, '
\ switches, etc. /
`-----------------------'
Figure 2 Formally verifiable networking framework for SDN
4. Formal Specification and Verification 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 October 2013 [Page 6]
Internet-Draft Formal Specification for SDN February 15, 2013
In this document, we propose to add SDN language compiler and tools
such as verifier on top of SDN control software. Figure 3 illustrates
formal specification and verification tools between SDN control
software and 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 3 SDN formal language and tools
We consider developing new formal specification language with simple
and minimum semantics to support new properties of SDN networks. 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 SDN through the analysis of the requirement
for OpenFlow.
Shin et al., Expires October 2013 [Page 7]
Internet-Draft Formal Specification for SDN February 15, 2013
5. Examples
5.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 4.
The topology consists of a single switch and three hosts (H1, H2, and
H3).
--------
+--->| Switch |---+
| -------- |
| | |
| v v
---- ---- ----
| H1 | | H2 | | H3 |
---- ---- ----
Figure 4 Example virtual topology
An abstract view point is used to model packets by abstracting out
Shin et al., Expires October 2013 [Page 8]
Internet-Draft Formal Specification for SDN February 15, 2013
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 October 2013 [Page 9]
Internet-Draft Formal Specification for SDN February 15, 2013
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.
5.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 October 2013 [Page 10]
Internet-Draft Formal Specification for SDN February 15, 2013
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.
Shin et al., Expires October 2013 [Page 11]
Internet-Draft Formal Specification for SDN February 15, 2013
5.3 Subtle Ambiguities Discovery and Correctness Verification
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.
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
[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, 2012.
[b-Nam12] K-H. Nam, et al., Draft Document of Y.FNsdn-fm
Shin et al., Expires October 2013 [Page 12]
Internet-Draft Formal Specification for SDN February 15, 2013
"Requirements of formal specification and verification
methods for software-defined networking, ITU-T (work in
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 October 2013 [Page 13]
Internet-Draft Formal Specification for SDN February 15, 2013
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 October 2013 [Page 14]
