It seems odd that I haven't seen a full state diagram (including send/receive packet details) for SSL, unlike e.g. TCP, since I think that having one, either as part of the spec (which only contains a brief one for the handshake sequence) or created from it before writing any code, would've made it much more difficult to cause bugs like this. At least I've found state diagrams very useful when working with protocols like this.
Agreed. The sheer brilliance of clarity in the classic TCP/IP Illustrated: Volume 1 - The Protocols only becomes visible in hindsight. Anyone know if the the LaTeX source for its diagrams are available? I have been able to emulate them for the most part in graphviz using shape=record when required, but wonder if that was the technique used.
(PS. Reading the above tome ~1999, I actually discovered numerous specification flaws in the RFCs ... eg. for ARP and ICMP, that could be used for remote OS detection.)
What is interesting is that the (core?) of OpenSSL was re-written in Coq according to the author. Then the natural question can that representation be used to generate C code from it and would that make a safer product.
It seems like the author was able to discover the vulnerability while in the process of specifying it in Coq (understanding the handshakes better during specification).
From what I read the Coq specification itself wasn't complete or used to discover the vulnerability.
Would be great if the author shed some light here.
That seems correct. He discovered it while creating the coq specification but coq wasn't itself used to discover the bug. He confirmed that much in this podcast (It's in Japanese though): http://mozaic.fm/post/88061749963/4-security-protocol.
I very much hope that some next big crypto / security library will be designed and tested in some rigorous language like Haskell, its key parts proven correct with something like Coq, and then an efficient and portable implementation code generated automatically.
A C implementation seems inevitable, but an easy-to-link Rust implementation would be very nice to have.
It's funny, I just assume open source security oriented development would follow far more rigorous testing and verification than it apparently does. I guess it's no different from every other kind of development - testing and verification are not the fun part. Human incentives being what they are, this keeps playing out. Bounties are probably the only practical way to reverse those incentives because making that cash makes testing and verification fun again.
Well, this is sort of fudd being spread by the libressl project.
Most old and large codebases will have a mix of coding styles, etc... even at big companies (take a gander at the recently posted Windows 2000 source code for example, or the leaked Half Life 2 codebase, etc).
Does it make testing more difficult with preferred tool X? Maybe... but perhaps tool X isn't the best fit for the codebase? Or perhaps minor changes could be made to make it work well.
In any event... part of being a developer is being able to read and understand a variety of coding styles... since, coding styles have zero effect on the code's purpose/execution.
Not trying to detract... but we should remember the people who complained about the coding styles and difficultly in reading/understanding the codebase were new to the codebase, and the codebase was not in their expected format... which is normal when you sit down to any new codebase. Also... this is a crypto codebase... so there will be an element that is always difficult for an outsider to read and understand.
The OpenSSL developers intentionally breaking malloc/free and making other ridiculous engineering decisions is not 'mix of coding styles', it's literally incompetence.
I would be careful before you throw the "incompetence" word around. Remember this library was written by some of the best cryptographers around, and has been the standard for a very long time -- because, generally, it does it's job very well.
If you actually look into these "ridiculous engineering decisions" you will find very good reasons why they did things the way they did.
With that said, of course it may be able to be done better. All code can be done better. Remember the OpenSSL team was severely underfunded, and severely understaffed. So it's not fair to label them as "incompetent" one bit.
I think the key term in your comment is "cryptographer". Not software engineer, but cryptographer. The actual encryption that goes on in openssl is very good, but the engineering which surrounds that cryptography - not so much.
Maybe I'm weird but writing a test, seeing it fail, fixing the bug, and then seeing it pass is quite delightful. Having a set of 100+ test, doing a large refactoring and seeing them all pass, is a completely joy. Then again, I also like writing documentation.
Proposal: When something is completed according to the devs a bonus is posted. For every vulnerability discovered by all the other devs in the company a portion of the bonus gets paid out. If an 'x' period has passed and no vulnerabilities have been discovered the remainder is paid out to the original devs.
Your proposal is interesting in an office dynamic sense, however I feel that the problem is really time pressure, not a lack of quality pressure. Additional carrot (financial reward) for programmers is always good, but perhaps a more meaningful range of attacks would only be made by experienced external consultants... and the size of the fund must then be large enough to interest them.
For fun, I just duckduckwent 'make a game of it' and got some amusing responses in the context of this suggestion.
Kids can make a game out of almost anything! See more about gross motor activities, outdoor play and pool noodles.
Whatever you'd like to improve about your life, try making it into a game. Challenge yourself. Make up your own rules. Then play it to win.
When the family gets so big that you no longer can buy holiday gifts for everyone, you have to find an alternative. For many, that turns the gift exchange into a rousing game. "We used to buy for everyone and I enjoyed that, but in the last couple of years, we had to face the fact ...
I decided to put together my own Iron Rations and make a game of it. You are welcome to play. I hope you have some helpful ideas to add to the stash. The rules are: Everything must be shelf safe with an expiration date or best by date of at least two years.
Principal Skinner: Oh, licking envelopes can be fun! All you have to do is make a game of it. Bart: What kind of game? Principal Skinner: Well, for example, you could see how many you could lick in an hour, then try to break that record.
Perhaps but there are so many more actually fun "games" than testing your code that you are again fighting natural incentives - people will pick the most fun game when given the choice of many, yes?
