dependability, embedded, l4, microkernel, safety, security, seL4
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…