Dragon

Microkernel written in SPARK Ada, formally verified with gnatprove.

Design

Capability-based microkernel. No ambient authority: every privileged operation (thread creation, page mapping, IPC) requires a valid capability with the right permission bits, checked before the operation runs. Capabilities carry an owner and can only be revoked or derived by that owner.

Subsystems:

• Dragon.Types — shared primitive types, ids, status codes
• Dragon.Capabilities — capability table, install/derive/revoke
• Dragon.Vmm — address spaces, page mappings
• Dragon.Threads — thread control blocks
• Dragon.Scheduler — priority-based ready queue
• Dragon.Ipc — synchronous rendezvous endpoints
• Dragon.Syscall — syscall dispatcher, enforces capability checks

Build

Requires GNAT (2012 profile) and gprbuild.

gprbuild -P dragon.gpr
./bin/dragon_main

Verify

Requires gnatprove.

gnatprove -P dragon.gpr --level=2 -j0

C SDK

sdk/c builds libdragon.so, a thin C ABI over Dragon.Syscall.Handle. Use it to write a service or a distribution component for Dragon in C without touching Ada.

cd sdk/c
make
LD_LIBRARY_PATH=lib ./examples/echo_service

Include sdk/c/include/dragon.h and link against sdk/c/lib/libdragon.so.

#include <dragon.h>

dragon_handle_t h = dragon_create();
dragon_install_root_cap(h, 1 /* slot */, DRAGON_NO_THREAD /* owner */);

unsigned long result;
dragon_status_t st = dragon_call(h, DRAGON_NO_THREAD, 1,
                                  DRAGON_SYS_THREAD_CREATE,
                                  /* arg1 */ 1, /* arg2 space */ 0,
                                  /* arg3 entry */ 0x4000,
                                  /* arg4 stack */ 0x8000, &result);

dragon_destroy(h);

dragon_call takes the caller's thread id, the capability slot used to authorize the call, the syscall number, up to four arguments, and an output pointer for the result. It returns a dragon_status_t. Status and syscall enum values in dragon.h match Dragon.Types.Status_Code and Dragon.Syscall.Call_Number by position — see sdk/c/include/dragon.h for the full list of syscalls and rights bits.

Versions

• 0.1 — initial microkernel MVP
• 0.2 — fixes unauthorized capability revocation and IPC message loss on concurrent senders
• 0.3 — C SDK (see CHANGELOG.md)
• 0.4 — fixes VMM lookup sentinel collision and capability derive without ownership check (see CHANGELOG.md)