[e-lang] Protocol implementation errors

[Jeroen C.van Gelderen]

On Thursday, Oct 2, 2003, at 17:50 US/Eastern, Bill Frantz wrote:

> From:
>
>>                 -- Security Alert Consensus --
>>                       Number 039 (03.39)
>>                  Thursday, October 2, 2003
>>            Network Computing and the SANS Institute
>>                      Powered by Neohapsis
>>
>> *** {03.39.004} Cross - OpenSSL ASN.1 parsing vulns
>>
>> OpenSSL versions 0.9.6j and 0.9.7b (as well as prior) contain multiple
>> bugs in the parsing of ASN.1 data, leading to denials of services. The
>> execution of arbitrary code is not yet confirmed, but it has not been
>> ruled out.
>
> This is the second significant problem I have seen in applications 
> that use
> ASN.1 data formats.  (The first was in a widely deployed 
> implementation of
> SNMP.)  Given that good, security conscience programmers have 
> difficultly
> getting ASN.1 parsing right, we should favor protocols that use easier 
> to
> parse data formats.

This is a little too anecdotal for my taste. When it comes to security 
I think we can safely ignore anything SNMP. The OpenSSL crew didn't 
(doesn't?) even have an exhaustive test-suite for their DER parsers 
which I believe to be a requirement when a security requirement is on 
the table.

> I think this leaves us with SSH.  Are there others?

While I like the SSH2 protocol because of its simplicity, it forces one 
to use ad-hoc approaches for anything more complex than single-level 
product types. Sum types are not supported at all, apart from those 
offered as primitives, and have to be (are) handcrafted in some ad-hoc 
fashion.


The implementation language seems to be more of a problem than the 
actual data representation formats. I have found that typed high-level 
(declarative) languages supporting sum/product types with pattern 
matching provide near bullet-proof framework for safely marshalling 
data of arbitrary complexity. The compiler will statically check that 
all corner cases are handled. If it compiles, it tends to be correct. 
And creating the corresponding proof is straightforward.

If one is really lucky, one's language supports polytypic programming, 
in which case a single algorithm can marshall arbitrary data structures 
correctly:
  http://www.math.chalmers.se/~patrikj/poly/dc/

The bottom line is that these problems occur because presently 
programmers are required to perform a compiler's job. Just like 
persistence bugs occurs because programmers are forced to do what 
should be the platform's responsibility (c.f. KeyKOS/EROS persistence). 
When language support is not feasible, parser generators can go a long 
way towards eliminating parser bugs.


Cheers,
-J

---------------------------------------------------------------------
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to majordomo at metzdowd.com