Subject: Re: [manet] Loops & Specification

From: [email-masked] (rvg)
Date: Thu, 11 Feb 2016 12:09:11 +1100

Dear MANET 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

Thanks. As co-author of that publication [1], I'm happy to clarify it further.

What it shows, is that an entirely plausible interpretation of the AODV
RFC, fully taking into account all mandates stipulated therein, admits
routing loops.

It also shows that the loops we found can occur in several open-source
implementations of AODV.

In a companion publication [2], we formally prove that under a different
plausible interpretation the protocol is loop free (not counting
possible loops due to timing issues).

As Charlie already indicated, our findings are the result of
ambiguities in the RFC. In fact, in [3] (and summarised in [1]) we
carefully examine a long list of ambiguities, contradictions and cases
of underspecification in the RFC, analysing in each case the arguments
for and against a particular reading.  (This is quite different from
implementation bugs, which can obviously also cause loops.)
Combinatorially, this gave rise to more than 5000 possible
interpretations of the RFC, any we classify which ones lead to loops
and which ones don't.

The take home message of this is not that AODV is a bad protocol.
It is also not that the RFC is badly written.
In fact I think that, as standards documents go, it is written rather well.

Our point is that the methodology of writing protocol specifications
in English prose only, unavoidably gives rise to these levels of ambiguity.
In our view, each protocol specification should consist of a
formalisation in an adequate specification formalism, accompanied by
an explanation in English. The choice of a specification formalism is
secondary - as long as it eliminates all ambiguity.

This message of course pertains to the development of AODVv2 just as well.

In our publications we show that formal methods have advanced to such a
state that they are now able to capture the full syntax and the full
semantics of network protocols.

> 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.

Our loops are related to intermediate route reply. As this tricky
(although useful) feature has been removed from the draft of AODVv2
(last time I checked; I'm not a regular reader of this list), that
problem does not apply any longer. As Charlie mentioned, other
shortcomings of the RFC that contributed to the loops we demonstrated
have been adequately addressed in AODVv2 as well.

Of course, by itself this does not guarantee that AODVv2 is loop free.
That requires formal proof, which is only possible on the basis of a
formalised specification (resolving all remaining ambiguities).

With best regards,
Rob van Glabbeek

[1] Sequence Numbers Do Not Guarantee Loop Freedom; AODV Can Yield Routing Loops
    http://theory.stanford.edu/~rvg/abstracts.html#100
    MSWiM 2013
[2] A Rigorous Analysis of AODV and its Variants
    http://theory.stanford.edu/~rvg/abstracts.html#97
    MSWiM 2012.
[3] A Process Algebra for Wireless Mesh Networks used for Modelling,
    Verifying and Analysing AODV
    http://theory.stanford.edu/~rvg/abstracts.html#102
    Technical Report 5513, NICTA, 2013.

---

From: "A .Riley Eller" <[email-masked]>
Date: Wed, 10 Feb 2016 17:49:40 -0800

> secondary - as long as it eliminates all ambiguity.

Good work.

This result further confirms the research done by Meredith Paterson et
al (langsec.org) and their denunciation of prosaic parser
specifications.

Further evidence of this exact problem can be found in various patches
submitted to correct loop-admission errors in the Linux kernel's IEEE
802.11(s) implementation. They result from similar ambiguities.

It's time to change the protocol specification process.

Riley Eller
coco communications

---

From: Charlie Perkins <[email-masked]>
Date: Wed, 10 Feb 2016 18:46:33 -0800

Hello Rob,

Thanks for your response!

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.

My experience with formal analytical tools has been positive.  We 
collaborated with a group from University of Pennsylvania after they 
uncovered an error in an early version of AODV that could arise if 
certain information were not purged during reboot.

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 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.  Improper or 
erroneous use obviously can eliminate that safeguard.  It would have 
been better for the title to emphasize that specification ambiguities 
(or programming errors) can neutralize the safeguards, instead of giving 
the impression that the mathematical proof is suspect.

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.

Regards,
Charlie P.

On 2/10/2016 5:09 PM, rvg wrote:
> _______________________________________________
> manet mailing list
> [email-masked]
> https://www.ietf.org/mailman/listinfo/manet
>