Charlie,
Thank you, sir! I believe that effectively crosses an item off of Justin's
list. I'm also pretty happy to read
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.
Regards,
Stan
On Fri, Feb 19, 2016 at 3:53 PM, Charlie Perkins <
charles.perkins@xxxxxxxxxxxxx> wrote:
Hello folks,
As requested, here is the email from Rob van Glabeek. It contains the
following passage:
As Charlie mentioned, other
shortcomings of the RFC that contributed to the loops we demonstrated
have been adequately addressed in AODVv2 as well.
In subsequent email, there was some follow-on discussion about whether or
not
English could be reasonably used as a specification language and some
other details.
Regards,
Charlie P.
-------- Forwarded Message --------
Subject: Re: [manet] Loops & Specification
Date: Thu, 11 Feb 2016 12:09:11 +1100
From: rvg <rvg@xxxxxxxxxxxxxxx> <rvg@xxxxxxxxxxxxxxx>
To: manet@xxxxxxxx
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.
_______________________________________________
manet mailing listmanet@ietf.orghttps://www.ietf.org/mailman/listinfo/manet
