Internet DRAFT - draft-shin-sdnrg-formal-verification
draft-shin-sdnrg-formal-verification
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]
