About Security: Singularity vs L4, Part 2

In a recent blog I compared Singularity with L4, explaining the fundamental difference in the two approaches and showed that L4 had a significant performance advantage. I promised a follow-up posting focussing on security, particularly as it related to the embedded-systems context.

Singularity is written in a modern, type-safe language (Sing#), while OKL4 is written in type-unsafe C and assembler. This means that many classical implementation bugs are prevented in Singularity by language rules (enforced by the compiler) while there is no such protection for the OKL4 implementation (although static-analysis tools, such as Goanna, can make up for much of this difference). More importantly, code written in Sing# is readily amenable to formal verification, due to the well-defined semantics and coding restrictions enforced by the language.

So, this should mean that it is relatively easy to formally verify (prove) the implementation correctness of Singularity, much easier than in OKL4, and as such, Singularity should be a superior platform (trusted computing base) for safety- and security-critical systems. Right?

Wrong.

The above argument ignores one important fact: Singularity isn’t all written in Sing#. Why not?

For one, every OS kernel requires code that is inherently type-unsafe. You can’t avoid pointer arithmetic in the kernel, you can’t avoid raw byte copies (for message passing, saving context etc), you can’t avoid jump tables (for exception vectors). These are inherently unsafe operations that cannot be expressed in a type-safe language. Hence, Singularity is also forced to use low-level code written in C, assembler or something similar.

But what they really forget to tell you is that, Sing#, as a managed language, needs significant run-time support. This isn’t just all the usual libraries, some of which probably require type-unsafe implementations for performance. It also includes the garbage collector. A big, ugly piece of tricky, unsafe code. And you can be sure it’s big. Certainly compared to OKL4.

Galen Hunt, the leader of the Singularity project, in private conversation freely admitted to me that “the amount of dirty code in Singularity is probably larger than all of L4”. (Where “probably” is an understatement, my estimate is that the garbage collector itself is several times OKL4’s code size.)

So, while formally verifying the Sing# implementation might not be all that difficult, verifying the dirty bits certainly is a much bigger job than verifying the complete OKL4 kernel. This is why you won’t be seeing a fully formally-verified Singularity any time soon. But you will see a fully formally-verified L4 kernel this year, and the commercial OKL4 version soon after.

The implication for security, safety and reliability should be obvious. A fully-verified kernel (i.e. OKL4) will provide a truly trustworthy foundation on which to build highly safe and secure system. Singularity can’t do this in the foreseeable future.