The seL4 Microkit, re‑implemented as a user‑space runtime on Linux. Written in Rust, with a custom C shared library (libmicrokit.so) and example user‑space programs.
The Linux Microkit is responsible for:
- Parsing a
.systemXML configuration (usingroxmltree). - Creating and mapping shared memory regions.
- Spawning and linking protection‑domain processes from compiled C
.soplugins. - Establishing unidirectional communication channels between domains.
- Running each process under a custom event‑handler loop for notifications and protected calls.
All domains communicate via shared buffers and Unix primitives (mmap, eventfd, pipe, clone, etc.). The Microkit itself is implemented in Rust (main.rs), dynamically links into libmicrokit.so, and orchestrates the setup and execution of every domain.
- XML validation & parsing: ensure well‑formed
.systemfiles and extract memory regions, protection domains, and channels. - Automated resource setup: allocate shared memory regions, create domains with appropriate stack sizes and guard pages.
- Dynamic loading & execution: link user‑space C plugins (
.so) at runtime and invoke theirinit,notified, andprotectedentry points. - Inter-domain communication: establish and manage unidirectional channels with notifications and protected procedure calls.
- Robust error handling: catch XML errors, symbol lookup failures, and constraint violations (e.g. stack size limits).
- Linux
- Rust toolchain
- GNU GCC (with
-fPIC,-shared) - Make
.
├── Cargo.toml # Rust project manifest
├── src/
│ └── handler.c # Event handler and process bootstrap
│ ├── loader.c # Simplified loader as a C DLL
│ └── main.rs # Rust XML parser implementation
│ ├── microkit.c # Core microkit API (IPC, notify, PPC)
├── include/
│ └── handler.h # Internal shared C API definitions
│ └── khash.h # Hashmap library
│ └── microkit.h # Public API used by each protection domain
├── example/
│ ├── *.c # Example user‑space programs
│ └── example.system # XML configuration for example
├── build/ # Output directory for shared objects
├── Makefile # Build rules for C and Rust components
└── README.md # You are here
- Clone the repository:
git clone git@github.com:mikemospan/linux_microkit.git cd linux_microkit - Building the Linux Microkit
make all
- Cleanup
make clean
Invoke the loader with the .system filename as the sole positional argument:
./linux_microkit <config.system>
<config.system>can be any.systemfile in the./example/directory.- The loader will always look for
libmicrokit.soin./build/.
This example shows a simple client–server interaction over a shared memory region and notification channel.
- A single memory region
sharedof size 4 KiB is defined. - Two protection domains, server and client, map that region read–write at virtual address
0x4000000, exposing it in each asbuffer. - The client sends notifications on channel ID 1 to the server, and the server can reply on channel 2.
<?xml version="1.0" encoding="UTF-8"?>
<system>
<memory_region name="shared" size="0x1000"/>
<protection_domain name="server" stack_size="0x2000">
<program_image path="server.elf"/>
<map mr="shared" vaddr="0x4000000" perms="rw" cached="false" setvar_vaddr="buffer"/>
</protection_domain>
<protection_domain name="client">
<program_image path="client.elf"/>
<map mr="shared" vaddr="0x4000000" perms="rw" cached="false" setvar_vaddr="buffer"/>
</protection_domain>
<channel>
<end pd="client" id="1"/>
<end pd="server" id="2"/>
</channel>
</system>- The loader allocates and maps the
sharedregion into both domains. - After
server.elfandclient.elfare loaded; each domain’sinit()is then called. - The client notifies the server to write data into
bufferon channel 1. - The server’s event handler wakes, processes the request, updates the value of
bufferand notifies back on channel 2.
- Fork the repository
- Create a feature branch:
git checkout -b feature/my-feature - Commit your changes with descriptive messages
- Push to your fork and open a Pull Request
Please keep C and Rust code style consistent.