1. 12
  1.  

  2. 8

    SSL libraries aren’t bananas, though, and I think this is where the argument falls down. For instance, SSL libraries don’t have immune systems – if a vulnerability exists in one instance, it exists in all of them.

    Yes, having fewer implementations means that vulnerabilities affect more users – but, it also means that the vulnerabilities are easier to fix, and more effort is concentrated in the implementations that exist.

    To put it another way: if we’re not (collectively) capable of writing one correct implementation, why would it be easier to write three, or five, or ten, correct implementations? The problem isn’t diversity, it’s the fact that we don’t know how to write a correct SSL implementation.

    (Moreover: I would speculate that we don’t yet have the tools to do so – formally verified systems seem too cumbersome to use, C is too unsafe, and Haskell doesn’t seem to allow control of resources sufficient to prevent information leaks).

    EDIT: added the word “yet” to the previous sentence: “we don’t” -> “we don’t yet

    1. 5

      formally verified systems seem too cumbersome to use

      This was posted on Lobste.rs about a month ago, and seems more relevant now:

      https://lobste.rs/s/amusph/mitls_a_verified_reference_implementation_of_the_tls_protocol_written_in_f_and_specified_in_f7/comments/nlpe3v

      1. 4

        Not all the problems are technical. The way in which the organization behind the project is run probably matters more than any given piece of code, and that is closer to being ‘like bananas’ (i.e. we get benefits from diversity). I’ve a blogpost detailing some thoughts about that here: http://rz.github.io/articles/2014/apr/security-orgs.html

        formally verified systems seem too cumbersome

        fwiw, it is not impossible: see https://github.com/vincenthz/hs-tls

        1. 3

          Is hs-tls actually formally verified, though? It looks like it’s just written in Haskell, which is a big bonus on ‘free theorems’, but falls short of formal verification. Moreover, I’d be afraid of information leaks via timing, etc., as noted.

        2. 2

          SSL libraries don’t have immune systems

          Use of valgrind and automatic methods for catching use after free are somewhat like immune systems. Sophisticated type systems, design by contract, or comprehensive unit tests are somewhat like immune systems.

          To put it another way: if we’re not (collectively) capable of writing one correct implementation, why would it be easier to write three, or five, or ten, correct implementations?

          That’s not the point. The point is that the various systems aren’t all vulnerable to the same single bug all at the same time, or at least to minimize the chances of that happening.

          1. 2

            As a user of an SSL implementation, though, it doesn’t really matter to me whether I’m vulnerable to some particular bug – it matters whether there is a vulnerability.

            Having everyone be vulnerable to different bugs instead of the same bug isn’t really much of a benefit – all the users are still vulnerable, just in different ways. It’s only a benefit if there are fewer bugs, and I don’t think that more implementations in total reduce the number of bugs in each implementation.

          2. 1

            Yes, having fewer implementations means that vulnerabilities affect more users – but, it also means that the vulnerabilities are easier to fix

            Why is this the case?

            1. 1

              Some formal verification can be annoying but I definitely think we should still try at least some. Someone here in Boulder has recently started a very exciting Idris library for this:

              https://github.com/idris-hackers/idris-crypto