Linked by jimmy1971 on Thu 27th Jan 2011 22:21 UTC
Privacy, Security, Encryption "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."
Thread beginning with comment 460013
To view parent comment, click here.
To read all comments associated with this story, please click here.
RE: Thinking...
by pepper on Fri 28th Jan 2011 10:26 UTC in reply to "Thinking..."
pepper
Member since:
2007-09-18

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.

Reply Parent Score: 1

RE[2]: Thinking...
by nfeske on Fri 28th Jan 2011 14:37 in reply to "RE: Thinking..."
nfeske Member since:
2009-05-27

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!

Reply Parent Score: 1