Security that is structural, not secret.
BraiNIX is a capability-based, security-first microkernel written end to end in Rust. Every guarantee is enforced by the design — the capability model, the type system, or a machine-checked proof. Nothing rests on an attacker not knowing something.
First principles
These decide every tradeoff. When they conflict with convenience, convenience loses.
Least authority
Nothing holds a capability it does not need, and no capability is ambient. Authority is named, granted, and revocable.
Fail closed
Absence of an explicit grant is denial. An error path that cannot prove safety denies the operation.
Structure over secrecy
Security is a property of the design, enforced by the capability model, the type system, or a machine-checked proof — never by what an attacker doesn’t know.
Minimize & name the trust
The set of components that can violate security is small, written down, and justified. Anything outside it is treated as hostile.
Every claim is falsifiable
A property that is asserted but not checked does not count as enforced. If it isn’t verified, it isn’t a guarantee.
Convenience is not a principle. It never wins a tie.
The contract
Each invariant is named, documented, and individually checkable. Asserted is not enforced.
No ambient authority. Every server’s capability set is frozen at launch, and capabilities are unforgeable typed tokens.
W^X holds for every page, always. No dynamic kernel heap — fixed-size pool allocators only. Per-process page tables (KPTI).
Inter-process communication is synchronous rendezvous only. No shared-memory IPC and no async queues exist in tree.
Every release is measured into the TPM, reproducibly built, and Ed25519-signed — with predicted PCRs published before the artifact ships.
The observe-only auditor reports and nothing else. It holds no spawn, kernel-mutation, or network capability — its compromise costs visibility, never privilege.
Any assistance layer acts only after explicit per-action consent on the trusted console, reached through capability-mediated IPC. A tenant, never a trusted authority.
Architecture
The smallest possible ring-0 surface. Everything else is an isolated, bounded userspace process.
Microkernel core
Drivers, filesystem, and the network stack all run in userspace. Ring 0 holds only what cannot live anywhere else.
Capability-mediated everything
No ambient authority. Every resource is reached through an unforgeable, typed, bounded, revocable token.
KPTI & W^X, structurally
The kernel is never mapped in user page tables. No page is ever simultaneously writable and executable — anywhere.
Decomposed network stack
Link, IP, and transport run as three separate isolated servers, chained only by synchronous IPC. Containment is the default.
One server per device
Each hardware device gets its own isolated server with a bounded capability set. A driver compromise stays local.
Measured, reproducible boot
Bootloader through kernel is measured into the TPM and Ed25519-signed, reproducibly built from source the project owns.
Hard lines
Do not cross without explicit sign-off. These are not preferences.
- — No ambient authority anywhere. Capability sets are frozen at launch.
- — W^X enforced globally and structurally. No page is ever writable and executable.
- — Synchronous rendezvous IPC only. No shared memory, no async queues.
- — No dynamic kernel heap. Fixed-size pool allocators only.
- — The dependency closure only ever shrinks toward zero external code.
- — No path to security depends on attacker ignorance.
Non-goals: POSIX compatibility · dynamic loading · ambient authority · network egress without an explicit grant · telemetry or phone-home of any kind · and any security argument that rests on obscurity.