SYSTEMS / SECURITY
TCS
A capability-oriented operating-system seed built from isolated communicating servers on seL4/Microkit.
- Current state
- Bootable OS seed
- Discipline
- Systems · Security
- Built with
- C / seL4 / Microkit / AArch64 / QEMU / Monocypher / Python build/test tooling
The idea
Software authority should be explicit, isolated and checked when an operation occurs. TCS explores that model in a small operating-system seed whose communicating servers enforce policy over a fixed microkernel capability graph.
How it works
A fixed kernel capability graph connects small native servers. An allocation-free policy state machine checks subject, object, rights and session generation on each read; separate profiles explore read-only UART interaction, signed administration and bounded worker lifecycle experiments.
What’s implemented
- Five-domain bootable seed in AArch64 QEMU
- Per-request policy checks, session revocation, quarantine and audit exhaustion
- Isolated read-only UART terminal and separate signed interactive profiles
- Saved boot images, transcripts, build reports and invariant tests
PROJECT STATUS / BOOTABLE OS SEED
Where it stands
Bootable OS seed
- A seed, not a general-purpose operating system
- Compile-time typed capability handles, persistent storage and dynamic process creation are not implemented
- Application authorization changes inside a fixed capability graph; seed revocation is not dynamic kernel-capability deletion
- No formal-verification or production-readiness claim
Source & resources
Documentation behind this project page
Reviewed October 1, 2026. Project descriptions reflect a source review; repository validation claims were not independently reproduced.