Hacker News Reader

There is a formally verified implementation of TLS in F# (comes from Microsoft Research, if anybody cares):

http://www.mitls.org

However, there are gotchas. At this point the TLS protocol has gotten pretty complex. Even the act of just stating what the desired security property are is not simple. Furthermore, understanding what their proof means requires you to go through at least two of their papers (and probably both of their tech reports to grok it fully). Then you need to look at the code itself and the different assertions/assumptions spread throughout, and make sure that those conform to the properties you expect. Even if you are familiar with the field, starting from scratch would probably take you a couple of weeks, just to gain confidence that what they prove is correct. And it might be possible that there are some features of TLS that they don't implement (as you can tell, I haven't taken the couple of weeks to fully understand their stuff).

Sounds complicated. Let's just build an AI that can program, and trust it when it says it's not spying on us.

My assumption would be that this formally verified implementation is not optimized, and therefore runs rather slowly compared to the C implementations. Plus it requires the .NET framework or Mono to run it. Am I off base?

I would imagine it is 'optimised for verification' rather than for speed, ie. the code will be written to follow the structure of the specification.

However, the nice thing about having a verified implementation is that it can be used as the specification (reference implementation) for any other optimisations you want to make.

Such a two-step process is usually much more tractable than trying to verify optimised code directly. This is used extensively by BedRock ( http://plv.csail.mit.edu/bedrock/ ) which uses functional programs as specifications and an assembly-like language for the "real"/optimised implementation. The resulting verification problems are straightforward enough to be mostly automated.

No, you're right on target. They are using non-optimized data structures, and rely on (Bouncy Castle's) managed code for encryption. From their paper, the throughput is around 10x slower than OpenSSL (but much closer to JSSE). My guess is that one could probably speed this up significantly, while still retaining the guarantees, but that's probably less interesting to these guys.

As for Mono or .NET, I assume so (AFAIK that's the only way to run F# applications).

As I said in a similar post, their proofs show that their implementation is logically correct--their implementation will behave according to their formalization of the RFCs.

This says nothing about how secure it is with respect to side-channel attacks. For example, they admit that they did not model time in their proofs, so they have NOT proved that they are immune to timing attacks. Moreover, F# runs on top of the unverified CLI--bugs in the CLI can be used to break miTLS.

There are certainly large commercial entities who have sufficient incentive to keep OpenSSL secure that they really ought to be contributing actively to the project; I wonder whether Amazon might step up given how badly (and publicly - witness Mojang's taking minecraft services offline and pointing the finger at Amazon as the vendor they were waiting on to fix things - https://twitter.com/notch/status/453529143121309696) they got bitten by this vulnerability. Cloud hosting companies clearly have a responsibility to deliver trustworthy services, and that means they need to be deploying software stacks they can rely on not to screw them; either they will need to step up and support OpenSSL or switch to different SSL solutions that have stronger guarantees. Network appliance vendors like F5 and Cisco also have a clear interest in fixing this stuff. Question is, will they?

(disclosure - I work for IBM, though not in cloud infrastructure. What I say for Amazon applies to our cloud services guys too.)

I'm not sure that OpenSSL is the project they ought to be contributing to. It looks to be beyond repair architecturally (as a project as well as codebase).

How in the heck is this mess of a project so popular?

Age, momentum; "network effects."

It's a readily-available collection of complicated things (ciphers, digests, cryptographic protocols, etc) that everyone needs. Implementing 'yourself' (your company, whomever) takes lots of time and thus money. It seems the world made the assumption that this open source project was the end-all be-all of cryptographic implementations.

This. How often are we told not to implement crypto ourselves? And the name is marketing perfection: OpenSSL. Yes, that's exactly what I want.

It was developed outside the US at a time when the US had export restrictions on strong crypto. Now that those restrictions are gone, anybody can just use NSS instead.

Are the alternatives much better? GnuTLS has had it's fair share of embarrassing bugs too and I can't think of a 3rd open source product that's as mature.

> a 3rd open source product that's as mature.

NSS, which is used by Mozilla and Chrome. For Apache, just google mod_nss or read this: https://stomp.colorado.edu/blog/blog/2010/06/04/on-setting-u...

It looks like NSS isn't supported on nginx. Hope somebody puts that on their todo list!

NSS is more complicated, for a lot of reasons. As I recall, it handles its own keystore which it doesn't share with other implementations (e.g. the ca-certificates package in Ubuntu/Debian); it requires you to initialize the keystore manually and teardown when you're done, but sometimes you don't know if anything else has done the initialization, so you don't know if it's safe for you to tear it down.

There are other issues as well; not blocking problems necessarily, but reasons why it might not be a great implementation or why it would break the way current SSL works for distro maintainers and users.

It's hardly a problem of open-source, it's a problem of open-incentives. While nobody disagrees the project is critical for everyone, are you (or I) willing to make it a priority? It's a essentially a "who will build the roads" issue.

Yeah, free software isn't a development model and it doesn't mean it's made by amateurs. As another prominent free project with a much better track record for security and stability, consider OpenSSH, the crown jewel of the OpenBSD crowd, a free software distribution itself popularly renowned for its security. Theo's criticism here of OpenSSL carries a lot of weight.

Note that despite being the crown jewel, OpenSSH's security page lists about two dozen vulnerabilities it has had at some time in the past.

Of course, they are disclosing their vulneratiblities, they disclose everything, and they have an established audit process. Quite the leaders in security in the free software world:

http://www.openbsd.org/security.html

Generalization in this case is really unhelpful, since there is almost no diversity in SSL libraries. There is 3 of them, but almost everyone uses openssl.

One case do not make a trend at all, and two cases is the worst statistical proof there is for trends.

On the positive side, open source model of development do allow projects to use not only what is common, but also the exciting fronter regarding security models. My project has used gnutls with pgp for 6 years now, nicely avoiding all those 2 major vulnerabilities, and that was only possible because someone found themselves wanting to implement the new TLS standard that supported pgp keys.

gnutls has also had vulnerabilities and it gets less attention, I guess you mostly got lucky.

Sadly, it'll never become popular because of the license.

The same license that some libraries inside Starcraft 2 has.

But blizzard must be one of those small companies that do not care about profits, or have no lawyers. No "serious company" or serious software would dare to use LGPL, right?

But instead of arguing license religion, I suggest we move back to the topic of OpenSSL and vulnerabilities.

You know as well as I do that LGPL is not always an option. A very visible case is console games.

But yes, let's go back to lamenting the state of crypto libraries, we can at least agree on that.

I would actually be interested in hearing some of the issues related to LPGL in video games and other projects. Are there stories / write ups on this that you could link to or would you mind explaining it some?

Based on some informal research I did ~10 years ago (i.e. I ready the LGPL as a high school student), the LGPL requires, among other things, an end-user license allowing reverse engineering. The LGPL isn't just "my code is GPL, the rest of the program is whatever"; it puts forth some requirements for the entire finished product that are either impractical (must include source code) or illegal (would violate NDA or other license terms for the console libraries) for console games.

Only reverse engineering for debugging modifications of the LGPL code in derivative works.

if you try to reverse engineer the protocol starcraft 2 uses with battlenet, you will have a hard time arguing in court that the LGPL license gives you permission to do so. If I recall right, starcarft 2 has some heavy restrictions on reverse engineering for this specific purpose, and I trust their lawyers to actually understand this difference.

For console games (which starcraft 2 is not), the console environment is incompatible with LGPL. If adaption of a security library depend on the console market, then such adaption won't happen.

I'm not aware of any long form text on this, but the issue is relatively straightforward.

A publisher hires a studio to make a game, which then gets published on platforms that actively prevent users from (compiling and) running their own software (consoles, iOS).

Since the user is not provided with the tools to replace a library used in a game, the terms of the LGPL cannot be met even if the studio were to release the source to their version of the library.

In fact, even if they released the source to their whole game (something the publisher would never allow) the LGPLv3 still cannot be met because of the anti-Tivoisation clause, which stipulates that users must be able to run their own compiled version of the software.

Would a clause in LGPLv3 that exempts the publisher/distributor from limitations beyond their control (console/iOS restrictions) help?

Also, I think the the user isn't prevented from recompiling and running altogether; a user can get a developer account. Although, I guess that presents an additional cost, something (L)GPL might be against.

>Would a clause in LGPLv3 that exempts the publisher/distributor from limitations beyond their control (console/iOS restrictions) help?

I doubt very much that RMS would want to add such a clause. Remember, the GPL and LGPL are political tools as much as software licences. They exist to move the world in a certain direction. Adding such clauses would reduce their reason for existing.

A linking exception from the library authors could accomplish that, I believe it's what GCC uses. LGPLv2 may also be ok, but GPL licenses in general are complex enough that no one is entirely certain.

If the library is statically linked (which is the case at least on consoles), the user would also need the game's source code. I think the restriction is enough to trigger the (L)GPL clauses anyway.

> Would a clause in LGPLv3 that exempts the publisher/distributor from limitations beyond their control (console/iOS restrictions) help?

Tivo would just create a complicated enough corporate structure to provide the same shroud for themselves and will then be able to satisfy all requirements.

I believe that GnuTLS is under LGPLv2 though.

My attitude towards complaints about open source projects is that if you think the errors are rudimentary then just submit some patches. If there is not enough test coverage then add one. This applies especially if you believe that the project is critically important.

I think what might be happening here is expert syndrome. People may be told that if they're not experts then they shouldn't be reviewing or changing the code.

Even if you work on a commercial project, where there is a reasonably stable core team, people just committing stuff, even if it's in itself pretty good stuff, won't result in good overall code quality. You need to have a systematic process, including a detailed coding standard, requirements about test and documentation coverage for submitted code, precise guidelines for contributing, rules of code review, and you need people who understand the whole project, review pretty much all of the code changes, have an overall development schedule in mind including refactorings and technical improvements, and all the time putting work into maintaining overall integrity of the project:

http://c2.com/cgi/wiki?ConceptualIntegrity

This is pretty much a must for any project where there is more than one person working, and the more people contributing or the more mission-critical the project the more of this kind of high-level coordination is required. Some open source projects with strong leadership do get to this kind of integrity, but most don't. It's easier when there is a relatively small team of very dedicated individuals, but some large projects have succeeded to some extent in building a real development culture in an open source setting, like Linux.

The failure mode with this approach is that it disallows coaching.

There may be some bug in a library that's similar to what I do for my day job, and I spot it immediately. Or perhaps I've seen the inevitable results of certain design decisions play out in multiple organizations.

I may not have time to code up a patch. Frankly, I've got about 5 projects on the go besides work and kids.

So, FOSS projects may lose out on that kind of expertise that could easily be crowd-sourced if it didn't ask so much of contributors.

^ this!

back in 2010, my business partner, marco peereboom, submitted a patch to openssl to add support for aes-xts. it was coded by joel sing, now a google employee and golang dev. they _didn't even respond to the mailing list email_ and after marco nagged for a reply the response was "we have a different plan for how to implement XTS" (i'm paraphrasing). _2 years later_, they added XTS support.

the openssl dev team is not responsive, doesn't accept contributions and generally speaking suffers from "you're not an expert" syndrome. look how expertly they've managed their project!

Well maybe his patch really wasn't in line with how it needed to be. I've always hated openssl but I'm not sure this is a valid case.

Sounds like this: https://www.peereboom.us/assl/assl/html/openssl.html ;)

Well, I can code myself out of a hole I have coded myself into. But I guess the world is a better place because I don't try to help crypto projects by contributing.

A while back, I tried submitting a patch to OpenSSL. It was a 3-line change (IIRC) related to the build process - in a particular esoteric setup, the build failed. Got literally zero replies regarding the issue on the mailing list, their IRC channel and on my/their github pull request.

I'd love to contribute more often to other OSS projects. But this behavior is more common than not.

this behavior is more common than not

This has not been my experience. I've contributed to many different projects, large and small (chpasswd, sendmail, apache, git, gerrit, openconnect, homebrew, msmtp, textmate, ...) and never had trouble getting a patch accepted.

edit: downvotes, really?

Those projects don't suck, though. When projects (continue to) suck, it's usually because their maintainers suck. When maintainers suck, it's hard to get patches in.

I've also submitted patches to OpenSSL and been entirely ignored[1]. The latest of which strictly improved testing, documentation and included a detailed study and write-up of actual bugs in OpenSSL and downstream code[2].

My conclusion was that the OpenSSL project is not interested in external contributions.

[1]: https://www.mail-archive.com/openssl-dev@openssl.org/msg3362...

[2]: http://jbp.io/2014/01/16/openssl-rand-api/

Stiff, I think you answered your own question. Intel HIRES them, open source projects don't generally hire people. They sit around and wait for someone to contribute. Are you truly surprised that a volunteer created software is not as rigorously tested as software created by Intel?

Being FOSS doesn't have to mean relying on volunteers. Linux is mostly written by paid developers; why isn't OpenSSL, considering its reach in the commercial world?

Slightly off topic, but do you know whether the paid developers of Linux work on the core kernel, or on device drivers?

Both, as they provide the bulk of the code. It would be more illuminating to examine where the unpaid volunteers contribute. My guess would be device drivers, but I don't know.

This has some information although not exactly what you wanted to know:

http://lwn.net/Articles/579081/

I had some problems expressing what bothers me clearly and edited the comment heavily, perhaps it makes more sense now. You're right it is not that surprising, but it's still disappointing that even the most rudimentary best practices are not adopted. Have a look at sqllite for comparison, also an open source project, also in C, certainly less mission critical, and what a difference:

https://github.com/smparkes/sqlite/tree/master/test

https://github.com/smparkes/sqlite/blob/master/src/rowset.c

sqlite does not seem less mission critical to me, and definitely relied on funding:

"D. Richard Hipp designed SQLite in the spring of 2000 while working for General Dynamics on contract with the United States Navy.[7] Hipp was designing software used on board guided missile destroyers" -- http://en.wikipedia.org/wiki/Sqlite#History

I work for a very large company that relies on a fork (with contributions back upstream) of SQLite for a majority of its massive enterprise SOA. It is not just unpaid volunteers keeping that project going.

What do you consider when choosing SQLite issues to assigns resources? I would guess it would start with issues relevant to your roadmap. If that's the case with most enterprise FOSS contributors, they most likely trusted the features of OpenSSL they were using. Thus no reason to go poking around that section of the code. It's understandable why a team might choose to not perform an ad-hoc security audit of features that pass specs, even more so when such an audit requires niche expertise. We can hope this bug changes that attitude and more enterprises with the resources and knowledge start performing security and encryption audits. Just as your buildings have security guards, we need proactive and preemptive audits of at least the most common libraries is use, flagging of software that implement unaudited encryption libraries. A Travis CI like badge on GitHub for these audit metrics would bring attention to the problem. We could call it EncryptCI. Maybe this already exists?

A number of the OpenSSL team are employed by large tech companies to work on OpenSSL. For example Bodo Möller and Ben Laurie work for Google.

This bug was in fact discovered by a Google employee: https://www.openssl.org/news/secadv_20140407.txt

I agree this is incredibly surprising. Even beyond typical production testing it seems to me that critical infrastructure crypto should have a formalized testing structure based on logic and information theory (as I had assumed OpenSSL did). Build trust from the bottom up. Test that only known affirmatively tested primitives are used for memory allocation, and other known sensitive operations. Things like buffer overflow, range checking, executable code in data, etc. can all be easily tested.

There is a lot of work in crypto research about trust in the logical and mathematical sense, why is this work not applied to software testing at least for infrastructure crypto?

P.S. By way of incentivizing this work... seems like a pretty good dissertation topic.

> I also wonder how much in the end the big institutions care about this stuff.

Well, if they did care more, you'd see engineers from Intel, IBM, et. al., contributing to the project in droves like they do with the Linux kernel.

Or maybe not after the current maintainers roll our their not so welcome mat.

Chrome and Firefox both use NSS. I would assume that the big institutions looked at OpenSSL and decided their money would be better invested in other projects.

"Big institutions" already did that. It's called NSS.