Modeling and analyzing the convergence property of the BGP routing protocol in SPIN

详细信息    查看全文

• 作者：Zhe Chen (1)
  Daqiang Zhang (2)
  Yinxue Ma (1)
  
  1. Software Verification Lab ; College of Computer Science and Technology ; Nanjing University of Aeronautics and Astronautics ; 29 Yudao Street ; Nanjing ; 210016 ; Jiangsu ; China
  2. School of Software Engineering ; Tongji University ; Shanghai ; 201804 ; China
  
• 关键词：BGP ; Routing protocol ; Convergence property ; Model checking ; Formal verification ; SPIN
• 刊名：Telecommunication Systems
• 出版年：2015
• 出版时间：March 2015
• 年：2015
• 卷：58
• 期：3
• 页码：205-217
• 全文大小：477 KB
• 参考文献：1. Abbas, C. J. B., Gonz谩lez, R., Cardenas, N., & Garc铆a-Villalba, L. J. (2008). A proposal of a wireless sensor network routing protocol. / Telecommunication Systems, / 38(1鈥?), 61鈥?8. CrossRef
  2. Baier, C., & Katoen, J. P. (2008). / Principles of model checking. Cambridge, MA: MIT Press.
  3. Ben-Ari, M. (2008). / Principles of the SPIN model checker. Berlin: Springer.
  4. Chen, Y. S., Liao, Y. J., Lin, Y. W., & Chiu, G. M. (2009). Hve-mobicast: A hierarchical-variant-egg-based mobicast routing protocol for wireless sensornets. / Telecommunication Systems, / 41(2), 121鈥?40. CrossRef
  5. Chen, Y. S., Lin, Y. W., & Pan, C. Y. (2011). Dir: Diagonal-intersection-based routing protocol for vehicular ad hoc networks. / Telecommunication Systems, / 46(4), 299鈥?16. CrossRef
  6. Chen, Z., Motet, G. (2010). Nevertrace claims for model checking. In / Proceedings of the 17th International SPIN Workshop on Model Checking of Software (SPIN 2010), Lecture Notes in Computer Science, (vol. 6349, pp. 162鈥?79). Berlin: Springer.
  7. Clarke, E. M., Grumberg, O., & Peled, D. A. (2000). / Model Checking. Cambridge, MA: MIT Press.
  8. Courcoubetis, C., Vardi, M. Y., Wolper, P., & Yannakakis, M. (1992). Memory-efficient algorithms for the verification of temporal properties. / Formal Methods in System Design, / 1(2/3), 275鈥?88. CrossRef
  9. Gastin, P., Oddoux, D. (2001). Fast LTL to B眉chi automata translation. In / Proceedings of the 13th International Conference on Computer Aided Verification (CAV鈥?1), Lecture Notes in Computer Science, (vol. 2102, pp. 53鈥?5). Berlin: Springer.
  10. Gerth, R., Peled, D., Vardi, M. Y., & Wolper, P. (1995). Simple on-the-fly automatic verification of linear temporal logic. In P. Dembinski & M. Sredniawa (Eds.), / Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification (pp. 3鈥?8). London: Chapman & Hall.
  11. Griffin, T., Shepherd, F. B., & Wilfong, G. T. (2002). The stable paths problem and interdomain routing. / IEEE/ACM Transactions on Networking (TON), / 10(2), 232鈥?43. CrossRef
  12. Griffin, T., & Wilfong, G.T. (1999). An analysis of bgp convergence properties. In / Proceedings of the ACM SIGCOMM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication (SIGCOMM 1999), pp. 277鈥?88.
  13. Herrmann, P., Krumm, H., Dr枚gehorn, O., & Geisselhardt, W. (2002). Framework and tool support for formal verification of highspeed transfer protocol designs. / Telecommunication Systems, / 20(3鈥?), 291鈥?10. CrossRef
  14. Holzmann, G. J. (1997). The model checker SPIN. / IEEE Transactions on Software Engineering, / 23(5), 279鈥?95. CrossRef
  15. Holzmann, G. J. (1998). An analysis of bitstate hashing. / Formal Methods in System Design, / 13(3), 289鈥?07. CrossRef
  16. Holzmann, G. J. (2003). / The SPIN model checker: Primer and reference manual. Boston, MA: Addison-Wesley.
  17. Huadmai, C. (2011). Verification of routing policies by using model checking technique. In / Proceedings of the IEEE 6th International Conference on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications (IDAACS 2011), (vol. 2, pp. 711鈥?16). IEEE.
  18. Huth, M., & Ryan, M. (2004). / Logic in Computer science: Modelling and reasoning about systems (2nd ed.). Cambridge: Cambridge University Press. CrossRef
  19. Kettaf, N., Abouaissa, A., Duong, T. V., & Lorenz, P. (2006). An efficient QoS routing algorithm for solving MCP in ad hoc networks. / Telecommunication Systems, / 33(1鈥?), 255鈥?67. CrossRef
  20. Myers, G. J. (1979). / The art of software testing. Hoboken, NJ: Wiley.
  21. Rekhter, Y., & Li, T. (1995). A Border Gateway Protocol 4 (BGP-4), RFC 1771. IETF.
  22. Rekhter, Y., & Li, T. (2006). A Border Gateway Protocol 4 (BGP-4), RFC 4271. IETF.
  23. Secci, S., Rougier, J. L., Pattavina, A., Patrone, F., & Maier, G. (2011). Multi-exit discriminator game for BGP routing coordination. / Telecommunication Systems, / 48(1鈥?), 77鈥?2. CrossRef
  24. Wang, A., Talcott, C. L., Jia, L., Loo, B. T., & Scedrov, A. (2011). Analyzing bgp instances in maude. In R. Bruni & J. Dingel (Eds.), / Proceedings of the 31st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE 2011), Lecture Notes in Computer Science (vol. 6722, pp. 334鈥?48). Berlin: Springer.
  
• 刊物类别：Business and Economics
• 刊物主题：Economics
  Business Information Systems
  Computer Communication Networks
  Artificial Intelligence and Robotics
  Probability Theory and Stochastic Processes
  
• 出版者：Springer Netherlands
• ISSN：1572-9451

文摘

The Border Gateway Protocol (BGP) is an interdomain routing protocol such that each autonomous system can independently formulate its routing policies. However, BGP does not always converge, because its routing policies may conflict and cause BGP to diverge, and result in persistent route oscillations. In this paper, we present an automated tool for verifying the convergence property of BGP by using the SPIN model checker. We have developed a SPIN library specifying a path vector protocol with a set of unspecified routing policies, and methods to instantiate the library to a specific BGP instance. The user only needs to provide models of network topology and customized routing policies, then SPIN can simulate the executions of the BGP instance, as well as automatically verify the protocol by exhaustively exploring all possible executions to detect possible divergences. The effectiveness of our library is demonstrated by experiments and verification results.