nanog mailing list archives

Re: update


From: Merike Kaeo <merike () doubleshotsecurity com>
Date: Mon, 29 Sep 2014 11:06:47 -0700

Heh….this reminded me of a project I had to do circa 1991/2 when getting my Master's in EE where we used this book and 
mechanism to
'validate' TCP.  http://spinroot.com/gerard/popd.html

Although as a student homework assignment I wouldn't say what we did was in any way rigorous but certainly had me 
learning some interesting
concepts (and as I was actually creating a backbone with routers at the time it was kind of fun to see where academics 
and operations went a bit
orthogonal) :)  And no, I can't for the life of me remember that far back except to remember that I was the only one in 
class with practical knowledge.

And then of course there's the 'how did one actually implement the protocols' and hence the Interop conferences as 
someone already mentioned.
Even a formal proof of 'protocol validation and correctness' doesn't alter the implementation creativities…

- merike


On Sep 28, 2014, at 11:41 PM, George Michaelson <ggm () algebras org> wrote:

for two asynchronous, otherwise unconnected systems, using TCP/IP there is
a state transition sequence which can be shown to work if you stick to it.
There are also (I believe) corner cases when you send unexpected sequences,
and some of them have known behaviours

in that sense, the question: "does the RFC adequately document the state
transition sequences which are understood to be valid states and
transitions" is a well formed question.

Robin Milner, in his calculus of communicating systems tried to codify a
formal mathematics of async communicating systems. I don't know if anyone
either extended the idea(s) or applied it to TCP/IP.

Certainly I believe there are formally verified protocols. Thats a space
Erlang occupies isn't it?

On Mon, Sep 29, 2014 at 4:14 PM, Larry Sheldon <larrysheldon () cox net> wrote:

On 9/29/2014 00:32, Pete Carah wrote:

For that matter, has the*specification*  of tcp/ip been proven to be
"correct" in any complete way?


I find that question in this forum really confusing.

I thought all of the RFC-descriptions of protocols were taken to be
statements that "if you do it this way, we think we can inter-operate" but
at no time to be taken as "right" or "wrong".
--
The unique Characteristics of System Administrators:

The fact that they are infallible; and,

The fact that they learn from their mistakes.


Quis custodiet ipsos custodes


Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail


Current thread: