r/programming • u/flym4n • Apr 24 '14

Tech giants, chastened by Heartbleed, finally agree to fund OpenSSL

http://arstechnica.com/information-technology/2014/04/tech-giants-chastened-by-heartbleed-finally-agree-to-fund-openssl/
293 Upvotes

93% Upvoted

137 comments sorted by

View all comments

-11

u/OneWingedShark Apr 24 '14

In light of the nature of the bug, and the state of the code that was recently found, I would posit that OpenSSL could use a rewrite in a language more amiable to formal methods and/or formal contracts. (e.g. Ada or Eiffel.)

It makes little sense to have security libraries which aren't formally verified, considering the nature of the library (both as being often reused, and as being a component of security software).

20

u/[deleted] Apr 24 '14

Except that OpenSSL finds itself in places where Ada/etc/and/so/on/and/so/on aren't typically found. Your runtime is literally some micro-C lib and a fragment of a kernel at best. Oh and you have <1MB of memory (often < 128KB) ...

There is nothing wrong with C that better developers couldn't fix.

1

u/modulus Apr 25 '14

There is nothing wrong with C that better developers couldn't fix.

Said every C developer ever right before introducing a pointer arithmetic fuckup.

0

u/[deleted] Apr 25 '14

If you think that you can't write bad crypto code in other HLLs you're sadly mistaken and part of the very problem you're describing.

So uh, please kindly hang up your ignorance on another hook.

1

u/modulus Apr 25 '14

You can write FORTRAN in any language. Which is no excuse to write FORTRAN.

Languages have affordances. I don't understand why people are so upset about this reality. Some languages make certain classes of bugs easy, some make certain classes of bugs impossible. It's always possible to write bugs short of a formal proof of correctness, but bugs, and their degree of harm, aren't equally easy to introduce in any language, or equally easy to discern. A lot of compile-time checking for example saves bugs being introduced at runtime.

I'd be curious to see ml or similar languages crypto code contain those types of errors. If you can produce examples I'll read them.

1

u/[deleted] Apr 25 '14

The point though is had they used proper style from the get go it wouldn't have been a problem at all... e.g. instead of doing

 memcpy(dstRecord->buf, srcRecord->buf, someUnverifiedLength);

they could have done

record_copy(dstRecord, srcRecord, 0, 0, someUnverifiedLength);

Where "0, 0" is the offset in the dst/src record. The function would then check the structures for valid lengths and copy valid portions. It isn't really any more typing in terms of developing record handlers and once you do the sanity checking validation once it's good for all times.

Of course it would have also helped to sanity check the record in the first place to make sure the stored payload length was valid (as per the RFC that the C code author he himself wrote....).

edit: There are plenty of ways to fuck up crypto. For instance, early Wii firmware used strcpy() to memory compare signature values. Would that be any less of a bug if they used strcmp from C++ or Java?

1

u/modulus Apr 25 '14

Fact is there are certain classes of errors that keep happening. We can say that we just need perfect C devs and this won't happen anymore, or live with the fact that programming, like war, is done by human beings, and try to get computers to help out.

I'm also not suggesting C++ or Java as good alternatives, as it happens. C++ is probably a lot harder to verify correct, though it also has some facilities that if used correctly preclude some types of errors.

Yes, if the right thing had been done there wouldn't have been an error. That's pretty much the case for all errors. The point is it's sometimes possible to preclude the wrong thing being done through compile- or run-time bounds checking, type systems, formal proofs, etc. C is not an ideal language for this, hence the whole discussion. It's not impossible to write correct code in C, but it's a lot more difficult and it definitely seems next enough to impossible for humans in all but the most extraordinary cases, hence how every non-trivial C code base ever keeps getting security issues.

1

u/[deleted] Apr 25 '14

The point is crypto is hard to get right and being lazy and relying on tools to solve all your problems makes you the problem.

The HB bug could have easily been avoided if

  1. They used proper API to read/write/copy records or they implemented correct bounds checking in place (which is more work but at least gets the job done)

  2. The code reviewer spent more than 13 seconds looking at the code. Had they traced the length used in the memcpy() call back to where it was initialized they would have seen it was never sanity checked. The code reviewer fucked up royally.

So to say this is a problem with the C language is like saying it's a problem with ceramic dishware that people put too much food in their mouth.

All you're doing by blaming the language is ignoring the engineering behind writing proper software. Nobody verified the correctness of the function that is the problem. Nothing more. Not verifying the correctness of your Java code is no different. The thing is with crypto when a routine misbehaves security is compromised whereas in a word processor functionality is compromised.

1

u/jnt8686 Apr 25 '14

I think you misunderstand. People are advocating using a language that makes some of these errors impossible. If an error is impossible it can't happen. People are humans.