SakuraOS Microkernel

The heart of the system. A capability-based microkernel formally verified to SPARK Platinum levels. Combining mathematical safety with high-performance IPC.

Capability-Based Security

Granular access control via Capabilities (CPtr). No implicit authority; every resource access is explicitly authorized and tracked.

Performance First

Optimized "Fast Path" IPC syscalls written in hand-tuned assembly where necessary, targeting under 200 cycles for short message passing.

Architecture Overview

The kernel aims to be minimal, pushing drivers and services to user space.

Components

IPC Manager: Synchronous & Notification mechanisms.
Memory Manager: Untyped Memory & VSpace models.
Scheduler: Priority-based preemptive scheduling (SMP).
Capability Manager: CSpace & Object derivation.

Targets

x86_64
AArch64 (ARMv8)
RISC-V 64-bit

SPARK Platinum Verification

We aim for the highest level of assurance: Absence of Runtime Errors (AoRTE) and functional correctness.

Full Pre/Post contracts on all subprograms
Information Flow Analysis for capability propagation
Loop termination and invariant proofs

System Specifications

Kernel Size Goal	< 64KB (Mini), < 256KB (Full)
Context Switch	< 500 cycles
License	MIT / Apache 2.0 (No GPL dependencies)