seL4

The world’s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is available as open source.

Features

• seL4 is a high-assurance, high-performance microkernel developed, maintained and formally verified by NICTA (now the Trustworthy Systems Group at Data61) and owned by General Dynamics C4 Systems. It is a member of the L4 family of microkernels, and is the world’s most advanced, highest-assured operating-system microkernel.
• seL4’s implementation is formally (mathematically) proved correct (bug-free) against its specification, is proved to enforce strong security properties, and its operations have proved save upper bounds on their worst-case execution times.

Sample projects and resources

• RISC-V-Guide. RISC-V Guide. Learn all about the RISC-V computer architecture along with the Development Tools and Operating Systems to develop on RISC-V hardware..
• NeptuneOS. Neptune OS: A Windows NT personality for the seL4 microkernel.
• awesome-provable. A curated set of links to formal methods involving provable code..
• veracruz. Main repository for the Veracruz privacy-preserving compute project, an adopted project of the Confidential Compute Consortium (CCC)..
• ferros. A Rust-based userland which also adds compile-time assurances to seL4 development..
• seL4_tools. Basic tools for building seL4 projects.
• docs. This is the source of the seL4 docs..
• seL4-CAmkES-L4v-dockerfiles. Dockerfiles defining the dependencies required to build seL4, CAmkES, and L4v..
• selfe-sys. A generated thin wrapper around libsel4.a, with supporting subcrates..
• sel4-armv8-vmm-manifest. A manifest that allows one to build virtualized seL4 for zcu102 and i.MX8.
• rpi3-rust-fel4-workspace. Rust embedded things running on the seL4 microkernel for the Raspberry Pi 3.
• ICSVerifiedSoftwareProject. A formally verified implementation of a bolt-on security device for ICS networks. Designed with TLA+ and written/proved in F*.
• solox-amp-rust. AMP experiments in feL4 (seL4/Rust) on SoloX ARM SoC (A9 + M4).
• ci-actions. CI GitHub actions for the seL4 repositories.
• website. The seL4.systems website.
• SeL4_101. How to create a Hello World seL4 project from scratch .
• Sofa. Operating System built on top of the seL4 microkernel..
• ferros-sabrelite-toy-system. Rust seL4 toy system built on ferros for the imx6 sabrelite platform.
• Advanced_Operating_System_2017. Basic operating system features implementation. File system/Process management/Memory management.
• veracruz-examples. A repository of larger example Veracruz computations .
• seL4_hydra. Attestation and software update in seL4.
• sel4-hobd-prototype. Prototype HOBD system running on seL4.
• seL4cp-workshop. My solutions to the draft-version of the seL4 Core Platform (seL4cp) Workshop held during the 2022 seL4 Summit (11 - 13 Oct)..
• whitepaper. Source for the seL4 white paper.
• fel4-test-project. A feL4 test project (Rust on seL4) - armv7 imx6 sabre lite.
• ferros-fancy-test. Test-runner support libraries for ferros..
• SeL4_CPIO. Create a simple SeL4 Project with a CPIO archive.
• SeL4_UserLandLib. How to Create a library and link an application against it .
• Sel4_EGA. how to use EGA display with Sel4.
• sel4twinkle-alloc-rs. An experimental Rust port of libsel4twinkle allocator.