Skip to main content
SpringerLink
Log in

A Declarative Approach to Network Device Configuration Correctness

  • Published:
Journal of Network and Systems Management Aims and scope Submit manuscript

Abstract

Configuration Logic (CL) is a formal language that allows a network engineer to express constraints in terms of the actual parameters found in the configuration of network devices. We present an efficient algorithm that can automatically check a pool of devices for conformance to a set of CL constraints; moreover, this algorithm can point to the part of the configuration responsible for the error when a constraint is violated. Contrary to other validation approaches that require dumping the configuration of the whole network to a central location in order to be verified, we also present an algorithm that analyzes the correct formulas and greatly helps reduce the amount of data that need to be transferred to that central location, pushing as much of the evaluation of the formula locally on each device. The procedure is also backwards-compatible, in such a way that a device that does not (or only partially) supports a local evaluation may simply return a subset or all of its configuration. These capabilities have been integrated into a network management tool called ValidMaker.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Similar content being viewed by others

Notes

  1. In programming, lazy evaluation is the process of fetching only the parts of a data structure or object passed as an argument to a function that are actually accessed by that function.

  2. “Yet Another Network Language”.

  3. Namely: \(\lnot (\varphi \vee \psi ) = \lnot \varphi \wedge \lnot \psi \), \(\lnot (\varphi \wedge \psi ) = \lnot \varphi \vee \lnot \psi \), \(\lnot \left[ \overline{p} = \overline{x} \, ; \, p = x \right] \, \varphi (x) = \langle \overline{p} = \overline{x} \, ; \, p = x \rangle \, \lnot \varphi (x)\), \(\lnot \langle \overline{p} = \overline{x} \, ; \, p = x \rangle \, \varphi (x) = \left[ \overline{p} = \overline{x} \, ; \, p = x \right] \, \lnot \varphi (x)\).

  4. http://www.cisco.com/c/en/us/td/docs/ios/12_2/configfun/configuration/guide/ffun_c/fcf007.html.

  5. http://psg.com/lists/netconf/netconf.2004/msg00448.html.

  6. http://github.com/sylvainhalle/MetaConfig. Note that the algorithm currently assumes that the input formula is already in PNF/DNF.

References

  1. Strassner, J.: Bridge to IP Profitability (2002). http://www.intelliden.com/library/GlobalOSS_BridgetoIP45.pdf. Accessed 27 May 2016

  2. Feamster, N., Balakrishnan, H.: Detecting BGP configuration faults with static analysis. In: 2nd Symposium on Networked Systems Design and Implementation (NSDI), (Boston, MA), pp. 43–56 (2005)

  3. Wool, A.: A quantitative study of firewall configuration errors. IEEE Comput. 6, 62–67 (2004)

    Article  Google Scholar 

  4. Burgess, M., Couch, A.: Modeling next generation configuration management tools. In: LISA, pp. 131–147. USENIX (2006)

  5. Hallé, S., Ngoupe, E.L., Nijdam, G., Cherkaoui, O., Valtchev, P., Villemaire, R.: Validmaker: a tool for managing device configurations using logical constraints. In: NOMS [35], pp. 1111–1118

  6. 802.11Q: Virtual bridged local area networks standard (2003). http://standards.ieee.org/getieee802/download/802.1Q-2003.pdf

  7. Configuring VTP (2007). http://www.cisco.com/en/US/products/hw/switches/ps708/products_configuration_guide_chapter09186a008019f048.htm. Accessed 27 May 2016

  8. Villemaire, R., Hallé, S., Cherkaoui, O.: Configuration Logic: a multi-site modal logic. In: TIME, pp. 131–137. IEEE Computer Society (2005)

  9. Delaet, T., Joosen, W.: A language for high-level configuration management. In: 21st Large Installation System Administration Conference, pp. 131–137. Usenix Association (2007)

  10. Fedor, M., Schoffstall, M.L., Davin, J.: An architecture for describing SNMP management frameworks (RFC 1157) (1990)

  11. Enns, R., Bjorklund, M., Schoenwaelder, J., Bierman, A.: Network Configuration Protocol (NETCONF) (RFC 6241) (2011)

  12. Bjorklund, M.: A Data Modeling Language for the Network Configuration Protocol (NETCONF). (RFC 6020) (2010)

  13. Burgess, M.: A site configuration engine. In: USENIX, pp. 309–337 (1995)

  14. Schönwälder, J., Marinov, V., Burgess, M.: Integrating cfengine and scli: managing network devices like host systems. In: IEEE/IFIP Network Operations and Management Symposium: Pervasive Management for Ubioquitous Networks and Services, NOMS (2008) 7–11 April 2008, Salvador, Bahia, Brazil, pp. 1067–1070. IEEE (2008)

  15. SolarWinds CatTools: Cattools Help (2012). http://www.kiwisyslog.com/help/cattools/mnu_filedbimportdevicefrmtab.htm

  16. Puppet Labs investors: (2013). http://puppetlabs.com/solutions/juniper-networks

  17. Taylor, M., Vargo, S.: Learning Chef. O’Reilly, Sebastopol, CA (2014)

    Google Scholar 

  18. Goldsack, P., Guijarro, J., Loughran, S., Coles, A.N., Farrell, A., Lain, A., Murray, P., Toft, P.: The SmartFrog configuration management framework. Oper. Syst. Rev. 43(1), 16–25 (2009)

    Article  Google Scholar 

  19. Lobo, J., Bhatia, R., Naqvi, S.A.: A policy description language. In: Hendler, J., Subramanian, D. (eds.) Proceedings of the Sixteenth National Conference on Artificial Intelligence and Eleventh Conference on Innovative Applications of Artificial Intelligence, July 18–22, 1999, Orlando, FL, USA, pp. 291–298. AAAI Press/The MIT Press (1999)

  20. Agrawal, D., Calo, S.B., Lee, K.-W., Lobo, J.: Issues in designing a policy language for distributed management of IT infrastructures. In: Integrated Network Management, pp. 30–39. IEEE (2007)

  21. Damianou, N., Dulay, N., Lupu, E., Sloman, M.: The Ponder policy specification language. In: Sloman, M., Lobo, J., Lupu, E. (eds.) POLICY, vol. 1995 of Lecture Notes in Computer Science, pp. 18–38. Springer, Berlin (2001)

  22. Object constraint language version 2.2, tech. rep. (2010). http://www.omg.org/spec/OCL/2.2

  23. Hallé, S., Deca, R., Cherkaoui, O., Villemaire, R.: Automated validation of service configuration on network devices. In: Vicente, J.B., Hutchison, D. (eds.) MMNS, vol. 3271 of Lecture Notes in Computer Science, pp. 176–188. Springer, Berlin (2004)

  24. Tuncer, D., Charalambides, M., Pavlou, G., Wang, N.: Dacorm: a coordinated, decentralized and adaptive network resource management scheme. In: 2012 IEEE Network Operations and Management Symposium, Maui, HI, USA, April 16–20, 2012 [35], pp. 417–425

  25. Seitz, L., Selander, G., Rissanen, E., Ling, C., Sadighi, B.: Decentralized access control management for network configuration. J. Netw. Syst. Manag. 16(3), 303–316 (2008)

    Article  Google Scholar 

  26. Burgess, M.: Theory and practice of configuration management in decentralized systems. In: Hellerstein, J.L., Stiller, B. (eds.) Proceedings of the Management of Integrated End-to-End Communications and Services, 10th IEEE/IFIP Network Operations and Management Symposium, NOMS 2006, Vancouver, Canada, April 3–7, 2006, p. 583. IEEE (2006)

  27. Koch, F.L., Westphall, C.B.: Decentralized network management using distributed artificial intelligence. J. Netw. Syst. Manag. 9(4), 375–388 (2001)

    Article  Google Scholar 

  28. Kahani, M., Beadle, P.: Decentralized approaches for network management. Comput. Commun. Rev. 27(3), 36–47 (1997)

    Article  Google Scholar 

  29. Hallé, S., Wenaas, É., Villemaire, R., Cherkaoui, O.: Self-configuration of network devices with Configuration Logic. In: Gaïti, D., Pujolle, G., Al-Shaer, E.S., Calvert, K.L., Dobson, S.A., Leduc, G., Martikainen, O. (eds.) Autonomic Networking, vol. 4195 of Lecture Notes in Computer Science, pp. 36–49. Springer, Berlin (2006)

  30. Agoulmine, N.: Autonomic Network Management Principles. Academic Press, London (2011)

    Google Scholar 

  31. Henderson, P., Morris, J., Jr.: A lazy evaluator. In: Proceedings of the 3rd ACM SIGACT-SIGPLAN Symposium on Principles on Programming Languages, pp. 95–103. ACM (1976)

  32. Friedman, D.P., Wise, D.S.: CONS should not evaluate its arguments. In: ICALP, pp. 257–284 (1976)

  33. Hallé, S., Cherkaoui, O., Valtchev, P.: Towards a semantic virtualization of configurations. In: 2012 IEEE Network Operations and Management Symposium, Maui, HI, USA, April 16–20, pp. 1268–1271. IEEE (2012)

  34. Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Springer, Berlin (1997)

    MATH  Google Scholar 

Download references

Acknowledgments

The authors would like to acknowledge the work of Éric Wenaas on an early version of ValidMaker. The authors acknowledge the financial support of the Natural Sciences and Engineering Research Council of Canada and Ericsson Canada.

Author information

Authors and Affiliations

  1. Laboratoire d’informatique formelle, Université du Québec à Chicoutimi, Saguenay, Canada

    Éric Lunaud Ngoupé & Sylvain Hallé

  2. Télécom Nancy, Nancy, France

    Clément Parisot & Sylvan Stoesel

  3. Laboratoire de téléinformatique et réseaux, Université du Québec à Montréal, Montreal, Canada

    Petko Valtchev, Roger Villemaire & Omar Cherkaoui

  4. Ericsson Canada, Montreal, Canada

    Pierre Boucher

Authors
  1. Éric Lunaud Ngoupé
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Clément Parisot
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sylvan Stoesel
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Petko Valtchev
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Roger Villemaire
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Omar Cherkaoui
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Pierre Boucher
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Sylvain Hallé
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sylvain Hallé.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Ngoupé, É.L., Parisot, C., Stoesel, S. et al. A Declarative Approach to Network Device Configuration Correctness. J Netw Syst Manage 25, 180–209 (2017). https://doi.org/10.1007/s10922-016-9387-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10922-016-9387-7

Keywords

Search

Navigation