Security software verifiability

There has been a great deal of fallout from the Snowden leaks so far, and one gets the sense that there is a lot more coming. One of those consequences was the voluntary shutdown of the Silent Mail secure email system. That action was, to some extent, prompted by the shutdown of the Lavabit secure email provider, which was also "voluntary", though it was evidently encouraged by secret US government action. The Silent Mail shutdown spawned a discussion about verifiability, which is also a topic we looked at back in June.

Zooko Wilcox-O'Hearn, founder and CEO of LeastAuthority.com, sent an open letter to Phil Zimmermann and Jon Callas, two of the principals behind Silent Circle, the company that ran Silent Mail. Given that Silent Mail was shut down due to concerns about a government coopting or abusing the service, Wilcox-O'Hearn asked, what guarantees are there for users of Silent Circle's other products: Silent Text for secure text messaging and Silent Phone for voice and video phone calls. There is little difference between the threats faced by all three products, he argued:

Wilcox-O'Hearn went on to point out that the Hushmail email disclosure in 2007 showed that governments can and will require backdoors in both client and server code. At the time of that disclosure, Zimmermann (who is known as the creator of Pretty Good Privacy, PGP) was on the board of advisers for Hushmail and noted that unverified end-to-end encryption is vulnerable to just this kind of "attack". At the time, Zimmermann said:

That came as something of a surprise to some at the time, though perhaps it shouldn't have. In any case, given that Silent Circle's code is open (released under a non-commercial BSD variant license), unlike Hushmail's, the real problem is that users cannot verify that the source and binaries correspond, Wilcox-O'Hearn said. It is not only a problem for Silent Circle, but also for LeastAuthority.com, which runs a service based on the Least Authority File System (LAFS, aka Tahoe-LAFS), which is open source (GPLv2+ or the Transitive Grace Period Public License). The open letter was essentially an effort to highlight this verifiability problem—which affects far more companies than just Silent Circle or LeastAuthority.com—particularly in the context of government-sponsored attacks or coercion.

Callas replied to the open letter (both also appeared on the cryptography mailing list), in essence agreeing with Wilcox-O'Hearn. He noted that there are a number of theoretical results (Gödel's incompleteness theorems, the Halting problem, and Ken Thompson's Reflections on Trusting Trust) that make the verifiability problem hard or impossible. For a service like Silent Circle's, some trust has to be placed with the company:

So, Silent Circle is essentially repeating the situation with Hushmail in that it doesn't (and really can't) provide verifiable end-to-end encryption. The binaries it distributes or the server code it is running could have backdoors, and users have no way to determine whether they do or don't. The situation with LeastAuthority.com is a little different as the design of the system makes it impossible for a LAFS service provider to access the unencrypted data, even if the server code is malicious. In addition, as Wilcox-O'Hearn pointed out, the client side binaries come from Linux distributions, who build it from source. That doesn't mean they couldn't have backdoors, of course, but it does raise the bar considerably.

But even verifying that a source release corresponds to a binary that was (supposedly) built from it is a difficult problem. The Tor project has been working on just that problem, however. As we reported in June, Mike Perry has been tackling the problem. In a more recent blog post, he noted some progress with Firefox (which is of particular interest to Tor), but also some Debian efforts toward generating deterministic packages, where users can verify that the source corresponds to the binaries provided by the distribution.

The problem of verifying software, particularly security-oriented software, is difficult, but also rather important. If we are to be able to keep our communications private in the face of extremely well-heeled adversaries, we will need to be able to verify that our encryption is truly working end to end. That, of course, leaves the endpoints potentially vulnerable, but that means the adversaries—governments, criminals, script kiddies, whoever—have to target each endpoint separately. That's a much harder job than just coercing (or attacking) a single service provider.