1、 I n t e r n a t i o n a l T e l e c o m m u n i c a t i o n U n i o n ITU-T Y.3320 TELECOMMUNICATION STANDARDIZATION SECTOR OF ITU (08/2014) SERIES Y: GLOBAL INFORMATION INFRASTRUCTURE, INTERNET PROTOCOL ASPECTS AND NEXT-GENERATION NETWORKS Future networks Requirements for applying formal methods t
2、o software-defined networking Recommendation ITU-T Y.3320 ITU-T Y-SERIES RECOMMENDATIONS GLOBAL INFORMATION INFRASTRUCTURE, INTERNET PROTOCOL ASPECTS AND NEXT-GENERATION NETWORKS GLOBAL INFORMATION INFRASTRUCTURE General Y.100Y.199 Services, applications and middleware Y.200Y.299 Network aspects Y.3
3、00Y.399 Interfaces and protocols Y.400Y.499 Numbering, addressing and naming Y.500Y.599 Operation, administration and maintenance Y.600Y.699 Security Y.700Y.799 Performances Y.800Y.899 INTERNET PROTOCOL ASPECTS General Y.1000Y.1099 Services and applications Y.1100Y.1199 Architecture, access, network
4、 capabilities and resource management Y.1200Y.1299 Transport Y.1300Y.1399 Interworking Y.1400Y.1499 Quality of service and network performance Y.1500Y.1599 Signalling Y.1600Y.1699 Operation, administration and maintenance Y.1700Y.1799 Charging Y.1800Y.1899 IPTV over NGN Y.1900Y.1999 NEXT GENERATION
5、NETWORKS Frameworks and functional architecture models Y.2000Y.2099 Quality of Service and performance Y.2100Y.2199 Service aspects: Service capabilities and service architecture Y.2200Y.2249 Service aspects: Interoperability of services and networks in NGN Y.2250Y.2299 Enhancements to NGN Y.2300Y.2
6、399 Network management Y.2400Y.2499 Network control architectures and protocols Y.2500Y.2599 Packet-based Networks Y.2600Y.2699 Security Y.2700Y.2799 Generalized mobility Y.2800Y.2899 Carrier grade open environment Y.2900Y.2999 FUTURE NETWORKS Y.3000Y.3499 CLOUD COMPUTING Y.3500Y.3999 For further de
7、tails, please refer to the list of ITU-T Recommendations. Rec. ITU-T Y.3320 (08/2014) i Recommendation ITU-T Y.3320 Requirements for applying formal methods to software-defined networking Summary Recommendation ITU-T Y.3320 provides a descriptive overview and requirements for applying formal methods
8、 to software-defined networking (SDN). Appendix I, introduces an example demonstrating how formal methods are applied to SDN environments. Formal methods are mathematics-based techniques used for specifying, developing, and verifying software and hardware systems and are expected to increase the rel
9、iability and robustness of the system. In SDN environments the consistency, reliability and security of applications are important as incomplete or malicious programmable entities could cause a break-down of underlying networks. In this sense, the use of formal methods can be an effective approach t
10、o the mitigation of such problems. History Edition Recommendation Approval Study Group Unique ID* 1.0 ITU-T Y.3320 2014-08-29 13 11.1002/1000/12284 Keywords Formal methods, formal specification, formal verification, future network, software defined networking. _ * To access the Recommendation, type
11、the URL http:/handle.itu.int/ in the address field of your web browser, followed by the Recommendations unique ID. For example, http:/handle.itu.int/11.1002/1000/11830-en. ii Rec. ITU-T Y.3320 (08/2014) FOREWORD The International Telecommunication Union (ITU) is the United Nations specialized agency
12、 in the field of telecommunications, information and communication technologies (ICTs). The ITU Telecommunication Standardization Sector (ITU-T) is a permanent organ of ITU. ITU-T is responsible for studying technical, operating and tariff questions and issuing Recommendations on them with a view to
13、 standardizing telecommunications on a worldwide basis. The World Telecommunication Standardization Assembly (WTSA), which meets every four years, establishes the topics for study by the ITU-T study groups which, in turn, produce Recommendations on these topics. The approval of ITU-T Recommendations
14、 is covered by the procedure laid down in WTSA Resolution 1. In some areas of information technology which fall within ITU-Ts purview, the necessary standards are prepared on a collaborative basis with ISO and IEC. NOTE In this Recommendation, the expression “Administration“ is used for conciseness
15、to indicate both a telecommunication administration and a recognized operating agency. Compliance with this Recommendation is voluntary. However, the Recommendation may contain certain mandatory provisions (to ensure, e.g., interoperability or applicability) and compliance with the Recommendation is
16、 achieved when all of these mandatory provisions are met. The words “shall“ or some other obligatory language such as “must“ and the negative equivalents are used to express requirements. The use of such words does not suggest that compliance with the Recommendation is required of any party. INTELLE
17、CTUAL PROPERTY RIGHTSITU draws attention to the possibility that the practice or implementation of this Recommendation may involve the use of a claimed Intellectual Property Right. ITU takes no position concerning the evidence, validity or applicability of claimed Intellectual Property Rights, wheth
18、er asserted by ITU members or others outside of the Recommendation development process. As of the date of approval of this Recommendation, ITU had received notice of intellectual property, protected by patents, which may be required to implement this Recommendation. However, implementers are caution
19、ed that this may not represent the latest information and are therefore strongly urged to consult the TSB patent database at http:/www.itu.int/ITU-T/ipr/. ITU 2015 All rights reserved. No part of this publication may be reproduced, by any means whatsoever, without the prior written permission of ITU
20、. Rec. ITU-T Y.3320 (08/2014) iii Table of Contents Page 1 Scope . 1 2 References . 1 3 Definitions 1 3.1 Terms defined elsewhere 1 3.2 Terms defined in this Recommendation . 2 4 Abbreviations and acronyms 2 5 Conventions 2 6 Introduction . 2 7 Overview of applying formal methods to software-defined
21、 networking 3 8 Functional requirements . 5 8.1 General requirements (GR) 5 8.2 Requirements of formal specification (FS) 5 8.3 Requirements of formal verification (FV) 5 8.4 Miscellaneous . 6 9 Environmental considerations 6 10 Security considerations . 7 Appendix I Overview of formal methods for n
22、etworking 8 I.1 High level operational model of SDN and formal methods tool 8 I.2 Formal specification tool 8 I.3 Formal verification tool 9 Bibliography. 11 Rec. ITU-T Y.3320 (08/2014) 1 Recommendation ITU-T Y.3320 Requirements for applying formal methods to software-defined networking 1 Scope This
23、 Recommendation describes requirements for using formal methods. Formal methods are mathematics-based techniques used to specify, develop and verify software and hardware systems in the context of software-defined networking (SDN) for future networks (FN). The scope of this Recommendation covers: an
24、 overview of formal methods (formal specification and formal verification) for SDN, and requirements for applying formal methods to SDN. An example of how to apply formal methods to SDN is provided in Appendix I. 2 References The following ITU-T Recommendations and other references contain provision
25、s which, through reference in this text, constitute provisions of this Recommendation. At the time of publication, the editions indicated were valid. All Recommendations and other references are subject to revision; users of this Recommendation are therefore encouraged to investigate the possibility
26、 of applying the most recent edition of the Recommendations and other references listed below. A list of the currently valid ITU-T Recommendations is regularly published. The reference to a document within this Recommendation does not give it, as a stand-alone document, the status of a Recommendatio
27、n. ITU-T Y.3001 Recommendation ITU-T Y.3001 (2011), Future networks: Objectives and design goals. ITU-T Y.3011 Recommendation ITU-T Y.3011 (2012), Framework of network virtualization for future networks. ITU-T Y.3300 Recommendation ITU-T Y.3300 (2014), Framework of software-defined networking. 3 Def
28、initions 3.1 Terms defined elsewhere This Recommendation uses the following terms defined elsewhere: 3.1.1 future network ITU-T Y.3001: A network able to provide services, capabilities and facilities difficult to provide using existing network technologies. A future network is either: a) A new compo
29、nent network or an enhanced version of an existing one, or b) A heterogeneous collection of new component networks or of new and existing component networks that is operated as a single network. 3.1.2 network virtualization ITU-T Y.3011: A technology that enables the creation of logically isolated n
30、etwork partitions over shared physical networks so that heterogeneous collections of multiple virtual networks can simultaneously coexist over the shared networks. This includes the aggregation of multiple resources in a provider and appearing as a single resource. 3.1.3 software-defined networking
31、ITU-T Y.3300: A set of techniques that enables to directly program, orchestrate, control and manage network resources, which facilitates the design, delivery and operation of network services in a dynamic and scalable manner. 2 Rec. ITU-T Y.3320 (08/2014) 3.2 Terms defined in this Recommendation Non
32、e. 4 Abbreviations and acronyms This Recommendation uses the following abbreviations and acronyms: FN Future Network SDN Software-Defined Networking 5 Conventions In this Recommendation, the following conventions are used: The keywords “is required to“ indicate a requirement which must be strictly f
33、ollowed and from which no deviation is permitted, if conformance to this Recommendation is to be claimed. The keywords “is recommended“ indicate a requirement which is recommended but which is not absolutely required. Thus this requirement need not be present to claim conformance. The keywords “can
34、optionally“ indicate an optional requirement which is permissible, without implying any sense of being recommended. This term is not intended to imply that the vendors implementation must provide the option and the feature can be optionally enabled by the network operator/service provider. Rather, i
35、t means the vendor may optionally provide the feature and still claim conformance with the specification. 6 Introduction Formal methods are software engineering techniques based on the mathematical representation and analysis of software programs and/or hardware. They include formal specification, a
36、nalysis of specification and formal verification of software and/or hardware behaviour b-Clarke. The formal specification describes the semantics of a system using mathematical representation. The formal verification is the act of proving or disproving the correctness of designs or implementations w
37、ith respect to the formal specification. Objectives and design goals for future networks are described in ITU-T Y.3001 which also identifies the high-level capabilities and characteristics that need to be supported by such future networks. To design and implement systems that conform to the design g
38、oals identified in ITU-T Y.3001, the structure and behaviour of the systems need to be described in a way that prevents misinterpretation of the intended meanings and that avoids inconsistency in the systems. FNs may be used for mission critical systems and/or other areas, such as private clouds and
39、 data centers, where systems have significant requirements for reliability and consistency and where otherwise a catastrophic disaster could occur. ITU-T Y.3300 describes the framework and fundamentals of SDN which it describes as a new networking approach that enables network resources to be direct
40、ly programed, orchestrated and controlled. Finally ITU-T Y.3011 describes network abstraction into networks that manage the virtualization of the networks. SDN facilitates network operators to introduce new capabilities by writing simple software programs that control the network in a programmable w
41、ay. In SDN based networks it is important to check the consistency and security properties of these programs before their installation or deployment in the network. Rec. ITU-T Y.3320 (08/2014) 3 As described previously, an effective approach to increasing reliability and reducing any misunderstandin
42、g or inconsistency of the meaning of the systems or programs is the adoption of formal methods. Formal methods help network operators and application developers protect their systems from unexpected errors that might not be caught during the development and deployment process. 7 Overview of applying
43、 formal methods to software-defined networking Figure 1 illustrates the overall flow from the informal description of the conceptual model, logical design and domain specific network through to the implementation of a system using formal methods. Figure 1 Overall flow of formal methods Traditional m
44、ethods for realizing network protocols and devices are based on community agreements on informal descriptions of such mechanisms b-Griffin. As depicted in Figure 1, these traditional methods can be improved by applying formal methods to the development process of software-defined networking b-Wang.
45、Targets of specification can conceptually model components or mechanisms, logical switch/router models, network protocols, topologies of virtual networks and so on. Informal descriptions of those targets can be encoded in formal specification languages that can reflect the features of targets of the
46、 existing methods. The formal specification can be in textual or graphical form to represent their semantics. Once the specifications are described formally, system and network designers can check for the existence of inconsistencies and possible errors in the specification with the help of formal m
47、ethods experts and/or supporting tools. Various types of formal verification methods (e.g., theorem proving, model checking and static analysis) can be applied to the validation and verification process. The high-level architecture of SDN consists of four layers as defined in ITU-T Y.3300: Applicati
48、on layer SDN control layer Resource layer Management functions multi-layer In order to provide formal methods to SDN, additional functions comprised in the formal methods component are needed to process the formal specification and the formal verification, (see Figure 2). The formal specification fu
49、nction provides an application-formal methods interface for 4 Rec. ITU-T Y.3320 (08/2014) SDN applications to express their semantics in a formal representation. The formal verification function provides a control-formal methods interface for the SDN controller to check whether new semantics can cause errors or operational conflicts within the network. Figure 2 Relationship between the formal methods component and the high-level SDN architecture The formal methods component su
