24 projects using seL4 RTOS
seL4 is a high-assurance, high-performance microkernel that is the first of its kind to be formally verified for functional correctness and security properties. It serves as a minimal core for building secure and reliable operating systems by enforcing strict isolation through a capability-based access control system.
A security framework for remote attestation and secure software updates built on the formally verified seL4 microkernel. It targets the I.MX6-SabreLite platform as a prover and utilizes a Windows-based verifier to ensure system integrity through the HYDRA and ASSURED architectures.
A development workspace for building Rust applications on the seL4 microkernel specifically for the Raspberry Pi 3 platform. It provides hardware abstraction layers for the BCM2837 SoC, DMA-backed graphics libraries, and various driver examples for embedded systems development.
A build manifest for deploying a virtualized seL4 environment on ARMv8 platforms including the Xilinx ZCU102 and NXP i.MX8. It integrates the seL4 microkernel with a Virtual Machine Monitor (VMM) to support guest Linux instances and inter-VM communication.
A collection of Dockerfiles and build infrastructure providing standardized development environments for the seL4 microkernel, CAmkES component framework, and L4v verification toolchain. It simplifies the setup of complex dependencies required for building, testing, and verifying seL4-based systems across x86, ARM, and RISC-V architectures.
A workshop project implementing a C-based version of the Wordle game running on the seL4 Core Platform. It demonstrates the development of isolated components on the seL4 microkernel, targeting ARM platforms such as QEMU and Raspberry Pi 3B.
A demonstration project for the seL4 microkernel that illustrates how to bundle multiple applications into a CPIO archive. It features a root server that parses the archive at runtime to load and execute embedded application binaries using the seL4 build system and libcpio.
A prototype Honda On-Board Diagnostics (HOBD) system built on the seL4 microkernel for the Sabre Lite IMx6 platform. It manages ECU diagnostic connections, logs data to an SD card, and provides a multi-threaded console interface for real-time system interaction.
A technical tutorial and project template for building a 'Hello World' application on the seL4 microkernel from scratch. It provides a manual setup for the project layout, CMake build system, and a basic root server implementation targeting x86_64 simulation.
A test project for the seL4 microkernel demonstrating EGA text display functionality on x86 platforms. It provides a simple implementation for graphical output in a secure microkernel environment, inspired by the seL4 examples repository.
The official web presence and documentation hub for the seL4 microkernel, the world's first operating system kernel with a formal mathematical proof of implementation correctness. It serves as a comprehensive resource for the seL4 ecosystem, covering hardware support, development tools, and industrial use cases.
A technical tutorial demonstrating the creation and integration of userland libraries within the seL4 microkernel environment. It provides a minimal implementation of a library called libFoo and shows how to link a root server application against it using the seL4 CMake build system.
A collection of essential tools and configuration files for building and maintaining seL4-based projects. It includes an ARM kernel elfloader, a comprehensive CMake-based build system, and various utilities for code style enforcement and project management.
An experimental Rust port of the libsel4twinkle allocator for the seL4 microkernel. It provides memory allocation capabilities for Rust-based seL4 projects, specifically targeting platforms like the SoloX ARM A9 + M4.
A generated thin wrapper around libsel4.a for the Rust programming language, providing access to seL4 microkernel syscalls and constants. It includes a suite of tools for configuring and building seL4-based applications, supporting platforms like ARM and x86_64.
Sofa is an operating system framework built on the seL4 microkernel, providing a suite of userland servers and a POSIX-compliant API via the musl C library. It includes a virtual file system, a UDP network stack using lwIP and virtio, and comprehensive process management capabilities.
An Asymmetric Multi-Processing (AMP) experiment using the seL4 microkernel and Rust on the i.MX6 SoloX SoC. It demonstrates running seL4 on the Cortex-A9 core to manage system resources and boot a bare-metal Rust firmware on the Cortex-M4 core.
The official whitepaper for the seL4 microkernel, providing a technical introduction to its architecture, formal verification, and security features. It covers seL4's role as both a high-performance microkernel and a hypervisor for security- and safety-critical embedded systems.
A demonstration project showcasing Rust applications running on the seL4 microkernel using the feL4 framework. It implements inter-thread communication between Rust-based threads on ARM and x86 platforms, utilizing the cargo-fel4 build system.
A suite of test-runner support libraries designed for the Ferros RTOS framework. It provides macros and runner utilities to facilitate automated testing within the Ferros and seL4 microkernel ecosystem.
A Rust library providing smart type-safe wrappers for seL4 microkernel development with a focus on compile-time resource tracking. It ensures memory safety and capability management through Rust's type system, targeting ARM-based embedded platforms like i.MX6 and TX1.
A demonstration system built on the seL4 microkernel using the Ferros Rust-based userland framework. It targets the i.MX6 Sabre Lite platform and implements a multi-process architecture including a TCP/IP stack, persistent storage, and an interactive console.
A comprehensive implementation of a Simple Operating System (SOS) built on the seL4 microkernel for the UNSW Advanced Operating Systems course. It features a process server, network stack integration via lwIP, and a custom shell, primarily targeting the i.MX6 ARM platform.
A curated collection of resources, languages, and tools focused on formal verification and provably correct software. It covers interactive theorem provers like Coq and Lean, dependently typed languages like Idris and Agda, and high-assurance projects such as the seL4 microkernel.
A centralized repository of GitHub Actions and reusable workflows designed specifically for the seL4 microkernel ecosystem. It automates critical tasks such as kernel compilation, formal proof verification, hardware simulation, and code style enforcement across multiple seL4-related projects.