Because seL4 is not Linux. It has no drivers, no TCP/IP stack, no filesystem, no GUI, no sockets, no browser engine. seL4 only provides isolation, capabilities, IPC, and scheduling.
Two ways to run a applications, browser,chat app on seL4:
- Run Linux as a virtual machine (like a sandbox) on seL4, this is the easiest method, and inside that Linux VM, you install Firefox, Chrome, or a chat app normally.
- This is the hard method because you build your own OS stack using CAmkES components, but gives maximum security. You must write every component yourself: network stack, TCP/IP, storage, GUI, browser engine or chat logic, crypto, input handling. There is no package manager, no apt, no yum, no pacman. You write components in C or Rust, describe them in CAmkES ADL, and compile the whole system into one image. Each part is a separate CAmkES component. The browser or chat app is just another component with no direct access to memory or devices.
The seL4 is a microkernel designed with a single objective: provable isolation. Its architecture is intentionally minimal, allowing every line of kernel code to be formally verified. This verification mathematically proves memory safety, correctness, and strict separation between processes. Unlike Linux, seL4 does not rely on policy layers or runtime hooks. Security is built directly into the kernel’s structure.
These components of seL4 include:
- Capability-based access control – resources are accessed only through unforgeable capabilities
- Minimal trusted computing base – a few thousand lines of code drastically reduce attack surface
- Strict process isolation – no shared global state, no implicit interactions
- Deterministic kernel behavior – predictable execution eliminates timing attacks
- User-space security services – policy engines run outside the kernel
In seL4, isolation is not a policy—it is a guarantee. A process cannot access memory, objects, or capabilities unless explicitly granted. This eliminates entire classes of vulnerabilities such as privilege escalation, buffer overflows, and unauthorized resource access.
The difference between seL4 and SELinux is architectural, not functional. SELinux adds MAC on top of a massive kernel. seL4 embeds isolation into the kernel’s foundation.
seL4 provides a hardened, formally verified architecture that guarantees isolation at the kernel level. SELinux, while powerful, cannot achieve 100% mandatory access control due to Linux’s monolithic design, shared global state, and lack of formal verification. seL4 solves these limitations by design, offering a minimal attack surface, strict capability-based access, and provable correctness. For systems requiring absolute security guarantees, seL4 stands as a technically superior alternative to SELinux.
SELinux implements MAC by applying policies to processes, files, sockets, and other kernel-managed objects. However, Linux is a monolithic kernel with millions of lines of code, dynamically loaded modules, and complex internal interactions. Because of this architecture, it is impossible to enforce MAC with absolute completeness.
If you want SELinux‑like fine‑grained control over access to resources, but in a seL4 system, you can model those permissions explicitly in CAmkES using a dedicated “Broker” component. Instead of relying on kernel‑level MAC hooks, the Broker becomes the single authority that decides which client component may access which resource, under which conditions, and at what time.
CAmkES known as Component Architecture for Microkernel‑based Embedded Systems is a framework for building seL4‑based systems as a set of static components wired together via well‑defined interfaces. Each component has explicit connections (RPC, dataports, interrupts), and the entire system’s structure is described in an architecture description language (ADL). At build time, CAmkES generates glue code and a CapDL specification that maps components to seL4 objects and capabilities, giving you precise control over who holds which capability.
This is one example for seL4, CAmkES Broker component ADL example with multiple workers:
component Broker {
provides DataPort mem_manager
uses seL4SharedData pool
}
component Worker {
dataport Buf(4096) data
}
component Worker2 {
dataport Buf(4096) data
}
assembly {
composition {
component Broker broker
component Worker worker1
component Worker2 worker2
connection seL4SharedData pool_conn(from broker.pool, to worker1.data)
connection seL4SharedData pool_conn2(from broker.pool, to worker2.data)
connection seL4DataPort mem_req1(from worker1.data, to broker.mem_manager)
connection seL4DataPort mem_req2(from worker2.data, to broker.mem_manager)
}
}
The Broker is the only component with access to raw memory. Worker1 and Worker2 have no direct access. They can only send requests to the Broker. The Broker decides which worker receives access to which memory region. This is a capability graph, not a rule list. It is structurally enforced by seL4, not heuristically enforced like SELinux.
The Broker receives a request from a worker. It checks the size and then selects a region inside the raw memory pool. The worker never touches the pool directly. The Broker writes into the pool and may later share a capability or a mapped region with the worker. This is how seL4 enforces isolation: only the Broker has the capability, and only the Broker can delegate it.
Why SELinux cannot do this ? SELinux cannot enforce 100% mandatory access control because Linux is a monolithic kernel with millions of lines of code, drivers that bypass hooks, shared global state, and no formal verification. seL4 solves this by design: the Broker owns the capability, and no component can bypass it. The policy is structural, not textual.
