Subject: Re: [manet] Loops & Specification

From: Charlie Perkins <[email-masked]>
Date: Tue, 9 Feb 2016 21:25:20 -0800

Hello folks,

I read with some interest the paper claiming that sequence numbers do 
not guarantee loop freedom:

>
> http://www.cse.unsw.edu.au/~rvg/pub/AODVloop.pdf 
> <http://www.cse.unsw.edu.au/%7Ervg/pub/AODVloop.pdf>

It turns out that sequence numbers do guarantee loop freedom after all, 
contrary to the title of the paper.  But it is possible to put bugs in 
various places that violate the hypotheses of the proof of loop 
freedom.  Getting inconsistent results due to bugs is not shocking news.

Since the claimed loop condition pertains to RFC 3561, I should not dive 
into the details about that.  I did check whether there is any impact on 
AODVv2, and the answer is that it does NOT have any impact.

 1. Section 4.4 of AODVv2 clearly forbids storing a stale sequence
    number in a "self-entry" such as described in the paper
 2. Section 7.4.2 of AODVv2 clearly forbids the erroneous interpretation
    leading to faulty handling of RERR as described in the paper
 3. I have reviewed RFC 3561 as part of reading their email, and I
    believe that some of the interpretations made by the authors are due
    to possible ambiguities in RFC 3561, combined with interpretations
    that ignore mandates in RFC 3561, intertwined with some confusion
    about the ways that a router should keep routes to itself.  More
    information about the discussion related to RFC 3561 is not germane
    to AODVv2, but available upon request.

Regards,
Charlie P.

---

From: [email-masked] (rvg)
Date: Thu, 11 Feb 2016 16:55:14 +1100

Hi Charlie,

> It would be much appreciated if we could get a formal analysis of 
> AODVv2, and please let me know if there is anything I can do to help.

We have already applied our experience in modelling (RFC-) AODV
to an earlier version of AODVv2 (Internet-Draft 22, March 12, 2012).
See [4] below.
   A small problem for us, however, is that the AODVv2 is a quickly
moving target. A formal analysis takes some time, and by the time it
is ready, the proposed new standard has already moved on, so that the
work is no longer fully applicable.
   I would be interested to work (or put a student on) transferring our
study to the current AODVv2, specially when you think there is a
version that is somewhat stable. Our (perhaps far-fetched) ideal would
be that formal specifications (of which a small snippet is shown at
the top of page 3 of [4], for instance) can be read by the people that
make proposals on how to further change the AODVv2 spec., so that a
proposal could have the form
	 "change line 13 of Process 4 into  [ ip = dip ]".

> There is a specification for intermediate route reply which should 
> rightfully be considered part of AODVv2, but was separated out in 
> accordance with a request during some very unfortunate earlier times.  
> It belongs as part of the protocol because it can reduce the number of 
> network-wide broadcasts, and that is a very desirable goal.  Flooding is 
> very expensive and is the main reason that manet routing protocols 
> produce congestion.

I agree with that, even though one has to be very careful with
intermediate route reply. Is that separated proposal relatively stable
by now? (And where do I find it? Sorry for now being up to date in
this regard.)

> I still think that the title of the paper is unfortunate, because it 
> wrongly places the blame for routing loops.  Sequence numbers do 
> definitely prevent routing loops if used properly. 

What we wanted to say is that the "used properly" cannot be taken for
granted (as we felt it too easily was). I hope the abstract and
conclusion of the paper do make that clear.  Although the
formal-methods community likes our work, it is hard to get traction in
the networks community; the choice of a rather controversial paper
title did help in this regard (eventually) :^)

> Finally, while you are undoubtedly correct that English prose is 
> vulnerable to misinterpretation and ambiguity, on the whole I think it 
> is clear that we have enough experience to avoid most such problems.  
> For instance, we have a pretty large Internet based on such 
> specifications, and overall it seems to work except for a well-known 
> list of problems (e.g., security) arising from initial design 
> decisions.  If we have automatic programming systems, then a purely 
> formal specification will be very useful.  Imparting knowledge to 
> real-life programmers seems to be a lot more effective using a natural 
> language.

I agree that for widely used internet protocols people appear to have
reached consensus on how to read the specifications. However, for
thinks like AODV this is only partially the case. I for instance
don't believe that AODV routers from different vendors could work
together very well, because they are based on subtly different readings
on the workings of the protocol.

Cheers,
Rob

[4] Peter Höfner and Sarah Edenhofer
    Towards a rigorous analysis of AODVv2 (DYMO)
    2nd International Workshop on Rigorous Protocol Engineering
    (WRiPE 2012), pp. 1-6, Austin, Texas, October, 2012
    http://nicta.com.au/pub?id=6169