Skip to content

OK Labs Story (1): The Beginning

Last week I promised a bit of history on Open Kernel Labs. Here is the first installment.

It all started more than ten years ago, when one morning I got a call from Kevin, identifying himself as an IP lawyer for Qualcomm. Knowing their litigious nature, this would normally send shivers down your spine. However, the conversation was all friendly, he wanted to know details of the IP status of our L4 microkernel (Pistachio-embedded) which we had open-sourced under a BSD license (the release of June’08 is still around). This was our fork of the Pistachio kernel from Karlsruhe, which we had earlier ported to several architectures, including ARM. What was special about this fork was that it was optimised for use in resource-constrained embedded systems.

When I went into the lab after the call to tell my students, Harvey immediately drew a connection to a guy called Eric who, using a yahoo address, had been asking very detailled technical questions on the mailing list.

This phone call was in May 2004, and Qualcomm was clearly interested in our kernel. I was going to the US anyway a couple weeks later, and in early June I visited them in San Diego, with an NDA in place (expired a long time ago). I spent a few hours in fairly intense technical discussions with a vice president and a senior engineer (Eric), and the upshot was that I was back in early August, together with my student Benno, to deliver a three-day course in L4 design, philosophy and use (paid at consulting rates, including business-class flight). The audience were a dozen or so engineers from Qualcomm, plus some from customers.

The course went well, and by September we had a contract to deliver consulting services to help Qualcomm engineers do prototype development. Initially this work was done by Benno and Carl, but expanded over time to about six full-time staff. Only half a year later, in about February 2005, and unknown to us for quite a while, Qualcomm decided to move L4 into production, as the kernel underneath their modem firmware and BREW operating system. The first phones running L4 (the Toshiba W47T) started shipping in Japan in the second half of 2006.

The technical reasons behind all this we only understood over time. It turns out that Qualcomm at the time had two problems. One was the flat-address-space design of their modem stack and tightly integrated BREW operating system. This had grown to millions of lines of code, and debugging such a beast without memory protection is a nightmare. This is obviously made worse by the proliferation of applications at that (pre-smartphone) time. And it was obviously not possible to support an open environment (with arbitrary third-party apps) in that way. There was also a desire to modularise the modem stack.

Qualcomm’s Plan A was to retrofit protection into REX, their home-grown RTOS. Some people foresaw this effort to fail, and were looking for a Plan B. (Apparently we were Plan B.2, I never found out what B.1 was.) The failure must have been spectacular, given the amazingly fast transition from evaluation to deployment of L4 (although Eric had clearly done a fair bit of prototyping before they approached us).

There was a second driver: Motorola had made a strategic move to Linux as their phone OS, Linux-based Motorola handsets were already shipping in China. They wanted to use Qualcomm chips in Linux handsets. Qualcomm in turn did not want Linux (or any GPL software) anywhere near their core IP. In order to sell to Motorola they needed a way to IP-wise isolate their IP from Linux. In short, they were looking for a virtulisation solution, which we sort-of had, in the form of an early-day Linux running on our L4 kernel. They had looked at various candidates satisfying their requirements, which were

  1. supports virtualised Linux,
  2. has the ability to run their modem stack efficiently, and
  3. runs on ARM processors.

They found that what we had came closest, despite no-one (including us!) claiming that what we had was production quality. So they basically contracted us to get it there, and my students did exactly that.

Ironically, the virtualised Linux didn’t make much of an impact. There were endless delays at Motorola’s side, partially due to internal politics, as well as doubts (from outside the group working with L4) that it could deliver the required performance. This scepticism, although unjustified, is somewhat understandable. The ARM9 cores used at the time (based on the ARMv5 architecture) have virtually-indexed, virtually-tagged caches. This means that the hardware cannot distinguish between data belonging to different address spaces, and consequently Linux (as well as other OSes, such as Windows CE) flushed the cache on every context switch. As in the virtualised setup Linux runs in its own address space, invoking a Linux system call requires a context switch (and another one when returning from the system call). Even on native Linux, caches get flushed very often, and Linux performance was bad, and one would reasonably assume that virtualisation would make this worse.

In fact, it was the other way round: on ARM9 processors, Linux ran faster virtualised on L4 than native! This was due to a rather nifty use of hardware features that allowed us to make context switches really fast on L4 (up to 50 times faster!) We had actually published this “fast address-space switch” (FASS) trick, yet none of our competitors picked it up, it seems to have exceeded their abilities (not surprising given what we found out about the competition over time, but I’ll leave this for another time). And our original implementation of FASS had been in Linux, and we had offered it upstream, but the maintainers rejected it as too complex. What’s a factor 50 between friends?

The dedicated Motorola engineers working on L4 eventually got an ARM9-based, virtualised Linux-on-L4 phone out into the market (the Motorola Evoke). I used it, and it was definitely snappy and nice to use, with seamless integration of Linux- and BREW-based apps. Much faster than the painfully slow HTC TyTN-II, which had a much more powerful ARM11 processor running Windows Mobile. But it was too late. By that time, smartphones required much more grunt than such a low-end processor could deliver (even without virtualisation and sharing the processor with the modem), so the trend went to separate, powerful applications processors. The era of “consolidated” phones, running an application OS concurrently with a real-time OS (to support the modem stack) on the same processor was stillborn.

RIP Open Kernel Labs, Welcome Cog Systems

This month marks the second anniversary of the acquisition of Open Kernel Labs (OK Labs) by General Dynamics (GD). It also marks ten years of us engaging with Qualcomm on commercialising L4 microkernel technology, and eight years since OK Labs was founded. Clearly an occasion to reflect.

In the two years since its acquisition, OK Labs has, in a way, died, and was, in a way, reborn. Specifically, in February of this year, GD closed down the former OK Labs engineering office in Sydney. But rather than this being the end of the L4-based business, it was a new beginning. The core engineers (mostly my former students) created a new, fully Australian-owned company, called Cog Systems.

Cog is continuing OK Labs’ mission of bringing L4 microkernel technology to the world. They have a reseller license that allows them to market the OKL4 Microvisor, which was the main product of OK Labs. And they added their own IP that complements it. They also partner with GD to service pre-existing contracts for OKL4 deployments. In that sense they are really OK Labs reborn.

I think this is a great outcome. We now have a local company who are experts in L4 technology, and are highly skilled and innovative. They will continue to be a great partner not only for GD, but for us in NICTA too, as they will be able to work with us on delivering seL4-based solutions to customers.

The existence of Cog is one reason I’m confidently talking to potential seL4 customers who would use engineering support to build their critical systems. It’s also a step towards creating a critical-system ecosystem in Sydney. I’m very much looking forward to working with them in the future!

I will over the next few weeks reflect on how we got here over the last then years, in particular the history of OK Labs. Stay tuned.

PS: Neither NICTA nor I hold shares in Cog, nor do we have any other interest in the company, other than our general desire to support the Australian high-tech industry. We’re dealing with Cog at arm’s length.

seL4 is finally free! Can you afford not to use it?

The world’s most highly assured operating system (OS) kernel

… the only one with a formal proof of implementation correctness (freedom from bugs), the only one with a proof of security that extends all the way to the executable code, the only protected-mode OS with sound worst-case execution time (WCET) bounds, is finally free. It is available under the same license as the Linux kernel, the GPL v2. Everyone can use it, and everyone should. And, as I’ll explain, they may, one day, be considered negligent for not using seL4, and such liability could reasonably start with any system that is designed from now on.

Critical systems

Let’s expand on this a little. Let’s assume you, or our company, is building a device/system whatever which has safety or security requirement. There are lots of these, where failure could lead to death or injury, loss of privacy, or loss of money. Many systems that are part of everyday life fall into that category, not only national-security type of systems (but those obviously do too).

Medical implants

Medical implants could kill a patient or fail to keep them alive if they fail. Such systems may fail because their critical functionality (that keeps the patient alive) is compromised by a “non-critical” part that misbehaves (either by a bug triggered during normal operation, or a vulnerability exploited by an attacker). Most implants have such “non-critical” code, in fact, it tends to be the vast majority of the software on the device. Most devices these days have some wireless communication capability, used for monitoring the patient, the state of the device, and maybe even to allow the physician to adjust its operation. On systems not built on seL4, there can be no guarantee that this “non-critical” software is free from dangerous faults, nor can there be a guarantee that its failure cannot cause the critical bits to fail.

Cars

Complex software in a car could misbehave and compromise critical components like engine control, breaks, air bags. Attacks on cars are well documented. The CAN networks in cars are fundamentally vulnerable, so many of the devices on the bus can be the starting point of an attack. Furthermore, functionalities that used to run on separate ECUs (microprocessors) are increasingly consolidated onto shared processors, creating more potential vulnerabilities. Car hacks clearly have the potential to kill people.

Industrial automation

Industrial automation systems are in many ways – other than scale ;-) – similar to medical implants: Some critical functionality (which may or may not be small but is likely to be highly assured) runs beside large, complex software stacks that supports monitoring, control, reprogramming etc, and is far too complex for high assurance to be feasible. If such a system misbehaves it may cause millions of dollars worth of damage, or even endanger lives.

Others

There are many other systems where failure is expensive or dangerous. They include systems performing financial transactions (eg point-of-sale systems or ATMs), voting machines, systems holding or providing access to personal data (cards with medical history, etc).

There are many more examples.

Limitations

Of course, seL4 cannot give a complete guarantee of no failure either. The hardware could fail, the system could be ill-designed or wrongly configured, or few other things could go wrong. But it definitely (for a well-designed and -configured system) makes it impossible for a compromised “non-critical” subsystem to interfere, through a software fault, with the critical part. This is by far the most likely source of error, and seL4 gives you the highest degree of certainty achievable to date that this won’t happen.

So, why would you not want to use seL4 in your next design?

Let’s examine the reasons people usually give.

License

seL4 is published under the GPLv2. This means that any improvements will have to be open-sourced as well, which is a concern to some people.

I claim this is mostly a misconception. Nothing you build on top of seL4 will be affected by the kernel’s license (just as you can build closed-source stuff on Linux). seL4 contains the GPL to the kernel, and our license files have explicit wording (taken from Linux) confirming that.

How about changes to seL4 itself? Reality is that you aren’t likely to make significant changes to seL4. For one, any change will invalidate the proofs. Ok, maybe you don’t care too much about this, as even if it’s not 100% verified, even a slightly modified seL4 system will be massively more dependable than anything else. So maybe you want to do some “improvements” and then keep them to yourself?

As long as those are actual “improvements”, I suspect that you won’t be able to outrun the momentum that’s behind seL4 at present. No-one knows better than us how to improve seL4 even more (despite it already being much better than any comparable system), and we keep doing this. And if you have a real use case that requires some improvements, you’re better off talking to us than to try on your own.

Or maybe your improvements are really adaptations to proprietary hardware. In most cases that will be a non-issue, as seL4 contains no device drivers (other than a timer and the interrupt-controller driver), so any proprietary stuff isn’t likely to be visible to the kernel. But if you really have to modify the kernel in a way that exposes sensitive IP, then you can always get access under a different license (for a fee). If this is your situation then talk to us.

Processor architecture

Maybe you want to run seL4 on a processor that isn’t presently supported. As long as it’s a supported CPU architecture (ARM and x86) then that isn’t a big deal, and we can help you porting. If you need it on a different architecture (say Power) then that would involve a fair bit more work. Still, you should talk to us about a port, the cost is likely to be a small fraction of your overall project cost, and will be tiny compared to the potential cost of not using seL4 (more on that below).

Performance

I thought our work in the past 20 years was enough to debunk the “microkernels are slow” or even “protection is too expensive” nonsense. Ok, some microkernels are slow, and, in fact, almost all commercial ones are, especially the so-called high-assurance ones (OKL4 is an exception). But seL4 isn’t. It runs loops around all the crap out there! And OKL4, shipped in billions of power-sensitive mobile devices, has shown that a fast microkernel doesn’t cause a performance problem. Performance is definitely one of the more stupid excuses for not using seL4!

Resource usage

Unless you have an extremely constrained system, then seL4 is small (compared to just about everything else). If you’re running on a low-end microcontroller (with not only serious resource constrains but also no memory protection) you should look at our eChronos system instead.

Legacy

Your design has to re-use a lot of legacy software that is dependent on your old OS environment. Whether that’s a real argument probably depends a lot on how well your legacy software is written. If it is essentially unstructured homebrew that doesn’t abstract common functionality into libraries, then you may have a real problem. In the sense of having a real problem, which is going to bite you hard sooner or later, whether you’re migrating to seL4 or not. If that isn’t the case, then there is likely to be a sensible migration path, the cost of which is likely to be dwarfed by the potential cost of not using seL4 (see below).

Environment and support

seL4 is a young system, with a limited support environment in terms of libraries and tools. That is true, but it’s also changing rapidly. We’ll see userland developing quickly. And don’t you think that just because it’s open source there isn’t good support. Between NICTA and GD and our partners, we can certainly provide highly professional support for your seL4-based development. Just talk to us.

So, what’s the trade-off?

Well, ask yourself: You’re developing some critical system. Critical in the sense that failure will be very costly, in terms of lost business, lost privacy, loss of life or limb. Imagine you’re developing this based on yesterday’s technology, the sort of stuff others are trying to sell you, and what you may have been using believing (at the time at least) that it was state of the art. Now it ain’t.

So, imagine you are developing this critical system and decide not to use seL4. And, sooner or late, it fails, with the above costly consequences. You may find yourself in court, being sued for many millions, trying to explain why you developed your critical system using yesterday’s technology, rather than the state of the art. I wouldn’t want to be in your shoes. In fact, I might serve as an expert witness to the other side, which argues that you should have known, and that doing what you did was reckless.

Do you want to run that risk? For what benefit?

Think carefully.

Clarification on seL4 media reports

The open-sourcing of seL4 has created a bit of media coverage, generally very positive, good to see.

Some of it, however, is inaccurate and potentially misleading. I’ve commented where I could, but some sites don’t allow comments.

One frequent error is the (explicit or implicit) claim that seL4 was developed for or under the DARPA HACMS program, stated eg at Security Affairs, and seemingly originated at The Register. This is incorrect: seL4 pre-dates HACMS by several years, and was, in fact, a main motivation for HACMS. We are a “performer” under this project, and, together with our partners, are building an seL4-based high-assurance software stack for a drone, please see the SMACCM Project page for details. [Note 31/7/14: The Register has now corrected their article.]

LinuxPro states that DARPA and NICTA released the software, the release was by General Dynamics (who own seL4) and NICTA. Also, seL4 wasn’t developed for drones, it’s designed as a general-purpose platform suitable for all sorts of security- and safety-critical systems. I for one would like to see it making pacemakers secure, I may need one eventually and with present technology would feel rather uncomfortable about this.

I’ll keep adding if I find more…

Sense and Nonsense of Conference Rankings

The CORE Rankings

Some may know that a few years ago, the Australian Research Council (ARC) had a ranking of publication outlets produced. For computer science, the exercise was outsourced to CORE, the association of Australian and NZ CS departments (Oz equivalent of CRA). It categorised conferences (and journals) into A*, A, B and C venues.

I have in the past stated what I think of that list: very little. In short, I think it’s highly compromised and an embarrassment for Australian computer science. And I’m outright appalled when I see that other countries are adopting the “CORE Rankings”!

The ARC disendorsed the rankings in 2011. Yet, in 2013, CORE decided to maintain and update it. I argued that updating with a similar process as the original one will not improve the list.

The Fellows Letter

Now, some senior colleagues (Fellows of the Australian Academy of Science) have written an open letter, denouncing not only the CORE list, but basically any use of publication venues as an indicator of research quality.

The letter was, apparently, written by Prof Bob Williamson from the ANU, and fellow group leader at NICTA. Bob is a guy I have a lot of respect for, and we rarely disagree. Here we do completely. I also highly respect the other Fellows (one of them is my boss).

The Fellows essentially argue (with more clarification by Bob) that looking at where a person has published is useless, and the right way to judge a researcher’s work is to read their papers.

What I think

With all respect, I think this is just plain nonsense:

  1. These rankings exist, like it or not. In fact, we all use them all the time. (Ok, I cannot prove that the “all” bit is strictly true, some, like Bob, may not, the rest of us do.) When I look at a CV, the first thing I look for is where did they publish. And I claim that is what most people do. And I claim it makes sense.

    Fact is that we know what the “good” venues are in our respective disciplines. This is where we send our papers to, this is where we tell our students and ECRs they need to get their papers accepted. They are the yardsticks of the community, like it or not, it is where you publish to have impact. Publishing in the right venues leads to high citations, publishing in the wrong ones doesn’t.

    Of course, we really only understand the venues in our own sub-disciplines, and may be a few neighbouring ones. So, collecting and documenting these top venues across all of CS isn’t a bad thing, it creates clarity.

  2. The idea that someone can judge a person’s work simply by reading some of their papers (even the self-selected best ones), with respect, borders on arrogance. In effect, what this is saying is that someone from a different sub-discipline can judge what is good/significant/relevant work!

    If this was true, then we as a community could reduce our workload drastically: We’d stop having conference PCs where everyone has to read 30 papers, and every paper gets at least half a dozen reviews before being accepted (as at OSDI, where I’m presently struggling to get all my reviews done). Instead, every conference would simply convene a handful of Bobs, divide the submissions between them, and each decides which one of their share of the papers should be accepted.

    Of course, things don’t work like this, for good reasons. I’ve served on enough top-tier conference PCs to have experienced plenty of cases where the reviews of discipline experts diverge drastically on multiple papers. In my present OSDI stack of 29 papers this is true for about 35% of papers: 10 papers have at least one clear reject and one clear accept! And it is the reason why each paper gets at least 6 reviews: we get the full spectrum, and then at the PC meeting work out who’s right and who’s wrong. The result is still imperfect, but vastly superior to relying on a simple opinion.

    Now these reviewers are the discipline experts (in this case, leading researchers in “systems”, incorporating mostly operating systems and distributed systems). If you get such a diversity of opinions within such a relatively narrow subdiscipline, how much would you get across all of computer science? I certainly would not claim to be able to judge the quality of a paper in 80% of computer science, and someone thinks they can, then my respect for them is taking a serious hit.

    In summary, I think the idea that someone, even one of the brightest computer scientists, can judge an arbitrary CS paper for its significance is simply indefensible. An expert PC of a top conference accepting a paper has far more significance than the opinion of a discipline outsider, even a bright one!

  3. Of course, that doesn’t justify using the publication outlets as the only criterion for promotion/hiring or anything else. That’s why we do interviews, request letters etc. Also, I definitely believe that citations are a better metric (still imperfect). But citations are a useless measure for fresh PhDs, and mostly of not much use for ECRs.

  4. Nor do I want to defend the present CORE list in any way. I said that before, but I’m repeating for completeness: the present CORE list is the result of an utterly broken process, is completely compromised, and an embarrassment for Australian computer science. And any attempt to fix it by using the existing process (or some minor variant of it) is not going to fix this. The list must either be abandoned or re-done from scratch, using a sound, robust and transparent process.

  5. My arguments only are about top venues. A track record of publishing in those means something, and identifying across all of CS what those top venues are has a value. By the same token I believe trying to categorise further (i.e. B- and C-grade venues, as done in the CORE list) is a complete waste of time. Publishing in such venues means nothing (other than positively establishing that someone has low standards). So, if we bother to have a list, it should only be a list of discipline top venues, nothing more.

Closing the gap: Real OS security finally in reach!

A few years ago we formally verified our seL4 microkernel down to C code. That proof, unprecedented and powerful as it is, didn’t actually establish the security (or safety) of seL4. But the latest achievement of NICTA’s Trustworthy Systems team actually do provide a proof of security.

What the original seL4 verification achieved was a proof that the kernel’s C code correctly implements its specification. The specification is a formal (mathematical) model of the kernel, and the proof showed that the C implementation is “correct”, in the sense that all possible behaviours, according to a semantics of C, are allowed by the spec.

This is both very powerful and limited. It’s powerful in the sense that it completely rules out any programming errors (aka bugs). It’s still limited in three important respects:

  1. Ok, the code adheres to the spec, but who say’s the spec is any good? How do you know it’s “right”, i.e. does what you expect it to, is it “secure” in any real sense?
  2. The C standard is not a formal specification, and is, in fact, ambiguous in many places. In order to conduct the proof, we had to pick a subset which is unambiguous, and we proved that our kernel implementation stays within that subset. However, we have no guarantee that the compiler, even on our subset, assumes the same semantics!
  3. Everyone knows compilers are buggy. So, even if we agree with the compiler about the semantics of our C subset, we can still lose if the compiler produces incorrect code.

Two sets of recent results remove these limitations. One set of work addresses the first limitation, and another the remaining two.

Integrity and confidentiality proofs

What does it mean for the kernel spec to be “good”? It means that the kernel can be used to build the kind of systems we want to build, with the right properties. The specific properties we are after are the classical security properties: Integrity, confidentiality and availability. (For safety a further property is required, timeliness. seL4 has this too, but I’ll discuss this another time.)

Availability is actually a non-issue in seL4: the kernel’s approach to resource management is not to do any, but to leave it to user-level code. The exact model is beyond the level of technicality of this blog, I refer the interested reader to the paper describing the general idea. The upshot is that denial of kernel services is impossible by construction. (This does not mean that availability is necessarily easy to enforce in seL4-based systems, only that you can’t DOS the kernel, or a userland partition segregated by correct use of kernel mechanisms.)

Integrity, at the level of the microkernel, means that the kernel will never allow you to perform a store (write) operation to a piece of memory for which you haven’t been explicitly been given write privilege; including when the kernel acts on behalf of user code. The NICTA team proved this safety property for seL4 about two years ago (see the integrity paper for details). In a nutshell, the proof shows that whenever the kernel operates, it will only write to memory if it has been provided with a write “capability” to the respective memory region, and it will only make a region accessible for writing by user-code (eg by mapping it into an address space) if provided with a write capability.

confidConfidentiality is the dual to integrity: it’s about read accesses. The figure at the left illustrates this, by showing allowed (black) and forbidden (red) read accesses. However, it turns out that confidentiality is harder to prove than integrity, for two reasons. 1) violation of confidentiality is unobservable in the state of the entity whose confidentiality has been violated 2) confidentiality can be violated not only by explicit reads (loads or instruction fetches) but also by side channels, which leak information by means outside the system’s protection model.

A NICTA team led by researcher Toby Murray has just recently succeeded in proving that seL4 protects confidentiality. They did this by proving what is called “non-interference”. The details are highly technical, but the basic idea is as follows: Assume there is a process A in the system, which holds a secret X. Then they look at any arbitrary execution traces of an arbitrary second process B. If the initial state of the system of any two such traces is identical except for the value of X, they proved that the two traces must be indistinguishable to B. This implies that B cannot infer X, and thus A’s confidentiality is maintained. The technical paper on this work will be presented at next month’s IEEE “Oakland” security conference.

Binary verification

In order to remove from our trusted computing base the C compiler, as well as our assumptions on the exact semantics of C, the team proved that the kernel binary (i.e., the output of the compilation and linking process) is consistent with the formal model of the kernel implementation. This formal model is actually what had earlier been proved to be correct with respect to the kernel spec (it had been obtained by formalising the C code using the formal C semantics). By verifying the binary against the formal model, the formalisation process (and thus our assumptions on the C semantics) are taken out of the trusted computing base.

Binary verification workflow and proof chain

Binary verification workflow and proof chain

The verification of the binary went in multiple phases, as indicated by the figure on the right. First, the binary was formalised. This was done with the help of a formal model of the ARMv6/v7 architecture. That formalisation of the architecture had previously been done at Cambridge University, in close collaboration with ARM, and is extensively validated. It’s considered to be the best and most dependable formalisation of any main-stream processor.

The formalised binary, which is now a complex expression in mathematical logic inside the theorem prover HOL4, was then “de-compiled” into a more high-level functional form (the left box called “function code” in the figure). This translation is completely done in the theorem prover, and proved correct. Similarly, the formal kernel model is transformed, using a set of “rewrite rules” which perform a similar operation as the compiler does, into a functional form at a similar abstraction level as the output of the above de-compilation. Again, this operation is done in the theorem prover, by application of mathematical logic, and is proved to be correct.

We now have two similar representations of the code, one obtained by de-compilation of the binary, the other by a partial compilation process of the formalised C. What is left is to show their equivalence. Readers with a CS background will now say “but that’s equivalent to the halting problem, and therefore impossible!” In fact, showing the equivalence of two arbitrary programs is impossible. However, we aren’t dealing with two arbitrary programs, but with two different representations of the same program (modulo compiler bugs and semantics mismatch). The operations performed by a compiler are well-understood, and the re-writing attempts to retrace them. As long as the compiler doesn’t change the logic too much (which it might do at high optimisation levels) there is hope we can show the equivalence.

And indeed, it worked. The approach chosen by Tom Sewell, the PhD student who did most of the work, was to compare the two programs chunk-by-chunk. For each chunk he used essentially a brute-force approach, by letting an SMT solver loose on it. Again, some trickery was needed, especially to deal with compiler optimisations of  loops, but in the end, Tom succeeded. Details will be presented at the PLDI conference in June.

The resulting tool is fairly general, in that it is not in any way specific to seL4 code, although it has limitations which are ok for seL4 but might be show-stoppers for other code. Specifically, the tools can’t deal with nested loops (but seL4 doesn’t have any, nor should any microkernel!) At present, the tools grok the complete seL4 binary when compiled by gcc with the -O1 optimisation flag. We normally compile the kernel with -O2, and this introduces a few optimisations which presently defeat the tool, but we’re hopeful this will be fixed too.

This is actually quite a significant result. You may have heard of Ken Thompson’s famous Turing Award Lecture “Reflections on trusting trust“, where he describes how to hack a compiler so it will automatically build a back door into the OS. With this tool, seL4 is no longer susceptible to this hack! If the compiler had built in a back door, the tool would fail to verify the correctness of the binary. But regular compiler bugs would be found as well, of course.

Where are we now?

proof-chainWe now have: 1) Proofs that our abstract kernel spec provides integrity and confidentiality; 2) A proof that the formalised C code is a correct implementation of the kernel spec; and 3) a proof that the kernel binary is a correct translation of the formalised C code. Together this means that we have a proof that the kernel binary has the right security properties of enforcing confidentiality and integrity!

There are still some limitations, though. For example, we haven’t yet verified the kernel’s initialisation (boot-strap) code, this is work in progress (and is nearing completion). There are also bits of unverified assembler code in the kernel, and we don’t yet model the operation of the MMU in detail. So there are still some corners in which bugs could, in theory, be hiding, but we’re getting closer to sweeping out the last refuges of potential bugs.

A more fundamental issue regards the side channels mentioned above. These are traditionally classified into two categories: storage channels and timing channels. The difference is essentially whether a common notion of time is required to exploit them.

In principle our non-interference proof covers storage channels, up to the point to which hardware state that could constitute a channel is exposed in the hardware model that is used in the proof. Presently that model is fairly high-level, and therefore might hide potential storage channels. It does cover things like general-purpose CPU registers, so we know that the kernel doesn’t forget to scrub those in a context switch, but modern CPUs have more complex state that could potentially create a channel. Nevertheless, the approach can be adapted to an arbitrarily-detailled model of the hardware, which would indeed eliminate all storage channels.

Timing channels are a different matter. The general consensus is that it is impossible to close all timing channels, so people focus on limiting their bandwidth. So far our proofs have no concept of time, and therefore cannot cover timing channels. However, we do have some promising research in that area. I’ll talk about that another time.

When “persistent” storage isn’t

A couple of weeks ago we published our RapiLog paper. It describes how to leverage formal verification to perform logically synchronous disk writes at the performance of asynchronous I/O (see the previous blog on the implications of this work).

A frequent comment from reviewers of the paper was: “why don’t you just use an SSD and get better performance without any extra work?”

My answer generally was “SSDs are more expensive [in terms of $/GiB], and that’s not going to change any time soon.” In fact, the RapiLog paper shows that we match SSD performance using normal disks.

What I didn’t actually know at the time is that, unlike disks, SSDs tend to be really crappy as “persistent” storage media. A paper by Zheng et al. that appeared at the Usenix FAST conference in February studies the behaviour of a wide range of different SSDs when electrical power is cut – exactly the scenario we cover with RapiLog. They find that of the 15 different SSD models tested, 13 exhibit data loss or corruption when power is lost! In other words: SSDs are a highly unreliable storage medium when there is a chance of power loss. They also tested normal disks, and found out that cheap disks aren’t completely reliable either.

They did their best to stress their storage devices, by using concurrent random writes. In RapiLog, we ensure that writes are almost completely sequential, which helps to de-stress the media. And, of course, we give the device enough time to write its data before the power goes.

I quote from the summary of Zheng et al.: “We recommend system builders either not use SSDs for im- portant information that needs to be durable or that they test their actual SSD models carefully under actual power failures beforehand. Failure to do so risks massive data loss.”

For me, the take-away is that putting the database log on an SSD undermines durability just as running the database on a normal disk in unsafe mode (asynchronous logging or write cache enabled). In contrast, using RapiLog with a normal disk gives you the performance of an SSD with the durability of a normal disk. Why would you want to use anything else?

Follow

Get every new post delivered to your Inbox.