seL4 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.

Links

• The SMACCM project @ NICTA – general information about the project that uses seL4 in UAV.
• Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations – General Dynamics’ whitepaper on the subject.
• How to get started and source code – seL4 site.
• Comprehensive Formal Verification of an OS Microkernel – detailed article about seL4 formal verification.
• seL4: Formal Verification of an OS Kernel – detailed article about seL4 formal verification more concise than previous one.
• Formal Memory Models for Verifying C Systems Code – Harvey Tuch’s fascinating PhD thesis on the subject.

Key takeaways

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