John Day wrote:
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.
C'mon. You don't really believe that do you?
Which one in particular.
The KIV-tool, which I was shown and explained in 1996 by a student doing
his master thesis with it on a module of our software, can output
source code at the end of its processing. Code that is a guaranteed
bug-free implementation of the spec. (which MUST NOT be confused
with the given spec providing the desired behaviour and being free
of unintended (and unthough-of) behaviour).
(While the tool's name appears to originate from the University of
Karlsruhe (->Karlsruhe Interactive Verifier), and that student back
then was from Karlsruhe, the current homepage of the tool appears
to be at the University of Augsburg:
http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/
)
Ever see a compiler with bugs?
Compiler bugs are comparatively rare, many of them are problems
of the optimizer (therefore avoidable) and many happen under
obscure situations that can be avoided by defensive programming
style. Code generators often produce "defensive style code".
Using a robust and mature programming language, such as C89,
may also help to avoid compiler problems of fancy or complex
languagues or fancy features.
Look at the long list of defects of modern CPUs. Apps programmers
that use a compiler rarely have to know (let alone take into account)
those CPU defects because most compiler code generators use only
a subset of CPU features anyway.
Who verified the verifier? How do you know the verifier is bug free?
Now you must be kidding.
Are you suggesting that anyone using the programming language Prolog
would be gambling and could never expect deterministic results?
With a decent amount of expertise and the right mindset,
even mere mortal humans can produce code with a very low error rate.
IIRC, Donald E. Knuth didn't need a formal specification and a
formal proofing tool to achieve a low error rate for TeX and Metafont.
Having started assembler programming at the age of 12 myself, I could
easily understand why DEK used Assembler for his algorithm code examples
in TAOCP when I first encountered these books at age 21.
As I indicated before, I have been working on this problem since we
discovered Telnet wasn't as good as we thought it was. For data
transfer protocols, it is relatively straightforward and can be
considered solved for anyone who wants to bother. The problem is
most don't.
There is a perverted conditioning in our education system and
business life by rewarding mediocrity (cheating, improvising, being
superficial) which is IMO one of the underlying causes for
http://en.wikipedia.org/wiki/Dunning_Kruger
and impairs many implementors' motivation to watch out and compensate for
defects in the spec and to recognize and respect design limits of a spec,
i.e. avoid underspecified protocol features or require official
clarification and adjust the code accordingly before shipping
implementations of underspecified protocol features.
The real problem is the so-called application protocols where dealing
the different semantics of objects in different systems makes the
problem very hard and very subtle. The representation of the
semantics is always of what you think its seminal properties are.
This is not always obvious.
I believe that the real difficulty is about designing and discussing
at the abstract level and then performing formally correct transitions
from abstract spec level to concrete specification proposla level
and comparing implementation options at the spec level ... and getting
everyone that wants to participate to understand the abstraction
and how to perform transitions from and to concrete spec proposals.
I'm experiencing that difficulty myself every once in a while.
In 1995/1996 I had a adopted notion/bias for the uselessness of
traditional GSS-API channel bindings (as defined in GSS-APIv1 rfc1508/1509
and GSS-APIv2 rfc2743/2744) and it took me a few weeks of discussion
to really understand what Nico was trying to accomplish with
cryptographic channel bindings, such as tls-unique, its prerequisites
and real properties and its benefits.
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.
One person's gap is another person's bug. What may be obvious to one
as something that must occur may not be so to the other.
There is a significant difference between a bug in an implementation
and an unintended consequence due to a "gap" in the specification.
The SSLv3 protocol and the IETF successor TLS contains a somewhat
underspecified protocol option called renegotiation, and some apps folks
had the not very bright idea to abuse that protocol option and
made flawed assumptions about protocol properties that did not
actually exist.
Had those apps folks, rather than shortcutting on flawed assumptions,
simply collected the description of the renegotiation properties that
are sprinkeled throughout the TLS spec and put them into a single list,
and then thought about it for an hour, then the problem (the absence of
the property that they wanted to rely on) should have become obvious to them.
It became obvious for me as soon as I had put together that list and
thought about the consequences during discussion of TLS channel bindings.
The human mind has an amazing ability to convince us that how we see
the world is the way others do.
The Dunnin-Kruger effect, "Routine", "habits", are all variations
of trainig a neural network and improving the pattern recognition
over time. The strength of neural networks, to recognize also
variations of known patterns, is also its weakness, a bias/preference
to recognize stuff as something that is already known.
Fixing training errors and trying to add similar distinct patterns
very late usually result in a significant (re-)trainig effort --
and this is where the constant conditioning for cheating, improvising,
superficialness frequently kicks in.
"If all you have is a hammer, everything looks like a nail."
Technically, humans are capable of overcoming the Dunning-Kruger effect
and becoming aware of the limits/boundaries of their knowledge, but
many enjoy a happy life without ever trying to.
Having been on the Net when there were 15-20 very different machine
architectures, I can assure you that implementation strategies can
differ wildly.
I'm well aware that the amount of bad code out there outnumbers
the amount of good code. While I don't think that differing implementation
approaches imply causality for interop problems, there certainly is
the problem of ad-hoc/poor/dangerous/error-prone implementation design
that causes plenty of bugs and interop problems and unexpected
behaviours, neither of which a result of a conscious decisions,
getting shipped into the installed base.
Good specifications are sufficiently clear and precise to enable
smooth interop, yet sufficiently abstract to provide a high level
of implementation freedom as well as future extensibility.
What is much more of a problem is the common lack in recognizing
and respecting limits of a design/specification, and a lack of
compensating for relatively easy to recognize spec defects.
Relatively easy to recognize for a careful implementer, that is,
not necessarily easy to recognize for a mere reviewer.
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).
Which means there will always be a danger of "lost in translation."
The danger is real. If there is a lack of decent leadership,
the resulting spec (defects) may sometimes pose a significant
challenge to implementations&interop.
For consumers of the spec outside of the SDO, the option to
ask for clarification/fix might be non-obvious -- and regularly
is non-trivial for someone who has not previously participated
in the particular SDO (or any SDO at all) -- which is actually
quite common. There are easily two magnitudes more implementors
of specs distributed by the IETF than there are individuals who have
participated in the IETF over the past 30 years.
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.
Do you realize the cost of this amount of testing? (Not saying it
isn't a good idea, just the probability of convincing a development
manager to do it is pretty slim.) ;-)
I fail to follow. Compliance testing does not necessarily require
code or a test tool. Often, compliance will be as simple as actually
_reading_and_following_ the spec, how to process some PDU element.
And compliance testing may be as simple as a code review of less than
an hour and cross-checking a handful MUST and MUST NOTs.
Or what to do with a protocol option/feature one's own implementation
does not recognize, and then _do_what_the_spec_says_
rather than doing what a number of implementations are doing: regularly
aborting with a fatal error rather than doing what the spec says.
Example: the optional TLS protocol extension "Server Name Indication",
first specified here: http://tools.ietf.org/html/rfc3546#section-3.1
"HostName" contains the fully qualified DNS hostname of the server,
as understood by the client.
Doing what the spec says with respect to this requirement:
If
the server only needs to match the HostName against names containing
exclusively ASCII characters, it MUST compare ASCII names case-
insensitively.
If that is not sufficiently clear for an average implemetor to realize
that a case-sensitive comparison (strcmp,strncmp) will be incompliant
with the spec and a case-insensitive comparison (strcasecmp,strncasecmp,
_stricmp,_strnicmp) will have to be used instead, then we might have to
give up and close down the IETF SDO.
According to http://en.wikipedia.org/wiki/Server_Name_Indication#Support
support for this protocol option was originally designed in 2004,
and added into the main codeline of OpenSSL 0.9.8 in 2007.
However, OpenSSL-1.0.1c today still does a case-sensitive comparison...
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.
Being aware of the breakage of the TLS protocol version negotiation
within the installed base in 2009, an explicit reminder was added
into rfc5746 that processing TLS protocol version numbers correctly
in the TLS handshake was vitally important and has always been a
requirement in the TLS protocol spec.
TLS servers implementing this specification MUST ignore any unknown
extensions offered by the client and they MUST accept version numbers
higher than their highest version number and negotiate the highest
common version. These two requirements reiterate preexisting
requirements in RFC 5246 and are merely stated here in the interest
of forward compatibility.
The necessity for the TLS renegotiation info extension had become
painfully obvious after it had been realized that the two TLS connection
states involved in a TLS renegotiation had been completely independent,
enabling an MitM attacker to inject/prefix data of his choice at the
beginning of a TLS session, and the document is very explicit which
precise state information of the previous/enclosing session is carried
over into the successor TLS session and how.
Curiously, one vendor happened to actually break the TLS protocol
version negotiation much worse than it already was, by performing
a check on the client_version in the premaster secret of the
renegotiation ClientKeyExchange message not against the client_version
from the ClientHello from the very same TLS handshake, but instead
check against the client_version of the initial handshake, that had
been found to have painfully independent state and created the
necessity for the rfc5746 fix in the first place...
Simply following what the spec says during implementation would have
avoided the problem. Performing a code review of the reminded
TLS protocol version negotiation would have noticed that breakage.
Interop testing the protocol version negotiation in a meaningful
fashion, even with earlier TLS implementations from the very same
vendor would have clearly shown the breakage prior to shipment.
As it turns out, the vendor failed on all three accounts,
and this _new_ breakage got shipped...
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.
That last sentence is a doozy. You are saying that interop testing
will be required with bad implementations with sufficiently large
installed base that you have to live with it?
It seems to be a recurring event that one or more vendors create
an installed base that is clearly non-compliant with the original
spec, but too large to ignore, and as a result, everyelse adapts
to that behaviour for the sake of interoperability with that
installed base.
e.g. http://tools.ietf.org/html/rfc4178#appendix-C
http://tools.ietf.org/html/rfc5929#section-8
There may be others, but I'm actively tracking only very few
topics in the IETF, so these two are ones I know from the top
of my head.
-Martin