Abstract
The role of software and its flexibility is becoming more and more important in todays networks. New emerging paradigms, such as Software Defined Networking (SDN) and Network Function Virtualization (NFV), are changing the rules of the game, shifting the focus on dynamicity and programmability. Perfectly aligned with this new spirit, the FP7 UNIFY European project aims at realizing this appealing vision by applying DevOps concepts to telecom operator networks and supporting the idea of fast network reconfiguration. However, the increased range of possibilities offered by the DevOps approach comes at the cost of designing new processes and toolkits to make SDN and NFV a concrete opportunity. In this paper we specifically focus on the verification process as part of the challenging tasks that must be addressed in this scenario and its fundamental role of automatically checking some desired network properties before deploying a particular configuration. Our preliminary results confirm the feasibility of the approach and encourage future efforts in this direction.
Chapter PDF
Similar content being viewed by others
References
de Moura, L., Bjørner, N.S.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Jain, R., Paul, S.: Network virtualization and software defined networking for cloud computing: A survey. IEEE Communications Magazine 51(11), November 2013
John, W., Meirosu, C.: Unify d4.1: Initial requirements for the sp-devops concept, universal node capabilities and proposed tools (2014). https://www.fp7-unify.eu/index.php/results.html#Deliverables
John, W., Pentikousis, K., Agapiou, G., Jacob, E., Kind, M., Manzalini, A., Risso, F., Staessens, D., Steinert, R., Meirosu, C.: Research directions in network service chaining. In: 2013 IEEE SDN for SDN4FNS, November 2013
Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: Static checking for networks. In: NSDI 2012. USENIX, San Jose (2012)
Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.B.: Veriflow: Verifying network-wide invariants in real time. In: NSDI 2013. USENIX, Lombard (2013)
Meirosu, C.: m4.1: Sp-devops concept evolution and initial plans for prototyping (2014). https://www.fp7-unify.eu/index.php/results.html#Deliverables
Panda, A., Lahav, O., Argyraki, K.J., Sagiv, M., Shenker, S.: Verifying isolation properties in the presence of middleboxes. CoRR abs/1409.7687 (2014)
Porras, P., Shin, S., Yegneswaran, V., Fong, M., Tyson, M., Gu, G.: A security enforcement kernel for openflow networks. In: HotSDN 2012. ACM, New York (2012)
Sharma, S., Coyne, B.: DevOps For Dummies. Limited IBM Edition’ book, October 2013
Son, S., Shin, S., Yegneswaran, V., Porras, P.A., Gu, G.: Model checking invariant security properties in openflow. In: ICC, pp. 1974–1979. IEEE (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Spinoso, S., Virgilio, M., John, W., Manzalini, A., Marchetto, G., Sisto, R. (2015). Formal Verification of Virtual Network Function Graphs in an SP-DevOps Context. In: Dustdar, S., Leymann, F., Villari, M. (eds) Service Oriented and Cloud Computing. ESOCC 2015. Lecture Notes in Computer Science(), vol 9306. Springer, Cham. https://doi.org/10.1007/978-3-319-24072-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-24072-5_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24071-8
Online ISBN: 978-3-319-24072-5
eBook Packages: Computer ScienceComputer Science (R0)