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
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
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
On 09/28/2014 11:14 PM, Larry Sheldon wrote:
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".
Correct. That gave birth to the original "interop" conferences, informal gatherings of people to test out their implementations of the RFCs that eventually grew into the full-blown conference we know today. Frankly, this is where Mr. Stevens was instrumental in making the Internet what it is today.
On 09/29/2014 01:14 AM, Larry Sheldon 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 was adding it to Valdis's statement about proven correctness of the TCP/IP stack. It is only possible to prove correctness of software in relation to a (assumed) correct (and complete) specification. Correct software relative to a spec that doesn't relate to the real world may be considered correct but will still fail in application. Many of the famous failures of military systems (and many more from commercial systems) come from bad (or missing) assumptions in the spec, (and many also from bad implementation, to be sure...)
The thread in question is more about security than interoperation, and real-world effects of both compliant and non-compliant uses of the net. The real point is that many of the features included in tcp/ip to handle random occurrences make purposeful interference *worse*. In a world with purposeful attacks, those specifications have to be amended; in that sense they are not "correct".
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 use of modals (MUST, MUST NOT, SHOULD) in the specification implies a sense of correctness. Indeed that is mostly there to guarantee interoperation. In the early days (pre-mid-80's) the security aspects of the protocols was minimal; it was assumed that people would pay attention to the specs. Now we have players that (use spam for an example, again) (mostly) completely comply to the technical specifications but manage to bring the net to its knees anyhow, and also players that test what (mostly) minor violations to the spec will do to the rest of the net. (try to defend against a joe-job using stock qmail, for example; that system is completely compliant to the (older) RFCs and cannot handle significant amounts of forged mail, mostly due to its completely compliant handling of bounces. And some of the MUST statements in earlier application protocols (821/822, for example) have had to be turned off in order to defend against such purposeful actions (e.g. bounce all messages that fail delivery; doing so makes the spam problem MUCH worse.) The protocols have to be adapted to handle attacks, there is no alternative. In that way, there is (in some sense) correctness or not. At least the RFC system does allow for fairly easy (but not too easy) modification with experience. -- Pete
participants (5)
-
George Michaelson -
Larry Sheldon -
Merike Kaeo -
Pete Carah -
Stephen Satchell