Communications of the ACM
Nicta Pushes Sel4 Microkernel Beyond Drones
Researchers hope the seL4 operating system will find use in industrial automation and medical device applications.
Credit: Computerworld
NICTA, previously known as National ICT Australia, recently released the seL4 microkernel operating system as open source, including all of the kernel's source code, the mathematical proofs, as well as other code and proofs for building highly secure systems. SeL4, developed jointly with General Dynamics, has full "functional correctness proof," which means the implementation adheres to its specification. "[Defense] is pretty much what [General Dynamics] are mostly interested in, so they are less interested in other use cases, particularly when it's really small initial products that you don't know if they will turn into something really big," says NICTA professor Gernot Heiser.
The operating system so far has been used largely for military systems, but the researchers hope the seL4 open source code will be employed for medical devices and industrial automation, among other uses. "SeL4 gives you guaranteed isolation between the critical and less critical parts of the system," Heiser says.
In addition, anyone who builds a project using the operating system under the GNU GPLv2 license has to distribute it under the same open source license or a newer version.
From Computerworld
View Full Article
Abstracts Copyright © 2014 Information Inc., Bethesda, Maryland, USA
No entries found