ietf
[Top] [All Lists]

Re: Making RFC2119 key language easier to Protocol Readers

2013-01-09 02:03:40
Hi Martin,

I agree with your points below, if any one finds an error in IETF
standards then should report it on this list or write an ID about that
to community,

AB
++++++++++++++++++++++++++

Sub: Re: A proposal for a scientific approach to this question [was
Re: I'm struggling with 2219 language again]

http://www.ietf.org/mail-archive/web/ietf/current/msg76710.html

I believe that the problem with the formal logic is that it is difficult
to both write as well as read/understand, and to verify that the chosen
"axioms" actually reflect (and lead to) the desired behaviour/outcome,
the relative of scarcity of suitable tools, the complexity of the
underlying theory and tools, and the tools' resulting lack of
"intuitive usability".

Once you have both, there is still the problem that if a bug or ambiguity
shows up,

For any formal proofing system worth its dime, this can be 100% ruled out,
since the proofing system will emit a 100% bugfree implementation of the
spec in the programming language of your choice as a result/byproduct of the
formal proofing process.



 neither the code nor the formal spec nor a prose spec can be taken
be the right one.  What is right is still in the heads of the authors.

But maybe you're not really thinking of a defect in the implementation
(commonly called "bug") but rather a "gap" in the specification that
leads to unintended or undesired behaviour of a 100% bug-free
implementation of your spec.

(see Section 4 of this paper for an example:
  http://digbib.ubka.uni-karlsruhe.de/volltexte/documents/1827
)


Donald Eastlake wrote:

Another problem is maintenance. Protocols change. Having to maintain a
formal specification is commonly at least an order of magnitude more
effort than maintaining a prose description.

Definitely.  Discussing protocols at the level of formal specification
language would be quite challenging (typically impossible in an open
forum, I believe it is even be difficult in a small and well-trained
design team).



And, as has been mentioned before, I'd like to emphasize that the IETF
experience and principal is that, if you want interoperation,
compliance testing is useless.

Ouch.  I believe this message is misleading or wrong.

Compliance testing is VERY important, rather than useless,

Compliance testing would actually be perfectly sufficient iff the spec
was formally proven to be free of conflicts and ambiguities among
specified protocol elements -- plus a significant effort spent on
ensuring there were no "gaps" in the specification.

As it turns out, however, a significant amount of implementations will
be created by humans interpreting natural language specifications,
rather than implemenations created as 100% bug-free by-products of a
formal proof tool, and often, interop with such buggy, and often
spec-incompliant implementations is desirable and necessary since
they make up a significant part of the installed base.



The way to interoperation is interoperation testing between
implementations and, to a first approximation, the more and the
earlier you do interoperation testing, the better.


The #1 reason for interop problems and road-block to evolution of
protocols is the wide-spread lack of compliance testing (on the flawed
assumption that it is useless) and focus on black-box interop testing
of the intersection of two subsets of protocol features.

The problem with interop testing is that it really doesn't provide
much of a clue, and the results can _not_ be extrapolated to features
and areas that were not interop tested (typically the other 90% of the
specification, many optional features and most of the extensibility).


The near complete breakage of TLS protocol version negotiation is a
result of the narrow-minded interop testing in companion with a complete
lack of compliance testing.


If done right, pure compliance testing can go a long way to providing
interop.  The only area where real interop testing is necessary is
those protocol areas where the spec contains conflicts/inconsistencies
that implementors didn't notice or ignored, or where there is a
widespread inconsistencies of implementations with the specification,
of created by careless premature shipping of a defective implementation
and factual creation of an installed base that is too large to ignore.


-Martin