Microkernels Again, and Mathematically Proving Safety and Reliability

“The L4.verified project demonstrates that such contracts and
proofs can be done for real-world software. Software of limited
size, but real and critical.

“We chose an operating system kernel to demonstrate this: seL4.
It is a small, 3rd generation high-performance microkernel with
about 8,700 lines of C code. Such microkernels are the critical
core component of modern embedded systems architectures. They are
the piece of software that has the most privileged access to
hardware and regulates access to that hardware for the rest of the
system. If you have a modern smart-phone, your phone might be
running a microkernel quite similar to seL4: OKL4 from Open Kernel
Labs.”

“Yes, yes,
it’s verified. But does it run Linux?

“We’re pleased to say that it does. Presently, we have a
para-virtualized version of Linux running on top of the
(unverified) x86 port of seL4. There are plans to port Linux to the
verified ARM version of seL4 as well.”

“There
is now a way to mathematically prove that the software
governing critical safety and security systems in aircraft and
motor vehicles is free of a large class of errors – long before the
plane takes off or the car’s engine starts.”

Complete
Story