Guest post by “National ICT Australia, in conjunction with Open Kernel Labs, has released new software aimed at researchers, developers and manufacturers that has the ability to protect computer hardware from failure or being attacked. The seL4 microkernel is a small operating system kernel which regulates access to a computer’s hardware and is able to distinguish between trusted and untrusted software.”
Hi,
If you start with a potentially broken and buggy specification that has large gaping security holes and plenty of design flaws; and then mathematically prove that an implementation does implement this specification 100% correctly; then what have you gained?
Mathematical proofs aren’t a guarantee that anything actually works as intended.
– Brendan
Well first sometimes specifications are much easier to read than implementations: for example the specification of a square root function is very easy (
abs(f(x)*f(x) – x) < epsilon) whereas the implementations are usually hard to read, so if you have a formal proof of this specification, it’s interesting.
Secondly even if the complete specifications of say a spreadsheet are probably as complex as the implementation is, this doesn’t mean that some partial specifications cannot be interesting.
For any program you have, wouldn’t you be interested if you could proove that:
no infinite loops, no integer overflow, no array overflow ?
I’m not saying that they can proove these properties, I’m just pointing out that you don’t need to specify everything to be interesting.
Abstracting details away is always a good idea, esp. if you can abstract in a very intuitive but still accurate way or if you do it very formally and can then use that to derive other properties.
What I’m really missing in those OKL releases is a userspace. seL4 is very nice work, but for now they completely blend out most of the really important problems in OS security.
What is really needed are security architectures/concepts for building a scalable software stack. We’ve got enough microkernels by now. For example, Genode has an architecture document describing a ‘Bastille’ security infrastructure. It is rather basic but seems like a very scalable security concept. Ideas of CapDesk/Bitfrost can be applied to keep the system modular and reduce possible information flows. Furthermore, you need to write all the critical userspace in a safe language for system and application programming like Java(*cough*) or Lisp.
Everyone can write a “minimal” microkernel/hypervisor, but that got very little to do with the problems of system/OS security. AFAIK it is an unknown research problem if the above concepts would be sufficient or additional ones are needed.
In fact, one might even interpret seL4 as a demonstration of the *failure* of formal verification. Several months of work and they “only” verify a small core and still require many assumptions on the underlying system? How long are they planning to spend for a basic SSL and X.509 library, or on systems that need *new* features now and then and must be re-evaluated? No, you need need new designs. X.509 must be replaced by SPKI, services like SSL should be implemented as a module(filter) with interfaces controlled by the security monitor to maximize code re-use and minimalize the impact of failure(e.g., don’t compromise app, just the SSL session…see sandboxing in DJB’s paper on qmail security).
The Dresden guys(Genode, Fiasco, L4env) have some userspace to build up on but aren’t focused on security.
As one of the original creators of Genode, I wholeheartedly disagree. The Genode architecture is designed with security as primary motivation. In fact, the lack of security considerations in its predecessor (called L4env) was the reason why Genode was started in the first place.
I am excited about seL4 being finally released (at least in binary form). As far as I have captured its kernel interface, it looks like it could deliver the security mechanisms required to enforce the security principles of the Genode architecture at the kernel level.
Thanks to NICTA for making this valuable work publicly available!