seL4 – Formally Verified General-Purpose OS Microkernel

seL4seL4 the first formally verified microkernel OS

Recently I’ve come across an interesting article in Aviation week journal that was related to computing actually.

This article described seL4 microkernel operating system that had unique security features built-in that make this OS hard for hackers to crack. What is interesting is that seL4 microkernel was formally verified using automatic prover.

After digging a bit more I’ve found a whole new world of formal verification in general and of seL4 verification specifically.

If you are interested in formal verification of code and in microkernel operating systems then you’ll find below links useful.

In addition, the detailed article about formal verification of seL4 may be of interest as to SW so to QA engineers.

By the way seL4 OS is used in mobile phones running Android and in other security demanding platforms, such as a quadcopter unmanned aircraft and Boeing’s Unmanned Little Bird (ULB) helicopter that were mentioned in Aviation week article.


Key takeaways

  • Formal verification methods were made practical and affordable.
  • If you need secure general purpose operating system consider seL4.

Java Code Geeks