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.

Powered by WordPress