[174759] in North American Network Operators' Group
Re: update
daemon@ATHENA.MIT.EDU (Merike Kaeo)
Mon Sep 29 14:07:02 2014
X-Original-To: nanog@nanog.org
From: Merike Kaeo <merike@doubleshotsecurity.com>
In-Reply-To: <CAKr6gn0ikL+MwrJBSYSedD=faPYfQnV4hrfabR0uyh95qoHWew@mail.gmail.com>
Date: Mon, 29 Sep 2014 11:06:47 -0700
To: George Michaelson <ggm@algebras.org>
Cc: North American Network Operators' Group <nanog@nanog.org>
Errors-To: nanog-bounces@nanog.org
--Apple-Mail=_D56A6988-59B0-4A90-A5A5-C80322230851
Content-Transfer-Encoding: quoted-printable
Content-Type: text/plain;
charset=windows-1252
Heh=85.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=85
- 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
>=20
> 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.
>=20
> 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.
>=20
> Certainly I believe there are formally verified protocols. Thats a =
space
> Erlang occupies isn't it?
>=20
> On Mon, Sep 29, 2014 at 4:14 PM, Larry Sheldon <larrysheldon@cox.net> =
wrote:
>=20
>> On 9/29/2014 00:32, Pete Carah wrote:
>>=20
>>> For that matter, has the*specification* of tcp/ip been proven to be
>>> "correct" in any complete way?
>>>=20
>>=20
>> I find that question in this forum really confusing.
>>=20
>> 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:
>>=20
>> The fact that they are infallible; and,
>>=20
>> The fact that they learn from their mistakes.
>>=20
>>=20
>> Quis custodiet ipsos custodes
>>=20
--Apple-Mail=_D56A6988-59B0-4A90-A5A5-C80322230851
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment;
filename=signature.asc
Content-Type: application/pgp-signature;
name=signature.asc
Content-Description: Message signed with OpenPGP using GPGMail
-----BEGIN PGP SIGNATURE-----
Comment: GPGTools - http://gpgtools.org
iQEcBAEBCgAGBQJUKZ+3AAoJEA7gPO9LJuahgdsIAIGDUit/+kos4fkzDNvvGHPC
Ae2rtEtKxFVstpYjESwlchr0TDQ2TP1BD4Y28LZTBjTyU3oJ8t5NTLrV5AFNFkIN
4UUxiOLFhudQ/SY36zXmANIixjPPt4R6jWEXoUK3j7ICRPKMkLlNTXbmh/GxnP4M
3XGrYsDTRBaU9juGrr6D3aU760wJ1tYsg6FLi09wT4KSiY6dz+03yk6q9lz0stc4
6Z44r8xJGkRWl2UTpAF/fuoPmYY1jfQwASj1yuJUdGHVMkf5T4/OxI0jgGuuLGWp
0STDPZjsixYGvNHmgf7zZzf5tDjZRhHBPoE0w8LfPtKGJdAYtduPSdHOFMmfzoM=
=jalD
-----END PGP SIGNATURE-----
--Apple-Mail=_D56A6988-59B0-4A90-A5A5-C80322230851--
