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.
Chapter PDF
Similar content being viewed by others
Keywords
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
Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538–576 (2002)
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)
Chandy, K., Misra, J.: Proofs of networks of processes. IEEE Transactions on Software Engineering 7(4) (1981)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988)
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)
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)
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)
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)
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)
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)
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)
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)
Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19(5), 279–285 (1976)
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
Pnueli, A.: The temporal logic of programs. In: FOCS (1977)
Pnueli, A.: In transition from global to modular reasoning about programs. In: Logics and Models of Concurrent Systems. NATO ASI Series (1985)
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)
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)
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
Namjoshi, K.S., Trefler, R.J. (2015). Loop Freedom in AODVv2. In: Graf, S., Viswanathan, M. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2015. Lecture Notes in Computer Science(), vol 9039. Springer, Cham. https://doi.org/10.1007/978-3-319-19195-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-19195-9_7
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19194-2
Online ISBN: 978-3-319-19195-9
eBook Packages: Computer ScienceComputer Science (R0)