Ben Laurie blathering

23 Sep 2009


Filed under: Capabilities,Open Source,Programming,Security — Ben @ 13:13

In response to my not-so-recent rants on formal methods I was told to go and read up on seL4.

I’m glad I did, it’s really quite fascinating. To set the stage a little, L4 is a microkernel architecture with various implementations. Last time I looked it was mostly used by academics and was not very mature, but it seems to have moved on – for example, L4Linux is a version of it with Linux hosted on top, providing benefits like driver isolation.

seL4 is a variant of L4 that is based around a capability architecture (I confess I don’t know enough about L4 to understand how one variant can be capability-based without them all being, pointers welcome), which would be interesting in itself. But far more interesting than that – seL4 has been formally verified.

The approach is somewhat convoluted. First of all, they write a prototype of the kernel in Haskell, including all of the low-level hardware control (note that because this is a microkernel, this does not include most of the device drivers). This prototype is then linked to an emulator derived from QEMU, which allows user code to run in a binary compatible simulated environment. When user code calls the kernel, the emulator instead branches into the Haskell code, runs it, and then returns to the user code. This in itself would be pretty cool, but there’s more.

Next, there’s the abstract specification of the kernel. This describes the binary layout of arguments to system calls, the effect of each system call and of interrupts and traps (e.g. page faults), without describing the implementation. From the Haskell, they generate what they call an executable specification. This is done by an automatic translation from the subset of Haskell they use into a theorem proving language. They then prove that the executable specification is a refinement of the abstract specification. Which means, informally, that everything that is true of the abstract specification is also true of the executable specification. In other words, the executable specification implements what the abstract specification specifies.

However, we’re not there yet. The real kernel is written in C, by hand. This is required if you want a kernel that is appropriately optimised – automatic generation of C code from the Haskell would be possible, but unlikely to run fast. The C implementation is then verified by automatically translating it into the theorem proving language once more, and showing that this is a refinement of the executable specification. This automatic translation is another remarkable achievement, though they do not claim to be able to translate arbitrary C: it must be written to conform with some rules – for example, no passing addresses of local variables to functions. Clearly these rules are not too onerous: they manged to write a whole kernel that conformed to them.

Note that this does not rely on the correctness of the Haskell code! Since that is only used to generate the executable specification, which stands between the abstract specification and the C implementation, all we really care about is the correctness of the executable specification, which is proved. Although this strongly implies that the Haskell code is correct, it is in no way relied upon.

So, the end result of all this is a number of fun things.

  • Most importantly, a kernel written in C that has a formal proof of correctness.
  • A Haskell prototyping environment for the kernel (I guess I’d like this part even more if I could figure out how to learn Haskell without sitting next to a Haskell guru).
  • The tools needed to adopt this approach for other code.
  • A nice write-up of the whole thing.
  • Detailed costs for doing this kind of proof, and the costs of making changes. See the paper for more, but the big picture is the whole thing took 20 man-years, of which 9 were development of (presumably reusable) tools and 11 were the formal seL4 proof itself.

AES Explained

Filed under: Crypto,Open Source — Ben @ 10:27

AES in cartoon form – a really nice explanation. Example code to go with it, too.

14 Sep 2009

FreeBSD Chromium, Part 2

Filed under: Open Source,Programming — Ben @ 20:28

Over the weekend I got chromium building and linking on FreeBSD. It doesn’t run for long, but this seems like a major milestone! I also got commit and submitted the first round of patches, by the way.

However, I discovered in the process that I wasn’t building with debugging info. Now that I am, I can’t link on my FreeBSD machine, because ld runs out of RAM. If someone out there has a nice big (and fast would be nice, it takes a really long time to build) box that I could ssh or, even better, VNC or NX into, now’s the time to let me know! Mine is dying with a dataseg limit of 716800 – which I could increase, I guess, but its a pretty old box, so probably not by much before I get into thrashing…

Anyway, for anyone who wants to try, the primary patch is here:

There are a couple of other patches referenced there (for V8 and WebCore – they’re tiny so I hope I can push them upstream soon), and you still need to build as specified here.

3 Sep 2009

Why Open Is Better Than Proprietary?

Filed under: Open Source,Programming — Ben @ 12:46

First of all watch this fascinating TED talk by Dan Pink. Watch it all the way to the end: I promise it is worth it. Then consider this…

I’ve long argued that open source provides a clear economic benefit (and hence incentive). However, I’ve always had a bit of a nagging feeling that there’s more to it than that but have never been satisfied by sociologists’ lame attempts at explanations. Perhaps Dan Pink’s observations fill in that missing piece. Autonomy, mastery and purpose – open source development provides all three of these to developers, in copious quantities.

  • Autonomy: you choose what you work on, when you work on it, and how you work on it.
  • Mastery: putting all your work out there in public view gets you great feedback – and many studies have shown that people don’t improve without external feedback. Furthermore, seeing what other people have done is a fantastic learning resource.
  • Purpose: most open source projects have a purpose that goes beyond the mere development of the software – for example, Apache exists to serve up web pages better than anything else does – and the higher purpose is greater democratisation and freedom for everyone. not just the developers. OpenSSL exists to protect people from invasions of the privacy and theft of their data. It’s not just a geek toy, it’s critical infrastructure for the new world we are moving into.

It seems that economics is not the only thing that makes open source better.

1 Sep 2009

Kim Cameron Explains Why Hoarding Is Not Hoarding

Filed under: Crypto,Open Source,Open Standards,Privacy — Ben @ 14:13

I’ve been meaning for some time to point out that it’s been well over a year since Microsoft bought Credentica and still no sign of any chance for anyone to use it. Kim Cameron has just provided me with an appropriate opportunity.

Apparently the lack of action is because Microsoft need to get a head start on implementation. Because if they haven’t got it all implemented, they can’t figure out the appropriate weaseling on the licence to make sure they keep a hold of it while appearing to be open.

if you don’t know what your standards and implementations might look like, you can’t define the intellectual property requirements.

Surely the requirements are pretty simple, if your goal is to not hoard? You just let everyone use it however they want. But clearly this is not what Microsoft have in mind. They want it “freely” used on their terms. Not yours.

30 Aug 2009

Porting Chromium to FreeBSD

Filed under: Open Source,Programming — Ben @ 19:27

In my copious spare time, I’ve started work on a FreeBSD port of Chromium. So far it doesn’t even build, but I’ve identified a few problem areas people might like to pitch in on.

  • NSS port: the FreeBSD NSS port needs to be upgraded to at least NSS 3.12. Ideally to the latest version because it fixes some security holes.
  • Sound: mostly whatever Linux does it likely to be the right thing for FreeBSD, too, so much of the porting work at this stage is pretty mechanical. But sound isn’t – the Linux port uses ALSA, which FreeBSD has no truck with. I am informed that the right thing to use on FreeBSD is OSS. But someone needs to do that.
  • Build farm: building this sucker is slow. I wouldn’t mind having access to a nice big build farm.

So far none of the work has been committed, but I am optimistic that some will be soon. In the meantime, you’ll be needing some patches.

There’ll probably be another patch soon – I’m going through the rest of the code right now getting the parts that don’t need NSS or ALSA building.

In order to build this lot, you’ll need to configure like this:

cd src && GYP_GENERATORS=make python tools/gyp/gyp_chromium -D 'OS=freebsd' -D 'use_system_libxml=1' build/all.gyp

and build using gmake:

cd src && gmake chrome

Right now anything that fails on NSS or ALSA I’m just manually removing from the .mk files.

You’ll also need a bunch of ports installed, here’s what my notes currently say

Python >= 2.4       (lang/python24, lang/python25, lang/python26, lang/python30)
Perl >= 5.x         (lang/perl5.6, lang/perl5.8, lang/perl5.10)
gcc/g++ >= 4.2      (lang/gcc42, lang/gcc43, lang/gcc44, lang/gcc45)
g++-multilib >=4.2  (?)
bison >= 2.3        (devel/bison == 2.4.1)
flex >= 2.5.34      (base system: 2.5.4 - oops?)
gperf >= 3.0.3      (lang/gperf - NB: base system has /usr/bin/gperf == 2.7.2, port installs /usr/local/bin/gperf)
pkg-config >= 0.20  (devel/pkg-config == 0.23)
libnss3-dev >= 3.12 (security/nss == 3.11.9_2 - hand install?)
libgconf2-dev       (devel/gconf2)
libglib2.0-dev      (devel/glib20)
libgtk2.0-dev       (x11-toolkits/gtk20)
libnspr4-0d >= 4.7.1+1.9-0ubuntu0.8.04.5 (ubuntu0.8.04.1 causes duplicate dtoa references)   (devel/nspr?)
libnspr4-dev >= 4.7.1+1.9-0ubuntu0.8.04.5  (devel/nspr)
msttcorefonts (Microsoft fonts)
freetype-dev        (print/freetype)
libcairo2-dev       (no port!)
libdbus-1-dev       (devel/dbus)

Get in touch if you want to help. Or join the chromium-dev mailing list and pitch in.

7 Jul 2009

More Security Pie In The Sky

Filed under: Open Source,Security — Ben @ 12:39

The Institute for Public Policy Research have a report called “A national security strategy for the UK”. They want money for it, though, so you might prefer the executive summary, even if you aren’t an executive.

Recommendation 60: The Government should also approach the European Commission and the incoming Swedish Presidency to sponsor a programme for the creation of a range of secure and reliable standard software modules (such as simple operating systems, database management systems and graphical user interfaces). These modules should be developed using formal methods and be made available free of charge through an open source licence to encourage their widespread use.

I’m with them on a range of secure and reliable standard software modules. I’m with them on the free/open source front. I’m even mostly with them on their example modules, though I would say that a secure GUI is less of a software engineering problem and more of an HCI problem. But formal methods? We have essentially zero examples of useful systems that have been shown to be secure using formal methods, so why make this recommendation? Are these things written entirely by people looking for funding? Clearly they’re not written by people who want to solve the problem, or they’d make suggestions that might actually lead to a solution.

30 May 2009

Wave Trust Patterns

Filed under: Crypto,Open Source,Open Standards,Privacy,Security — Ben @ 6:04

Ben Adida says nice things about Google Wave. But I have to differ with

… follows the same trust patterns as email …

Wave most definitely does not follow the same trust patterns as email, that is something we have explicitly tried to improve upon, In particular, the crypto we use in the federation protocol ensures that the origin of all content is known and that the relaying server did not cheat by omitting or re-ordering messages.

I should note, before anyone gets excited about privacy, that the protocol is a server-to-server protocol and so does not identify you any more than your email address does. You have to trust your server not to lie to you, though – and that is similar to email. I run my own mail server. Just saying.

I should also note that, as always, this is my personal blog, not Google’s.

7 Apr 2009

CodeCon Is Back!

Filed under: General,Open Source,Programming — Ben @ 10:43

Unfortunately, I can’t be there, but the lineup looks great. The bio-hacking track looks particularly fun.

Not long to go now, less than two weeks. Sign up!

16 Jan 2009

Will GPLv3 Kill GPL?

Filed under: Open Source,Rants — Ben @ 14:49

I started looking at the LLVM project today, which is a replacement for the widely used gcc compiler for C and C++. My interest in this was prompted by thinking once more about static analysis, which it is pretty much impossible to use gcc for, and is likely to remain so, because Stallman opposes features which would enable it.

Anyway, being an optimist, I thought perhaps the interest in LLVM and clang (the C/C++ front end) were prompted by a sudden surge of interest in open source static analysis, but asking around, it seems it is not so.

The primary motivator appears to be GPLv3. Why? Well, here’s a few facts.

  • GPLv3 is not compatible with GPLv2. Don’t take my word for it, believe Richard.
  • Linux is, of course, famously GPLv2 without the upgrade clause, and hence GPLv3 incompatible.
  • FreeBSD, for example, are unlikely to accept software into the core that is GPLv3. No new licence can be used without core team approval and I am told this has not been given for GPLv3 and is not likely to be.
  • Commercial users of open source have always been a bit twitchy about GPLv2, but they’re very twitchy indeed about GPLv3. And don’t tell me commercial users are not important: these days they are the ones financing the development of open source software.

GCC is, apparently, going to move to GPLv3 – it says here that GCC 4.2.1 would be the last version released under GPLv2 (which is a bit rum, because I just checked GCC 4.4 and it is GPLv2. What gives?).

So, pretty clearly, there’s a need for a C/C++ compiler that is not GPLv3, and this, it would seem, is the real driver for LLVM.

Obviously this issue is not confined to GCC. As more software moves to GPLv3, what will the outcome be? Will the friction between GPL and other licences finally start persuading projects that free != GPL, and that BSD-style licences better suit their needs? Or will it just be that GPLv3 fails to make headway? We can only hope for the former outcome.

12 Jan 2009

Radio 4 on Open Source and Creative Commons

Filed under: Open Source — Ben @ 13:32

The Radio 4 programme “In Business” was all about free stuff and Creative Commons last night. Because of Auntie’s lameness, this link will presumably only work for a week.

Update: find the podcast here.

8 Jan 2009

OpenPGP:SDK V0.9 Released

Filed under: Crypto,Open Source — Ben @ 23:14

A long time ago my sometimes collaborator, Rachel Willmer, and I started work on a BSD-licensed OpenPGP library, sponsored by Nominet.

Things slowed down a bit when, shortly after getting the initial code done, I got hired by Google – that was a bit distracting. But Rachel has been plugging away ever since, with occasional interference from me. So, I’m pleased to announce that we’ve reached the point of a somewhat feature complete release, for some value of “feature complete”, OpenPGP:SDK V0.9.

Of course, its an open source project, so contributions and bug reports are welcome. More to the point, if anyone would rather use a library than shell out to gpg, I’d be happy to help them figure out how.

7 Jan 2009

Yet Another Serious Bug That’s Been Around Forever

Filed under: Crypto,Open Source,Programming,Rants,Security — Ben @ 17:13

Late last year the Google Security Team found a bug in OpenSSL that’s been there, well, forever. That is, nearly 10 years in OpenSSL and, I should think, for as long as SSLeay existed, too. This bug means that anyone can trivially fake DSA and ECDSA signatures, which is pretty damn serious. What’s even worse, numerous other packages copied (or independently invented) the same bug.

I’m not sure what to say about this, except to reiterate that it seems people just aren’t very good at writing or reviewing security-sensitive code. It seems to me that we need better static analysis tools to catch this kind of obvious error – and so I should bemoan, once more, that there’s really no-one working seriously on static analysis in the open source world, which is a great shame. I’ve even offered to pay real money to anyone (credible) that wants to work in this area, and still, nothing. The closed source tools aren’t that great, either – OpenSSL is using Coverity’s free-for-open-source service, and it gets a lot of false positives. And didn’t find this rather obvious (and, obviously staticly analysable) bug.

Oh, I should also say that we (that is, the OpenSSL Team) worked with oCERT for the first time on coordinating a response with other affected packages. It was a very easy and pleasant experience, I recommend them highly.

29 Oct 2008

Yahoo, Caja, OpenSocial

Filed under: Caja,Capabilities,Open Source,Programming,Security — Ben @ 13:01

I’m very excited that Yahoo! have launched their gadget platforms, including an OpenSocial platform. Why am I excited? Because Yahoo! require all gadgets to use Caja so that they can be sure the gadgets behave themselves without review. Caja allows the container (i.e. Yahoo!’s platform, in this case) to completely confine the untrusted Javascript (i.e. the gadget, in this case), only allowing it to perform “safe” operations. All other platforms either have to manually review gadgets or take the risk that the gadgets will do something evil to their users.

27 Oct 2008

J-PAKE Again

Filed under: Open Source,Security — Ben @ 15:15

When I wrote last week that I had implemented a J-PAKE demo someone rather churlishly commented, “not a demo till it runs on two machines, with a toy browser and toy server”.

So, this weekend I implemented J-PAKE as a proper OpenSSL module. Plus support in s_server and s_client. You can test it like this:

openssl s_server -jpake secret
openssl s_client -jpake secret

If you want to use two different machines, as required by Mr. Churlish, then you’ll need to use the -connect option to s_client.

If you want to use it yourself, you can find example code in apps/apps.c. Look for the functions jpake_client_auth() and jpake_server_auth().

24 Oct 2008

WTF Does Open Source Have To Do With Business Models?

Filed under: Open Source,Rants — Ben @ 14:52

Unless you are Red Hat, the answer is: about as much as eating lunch has to do with business models.

Whatever business you are in, you need your lunch, or you’re going to die. Likewise, but perhaps not quite so urgently, you need software. Open source is about getting the software you want for the minimum investment. It is cheaper and more efficient for those who need particular functionality to group together and provide it for themselves than it is to pay five different companies to not quite provide it in five different ways.

That’s all there is. End of.

So, when you read something like this: “Report: Pure Open Source No Longer a Viable Business Model”, what you are supposed to do is hit the keyboard violently and scream, “It never was, you morons! Get with the program!”

Selling support for software is a business model. Whether it is open source or not. That’s the business Red Hat is in. Not the “open source business”. There isn’t one.

19 Oct 2008


Filed under: Crypto,Open Source,Programming,Security — Ben @ 19:12

Just for fun, I wrote a demo implementation of J-PAKE in C, using OpenSSL for the crypto, of course. I’ve pushed it into the OpenSSL CVS tree; you can find it in demos/jpake. For your convenience, there’s also a copy here.

I’ve tried to write the code so the data structures reflect the way a real implementation would work, so there’s a structure representing what each end of the connection knows (JPakeUser), one for the zero-knowledge proofs (JPakeZKP) and one for each step of the protocol (JPakeStep1 and JPakeStep2). Normally there should be a third step, where each end proves knowledge of the shared key (for example, by Alice sending Bob H(H(K)) and Bob sending Alice H(K)), since differing secrets do not break any of the earlier steps, but because both ends are in the same code I just compare the resulting keys.

The code also implements the protocol steps in a modular way, except that communications happen by magic. This will get cleaned up when I implement J-PAKE as a proper OpenSSL library component.

The cryptographic implementation differs from the Java demo (which I used for inspiration) in a few ways. I think only one of them really matters: the calculation of the hash for the Schnorr signature used in the zero-knowledge proofs – the Java implementation simply concatenates a byte representation of the various parameters. This is a security flaw, as it can be subjected to a “moving goalposts” attack. That is, the attacker could use parameters that gave the same byte representation, but with different boundaries between the parameters. I avoid this attack by including a length before each parameter. Note that I do not claim this attack is feasible, but why gamble? It worked on PGP, after all.

The code and data structures are completely different, though. Also, because of the cryptographic difference, the two implementations would not interoperate.

13 Aug 2008


Filed under: Crypto,Open Source — Ben @ 11:21

When I joined Google over two years ago I was asked to find a small project to get used to the way development is done there. The project I chose was one that some colleagues had been thinking about, a key management library. I soon realised that unless the library also handled the crypto it was punting on the hard problem, so I extended it to do crypto and to handle key rotation and algorithm changes transparently to the user of the library.

About nine months later I handed over my “starter project” to Steve Weis, who has worked on it ever since. For a long time we’ve talked about releasing an open source version, and I’m pleased to say that Steve and intern Arkajit Dey did just that, earlier this week: Keyczar.

Keyczar is an open source cryptographic toolkit designed to make it easier and safer for developers to use cryptography in their applications. Keyczar supports authentication and encryption with both symmetric and asymmetric keys. Some features of Keyczar include:

  • A simple API
  • Key rotation and versioning
  • Safe default algorithms, modes, and key lengths
  • Automated generation of initialization vectors and ciphertext signatures

When we say simple, by the way, the code for loading a keyset and encrypting some plaintext is just two lines. Likewise for decryption. And the user doesn’t need to know anything about algorithms or modes.

Great work, guys! I look forward to the “real” version (C++, of course!).

24 Jul 2008

Open Web Foundation

Filed under: Open Source,Open Standards — Ben @ 18:41

I’m very pleased that we’ve launched the Open Web Foundation today. As Scott Kveton says

The OWF is an organization modeled after the Apache Software Foundation; we wanted to use a model that has been working and has stood the test of time.

When we started the ASF, we wanted to create the best possible place for open source developers to come and share their work. As time went by, it became apparent that the code wasn’t the only problem – standards were, too. The ASF board (and members, I’m sure) debated the subject several times whilst I was serving on it, and no doubt still does, but we always decided that we should focus on a problem we knew we could solve.

So, I’m extra-happy that finally a group of community-minded volunteers have come together to try to do the same thing for standards.

24 Jun 2008

Information Card Foundation Launched

Yet another industry alliance launches today: the Information Card Foundation (yes, I know that’s currently a holding page: as always, the Americans think June 24th starts when they wake up).

I have agreed to be a “Community Steering Member”, which means I sit on the board and get a vote on what the ICF does. Weirdly, I am also representing Google on the ICF board. I guess I brought that on myself.

I am not super-happy with the ICF’s IPR policy, though it is slightly better than the OpenID Foundation’s. I had hoped to get that fixed before launch, but there’s only so many legal reviews the various founders could put up with at short notice, so I will have to continue to tinker post-launch.

It is also far from clear how sincere Microsoft are about all this. Will they behave, or will they be up to their usual shenanigans? We shall see (though the adoption of a fantastically weak IPR policy is not the best of starts)! And on that note, I still wait for any sign of movement at all on the technology Microsoft acquired from Credentica – which they have kinda, sorta, maybe committed to making generally available. This is key, IMO, to the next generation of identity management systems and will only flourish if people can freely experiment with it. So what are they waiting for?

(More news reports than you can shake a stick at.)

« Previous PageNext Page »

Powered by WordPress