Advertisement

Abstract

The AODV protocol is used to establish routes in a mobile, ad-hoc network (MANET). The protocol must operate in an adversarial environment where network connections and nodes can be added or removed at any point. While the ability to establish routes is best-effort under these conditions, the protocol is required to ensure that no routing loops are ever formed. AODVv2 is currently under development at the IETF, we focus attention on version 04. We detail two scenarios that show how routing loops may form in AODVv2 routing tables. The second scenario demonstrates a problem with the route table update performed on a Broken route entry. Our solution to this problem has been incorporated by the protocol designers into AODVv2, version 05. With the fix in place, we present an inductive and compositional proof showing that the corrected core protocol is loop-free for all valid configurations.

Keywords

Target Node Actual Protocol Mobile Router Route Entry Route Table 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538–576 (2002)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Bouajjani, A., Jurski, Y., Sighireanu, M.: A generic framework for reasoning about dynamic networks of infinite-state processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 690–705. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Chandy, K., Misra, J.: Proofs of networks of processes. IEEE Transactions on Software Engineering 7(4) (1981)Google Scholar
  4. 4.
    Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988)Google Scholar
  5. 5.
    Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 19–32. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS. LIPIcs, vol. 18, pp. 289–300. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  7. 7.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of safety properties in ad hoc network protocols. In: PACO. EPTCS, vol. 60, pp. 56–65 (2011)Google Scholar
  8. 8.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of ad hoc networks with node and communication failures. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE 2012. LNCS, vol. 7273, pp. 235–250. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  9. 9.
    Edenhofer, S., Höfner, P.: Towards a rigorous analysis of AODVv2 (DYMO). In: 20th IEEE International Conference on Network Protocols, ICNP 2012, Austin, TX, USA, October 30-November 2, pp. 1–6. IEEE (2012)Google Scholar
  10. 10.
    Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 173–187. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  11. 11.
    Höfner, P., van Glabbeek, R.J., Tan, W.L., Portmann, M., McIver, A., Fehnker, A.: A rigorous analysis of AODV and its variants. In: MSWiM, pp. 203–212. ACM (2012)Google Scholar
  12. 12.
    Namjoshi, K.S., Trefler, R.J.: Analysis of dynamic process networks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 164–178. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  13. 13.
    Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19(5), 279–285 (1976)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Perkins, C., Ratliff, S., Dowdell, J.: IETF MANET WG Internet Draft (December 2014), http://datatracker.ietf.org/doc/draft-ietf-manet-aodvv2, current revision 06
  15. 15.
    Pnueli, A.: The temporal logic of programs. In: FOCS (1977)Google Scholar
  16. 16.
    Pnueli, A.: In transition from global to modular reasoning about programs. In: Logics and Models of Concurrent Systems. NATO ASI Series (1985)Google Scholar
  17. 17.
    Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 18–32. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  18. 18.
    van Glabbeek, R.J., Höfner, P., Tan, W.L., Portmann, M.: Sequence numbers do not guarantee loop freedom – AODV can yield routing loops –. In: MSWiM, 10 pages. ACM (2013)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2015

Authors and Affiliations

  1. 1.Bell LaboratoriesAlcatel-LucentNew yorkUSA
  2. 2.University of WaterlooWaterlooCanada

Personalised recommendations