Subject: Potential Routing loops in AODV

From: "Charles E. Perkins" <[email-masked]>
Date: Wed, 22 Dec 1999 13:25:58 -0800

Hello and Happy Holidays,

I forward to the list the following e-mail I received from
Carl Gunter.  The work of several people is involved in producing
these results, and they are credited within the body of the
forwarded note.  I have only made a few formatting changes.

I think these results indicate the importance of having such
tools as MURPHI, SPIN, and HOL available for testing the
correctness of manet protocols.

In later messages, one or more of the AODV authors will respond to
the points made in the following note.  It is our intention to produce
a revised draft before the next IETF meeting that includes solutions
to the problems that have been identified.

Regards,
Charlie P.

-------- Original Message --------

Date: Mon, 20 Dec 1999 18:06:37 -0500
From: "Carl A. Gunter" <[email-masked]>
Organization: University of Pennsylvania
To: "Charles E. Perkins" <[email-masked]>
CC: David Dill <[email-masked]>,
        Madanlal Musuvathi <[email-masked]>,
        "Samir R. Das" <[email-masked]>,
        Elizabeth Royer <[email-masked]>,
        "Obradovic, Davor" <[email-masked]>,
        "Bhargavan, Karthikeyan" <[email-masked]>,
        [email-masked]
Subject: Re: Potential Routing loops in AODV

Charles:

I'm appending a little write-up of what we know about routing loops for
AODV, including some suggestions for restrictions to include in the
standard.  I'm cc'ing to the folks whose work gets mentioned, including
some of the Monarch folks who pointed out issues to us.  Hope this
helps.

Cheers, Carl Gunter
http://www.cis.upenn.edu/~gunter

========================================================================

                                          Karthikeyan Bhargavan
                                          Davor Obradovic
                                          Carl Gunter
                                          University of Pennsylvania.   
Dec 20, 1999

             Analyzing the Occurrence of Loops in AODV
             =========================================

This note is a summary and confirmation of loops in AODV found by
Joshua Broch and Dave Maltz (CMU), Madanlal Musuvathi (Stanford), and 
Karthikeyan Bhargavan, Davor Obradovic and Carl Gunter (Penn).

We first describe the various conditions in which AODV nodes form loops
in a simple 3-node network. We then outline a general theorem of
loop-freedom under some restrictions of the protocol. Finally, we
analyze timeout behavior and specify timer values that would allow
us to relax some of the restrictions in the general proof. Some of
the results in this note have been presented in [4].

Tools:
=====
       The following tools were used to arrive at the proofs described 
       in this note
       
           (1) Murphi (Stanford) - a model-checker from Stanford [1]
           (2) Spin (Penn) - a model-checker from Bell Labs [2]
           (3) HOL (Penn) - a theorem prover [3]
       
       Researchers in the CMU group have been using manual analysis
combined
       with statistical analysis through NS/2 - a network protocol
simulator.

AODV Loops
==========

        Consider the following simple network of 3 nodes

                        A ----- B ----- D          

         - We run AODV processes at all 3 nodes.
         - D is the only destination. 
         - Both A and B need to send data to D.
         - The link B --- D is fragile and may be broken at any time.

        The network and the processes are modeled in Spin, and we try to
        verify that there will never be a loop between A and B.         
        We find that in the following scenarios {S1-S4} a loop will
        be formed between A and B:

         Let A and B have active routes to D to begin with: 

                              A ----> B ----> D
        
         S1. When the link B---D goes down, B generates a RERR.
             If B does not increment its seqno for D 
             (the current standard does not require B to do so), 
             and if the RERR gets dropped, there will be a loop.
             This bug is due to Madanlal Musuvathi, and was found by
             Murphi.  We have confirmed the loop in Spin.          
             
         S2. When the link B---D goes down, B generates a RERR.
             Suppose B DOES increment its seqno for D.  If the RERR
             gets dropped, and B deletes its route before A's route
             expires, there will be a loop.  This bug is due to Joshua
             Broch and Dave Maltz and was found by manual inspection.

             This loop is also discovered by Spin and Murphi.

         S3. Suppose B's route expires while A is still pointing at it.
             The standard does not explicitly say what happens when a
             route expires.  Consider the following possibilities:

                      (a) B deletes the route on expiry:
                            There will be a loop.
                      (b) B keeps the route around, unchanged,
                          as an expired route:
                            There will be a loop. (similar to S1)
                      (c) B keeps the route around as an expired route,
                          it increments the route's seqno,
                          and never deletes it:
                            Spin could not find a loop.
                      (d) B keeps the route around as an expired route,
                          it increments the route's seqno for D,
                          and deletes it after some time:
                            There will be a loop. (similar to S2)

         S4. The AODV process at B is restarted suddenly (reboot, crash,
             etc.) If A does not detect the restart as a link-breakage, 
             and continues to point to B, there will be a loop.

             Here, we assume that B restarts in a vanilla state, 
             so this case could be treated as one in which all routes 
             at B are suddenly deleted. 
             This scenario has been discussed in [4].

General Result
==============

        All the results in the previous section were for the 3-node
        network.  In this section we present a result for AODV's
        loop-freedom under some strict assumptions:

        Assume that
        ===========
        
            A1. When a node discovers that its next-hop to a dest is 
                unavailable or it receives an RERR for the dest from its 
                next-hop, it increments the seqno for the route 
                (and may send out an RERR).     
            A2. When a node discovers that its route to a dest has
                expired, it increments the seqno for the route.
            A3. Nodes NEVER delete routes.    
            A4. Nodes ALWAYS detect when a neighbor restarts its AODV
                process.  The restart is treated as if all links to
                the neighbor have broken. 

        Theorem:
        =======
                Consider an arbitrary network of nodes running AODV.
                If all nodes conform to the assumptions A1-A4, 
                there will be no loops formed.     
        
        We have proved a similar result for AODVv2 in [4], using a 
        combination of Spin and HOL. In that proof, we ignored the 
        timing behaviour of routes (routes never expire), and route
        errors are signaled by triggered RREPs (as descibed in
        AODVv2).    Consequently, we just used assumptions A3, A4 above.
        However, we believe that the proof can be extended for AODVv4,
        under the above assumptions.

        Of these assumptions, A1 (due to Musuvathi) avoids scenario S1. 
        A2 avoids looping scenario S3(b). 
        A3 avoids the scenarios S2, S3(a,d). 
        Finally, the A4 avoids the scenario S4. 

Timing Considerations
=====================

        The four "safe" assumptions made in the previous section will 
        avoid routing loops. Of the four assumptions, we consider A1 and
        A2 to be necessary. However, A3 may not be practical in a
        dynamic network where a node is likely to see lots of nodes for
        short periods of time.  Also, it is not clear how one would
        implement restart-detection as in A4.

        Now consider the looping scenarios S2, S3(a,d) and S4 described
        in the "AODV Loops" section. In all these cases, the loops get
        formed because A was pointing to B when B's route was deleted. 
        This is exactly the case that we need to avoid. That is, we need 
        to add assumptions that would prove the desired property:

        Proposition:
        ===========
                Consider any two nodes: A and B, looking for routes to
D. 
                When B deletes its route to D, A should not be pointing
                to B.

        Note that, if B deletes its route to D, when A is still pointing
        at it, then the lifetime of A's route had to be greater than the 
        lifetime of B's route (except in S4). This leads us to analyze
        the restrictions on route lifetime values that would make the
        proposition true. Such restrictions would allow us to ease
        assumption A3. 

        We model the processes again in Spin.
        This time we try to prove that 
                  if A points to B, 
                  and B has no route to D, then 
                       A's lifetime must ALWAYS be less than B's
lifetime.

        Spin provides a counter-example - 
                  If A keeps sending data packets to B 
                  which are either
                        (i) dropped by the network, or
                        (ii) ignored by B,    
                  then A's lifetime keeps getting updated to
                  ACTIVE_ROUTE_TIMEOUT, while B's lifetime decreases to
0.
                  Eventually, A's lifetime is non-zero while B's route 
                  has expired. This situation can easily lead to a loop.

        (i) and (ii) prompt us to propose the following:

                  (a) There must be some assumption about the
reliability
                      of data transmission. Otherwise, B has no way of
                      knowing if A is still pointing at it.
                  (b) If B receives a data pkt for D but has no route to
D,
                      it must take some action. In particular, it must 
                      either attempt to find a route to D or send an
                      RERR back to A.        

                      The standard does not explicitly state what a 
                      forwarding node must do when it does not have a   
                      route to the destination. We are stipulating that
                      it must do something, not just ignore the packet.

        There clearly are other possible solutions to this:

                  - Encode some reliability explicitly into the
protocol.
                    This would ensure that some of the data packets get
                    through.

                  - Make B aggressively broadcast RERR's with some 
                    reliability, so that A gets to know that B has lost
                    its route.

        If we consider (a) and (b), we can propose timeout constraints
        that enforce loop-freedom for AODV, even in the presence of
        route deletion. The idea is that B MUST keep its route as long
        as it is unsure if someone (A) is pointing at it. In particular,
        we want B to maintain its seqno for D as long as there is a
        possibility of a loop. 

        When it has waited for a long enough period, without receiving 
        any packets for D, it may safely delete the route. 
        Let us call this waiting period the DELETE_PERIOD. 
        We can characterize it using an assumed reliability of the 
        underlying layer. It is defined in the next section.

        Finally, we need to worry about S4. In this case, B's routes
        have already been deleted. If A does not detect the restart as a 
        link-breakage by some external mechanism, we shall need to make
        sure that B does not make requests that will be answered by A.
        One way to ensure this is to make B sleep till it does not
receive
        any packet for DELETE_PERIOD. This would ensure that when B does
        make its request, no-one is pointing at it. We may choose to be
        more aggressive by sending RERR's to A if B does receive a
        message.

        The remedies we propose avoid loops in the 3-node network we
        described.  We believe that they may be sufficient to ensure
        loop freedom in a general case, but we are still in the
        process of developing a formal proof of that.

Remedies for the Standard
=========================

        To avoid looping conditions in AODV, we propose that the
        standard must incorporate the following:

         1. Route errors must cause the seqno for the route to be
            incremented
         
         2. The standard must specify what happens when active routes
            expire.  We propose that they must be kept in the routing
            table for at least DELETE_PERIOD time, and that their
            seqno's must be incremented. (Look under 5. below for
            specification of DELETE_PERIOD)
                
         3. The standard must specify what happens when B receives 
            packets from A to D, and B does not have an active route
            to D.  We propose that B should then request for a route
            to D.  B may alternatively send an route error (RERR) to A.
            (Essentially, B cannot ignore the packet)

         4. The standard must make an assumption about the reliability
            of data transfer. In particular, it cannot be the case that
            A thinks it has a link to B, but all the packets from A to
            B get dropped. This assumption is necessary because the
            mechanism for detecting link-breakage is external to AODV.

            We propose that the standard assume that K out of N packets 
            get through (for some choice of K and N).

         5. Suppose

                MAX_LIFETIME = max(ACTIVE_ROUTE_TIMEOUT, 
                                   REV_ROUTE_LIFE, 
                                   MY_ROUTE_TIMEOUT(at destination D))
                           
                               (This is a measure of A's active
                                lifetime, i.e. the time A's route
                                can live without being used) 
 
                DELETE_PERIOD = N/K * MAX_LIFETIME
                           
                               (Period in which B is guaranteed by 4
                                above to get a data packet from A,
                                if A still has a route through B)
           
            Then
                (a) When a route error is discovered, a node should set
                    the hop-count to infinity, increment seqno, and set
                    the lifetime to DELETE_PERIOD (Ensures A1, Avoids
S1)
                        
                (b) When an *active* route expires, a node should set  
                    hop-count to infinity, increment seqno, and set the
                    lifetime to DELETE_PERIOD (Ensures A2 along with
(c),
                    Avoids S2,S3)
                
                (c) When a node receives a data packet for forwarding to
                    a dest, but it has an INFINITE hop-count for dest,
                    it should reset the lifetime to DELETE_PERIOD
                    (Avoids S2,S3 along with (b))    
                        
                (d) When the lifetime of a route expires when its
                    hop-count is infinity (i.e. after DELETE_PERIOD), 
                    the route may safely be deleted.    

            Note, that MAX_LIFETIME is really just ACTIVE_ROUTE_TIMEOUT,
            and DELETE_PERIOD is just BAD_LINK_LIFETIME. We are just
            placing strong constraints on their relationship with each
            other and with the other timing constants. In other words,
            one set of constraints implied by the above could be:
                     ACTIVE_ROUTE_TIMEOUT >= REV_ROUTE_LIFE
                     ACTIVE_ROUTE_TIMEOUT >= MY_ROUTE_TIMEOUT
                     BAD_LINK_LIFETIME >= N/K * ACTIVE_ROUTE_TIMEOUT

        6. The standard must specify what a node must do when the 
           AODV process restarts. In particular, it must take care of
           the case that other nodes may be pointing at it and may not
           have detected its absence yet. We propose that:
                     
                (a) When an AODV process restarts, it should go to sleep
                    for DELETE_PERIOD before making its presence felt in
                    any way.  This can be done by setting a sleep-timer
                    to DELETE_PERIOD.  (Avoids S4 along with(b))

                (b) If an AODV process receives a data packet when it is 
                    sleeping, it resets the sleep-timer to
DELETE_PERIOD.
                    It may broadcast a RERR packet for the destination
                    of the data packet. Anything other than a data
packet
                    is ignored.  (Avoids S4 along with (a))
                    
         7. If the reliability of the underlying layer cannot be
            accurately estimated, then
                 (a) Nodes should NEVER delete routes.
                 
                 (b) When a node restarts, 

                     (i) it should broadcast a RERR packet for every 
                         destination, reliably, or
                    (ii) it should wait for 
                            ALLOWED_HELLO_LOSS*HELLO_INTERVAL 
                         before starting any contact with the network.
                         This works if all nodes are using the HELLO
                         protocol to detect links, or
                   (iii) it should send a special RERR pkt to signal
                         that it has just restarted   

                     If none of (i)-(iii) (or any other alternatives)
                     can guarantee that the node's neighbors MUST
                     become aware of its absence, then loop-freedom
                     cannot be guaranteed.
         
References
==========

[1] Murphi home page, http://sprout.stanford.edu/dill/murphi.html
[2] Spin home page,
    http://netlib.bell-labs.com/netlib/spin/whatispin.html
[3] HOL home page, http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html
[4] Formal Verification of Standards for Distance Vector Routing, 
    Karthikeyan Bhargavan, Davor Obradovic and Carl Gunter, 
    available at http://www.cis.upenn.edu/~gunter/hol/papers/rip.ps