GuardBSD Logo



Rust Multi-Microkernel OS • Capability Security • BSD Licensed • Winter Saga Release



*** UNDER CONSTRUCTION ***



Welcome to GuardBSD Documentation

This is the official documentation for GuardBSD - a secure, capability-based, multi-microkernel operating system written entirely in Rust.

echo "Documentation is working!"

Use the sidebar to navigate through architecture, installation, APIs, internals and user guides.


Overview

GuardBSD is a modern, secure operating system built on a unique three-microkernel architecture, unlike traditional monolithic or single-microkernel designs:

  • µK-Space - memory management
  • µK-Time - scheduling & timers
  • µK-IPC - inter-process communication

Each microkernel is:

  • minimal,
  • isolated,
  • formally verifiable,
  • responsible for one strictly defined subsystem.

GuardBSD is designed for high-assurance environments, formal verification,
and multi-architecture support (x86_64 and ARM64).


Design Philosophy

Separation of Concerns

Each microkernel implements exactly one subsystem - eliminating kernel bloat and reducing bugs.

Security First

  • Capability-based security model
  • No ambient authority
  • Full revocation & delegation
  • Minimal trusted computing base

Formal Verification

Microkernels are intentionally small enough for automated proof systems.

Multi-Architecture Support

A unified Rust codebase supports identical behavior on x86_64 and ARM64, using architecture abstraction layers.


System Architecture

GuardBSD consists of:

  • Applications
  • System library (libgbsd)
  • Userland servers: Init, VFS, RAMFS, DevD, NetD
  • Drivers: Storage, serial, block devices
  • Three microkernels: µK-Space, µK-Time, µK-IPC
  • Hardware Abstraction Layer

See the detailed diagrams in Architecture Overview →


Microkernels

µK-Space (Memory)

Responsible for PMM, VMM, page tables, TLB, and address space creation.

µK-Time (Scheduler)

Implements the thread scheduler, timing subsystem, and timer interrupts.

µK-IPC (Communication)

Handles message passing, IPC ports, capability routing, and IPC syscalls.


Target Use Cases

  • Secure embedded devices
  • High-assurance systems
  • Real-time workloads
  • Virtualization environments
  • Networking appliances
  • Research & academic OS design

Recommended Next Sections

  • Architecture - high-level and full diagrams
  • Features - minimalism, security, performance
  • Status - roadmap and development progress

GuardBSD -> Secure • Fast • Modern

GuardBSD Overview

GuardBSD is a modern, secure, capability-based operating system built on a unique three-microkernel architecture. Unlike monolithic kernels or traditional single-microkernel systems, GuardBSD splits all privileged functionality into:

  • µK-Space - memory management
  • µK-Time - scheduling & timers
  • µK-IPC - inter-process communication

Each microkernel is:

  • minimal,
  • isolated,
  • independently verifiable,
  • responsible for one clearly defined task.

GuardBSD is written entirely in Rust and designed for formal verification, multi-architecture support, and high assurance environments.

Design Philosophy

Separation of Concerns

Each microkernel implements one subsystem only.
This eliminates kernel bloat and makes verification feasible.

Security First

  • Capability-based security
  • Zero ambient authority
  • Revocation and delegation
  • Minimal trusted computing base

Formal Verification

Microkernels are small enough to be machine-verified.

Multi-Architecture Support

A unified codebase supports x86_64 and aarch64 using architecture abstraction layers and Rust conditional compilation.

System Architecture

GuardBSD consists of:

  • applications,
  • system library (libgbsd),
  • userland servers (VFS, NetD, DevD, Init),
  • drivers,
  • three microkernels,
  • hardware abstraction layer.

See the full architecture breakdown in
Architecture Overview.

Microkernels

µK-Space (Memory)

Responsible for PMM, VMM, page tables, TLB, address space creation.

µK-Time (Scheduler)

Priority scheduler, timers, thread states, interrupt-driven scheduling.

µK-IPC (Communication)

Message passing, ports, capability management.

Target Use Cases

  • secure embedded devices
  • real-time systems
  • virtualized environments
  • high-assurance infrastructure
  • research and academic use

Next Sections