Version 7.0.0 of the seL4 microkernel has been released, bringing with it an alternate CMake-based build system with support for out-of-source builds and interactive configuration. Support for standalone ia32 builds and aarch64 specific documentation are also included in this release.

seL4 is a high-assurance open-source microkernel with strong isolation guarantees backed up by an end-to-end proof. In practice, this means that the seL4 codebase is bug-free in that it will behave as specified given that the proof assumptions are met. As such, it has been used to isolate critical trusted components from untrusted components running on the same processor.

The seL4 microkernel has been developed, maintained and formally verified by NICTA (now the Trustworthy Systems Group at Data61) and is owned by General Dynamics C4 Systems (GDC4S). NICTA and GDC4S decided to open-source seL4 in 2014 “in the hope that this will help everyone to build more dependable (safe, secure, reliable) computer systems.”

Read full news article on InfoQ