seL4 networking: stronger boundaries, existing systems.

What does networking on seL4 mean?

seL4 is a microkernel: it provides the foundation for controlling access to memory, processor time, and communication. Ethernet drivers, network stacks, and application protocols are separate software components built above that foundation. Using seL4 does not automatically make a network stack verified.

The useful design question is which components must be trusted to enforce a particular security requirement. A network driver may need access to its device and packet buffers; it need not receive access to every application's memory or to cryptographic keys. Separating those responsibilities lets engineers reason about a smaller set of privileged components.

Microkit makes the system structure explicit

The seL4 Microkit provides a framework and SDK for building systems whose structure is defined ahead of time. Protection domains host components, while configured channels and shared memory provide the communication paths they need.

For networking, that structure can separate device handling, packet processing, cryptographic operations, and access to field equipment. Each connection is an engineering decision: what data crosses it, who can write it, how inputs are checked, and what happens when a component fails.

Reduce exposure—and limit what a compromise can reach

Our approach is surgical. We identify the components whose behavior is essential to a security boundary and focus the replacement or redesign there. The existing applications and operating systems can continue to do their jobs on the other side of that boundary.

• Expose fewer services. Include the interfaces and protocols the deployment needs, and avoid unnecessary management endpoints at the network boundary.
• Grant less authority. Restrict each component's memory, device access, and communication paths to its role. Hardware and DMA access must be accounted for as part of that design.
• Separate parsing from permission. Treat received data as untrusted. Where the application requires it, place authorization checks between a protocol handler and the operation it requests.
• Make failure behavior deliberate. Define how malformed traffic, exhausted buffers, and component faults affect forwarding and equipment access. Isolation helps contain faults; availability still requires its own design and testing.

Fewer exposed features reduce opportunities for attack. Isolation addresses a different problem: limiting the consequences when an exposed component does contain a vulnerability. Both matter.

Example: replace a gateway, preserve the control stack

Consider a site where an Ethernet-connected gateway links supervisory software to serial Modbus equipment. A targeted project could replace that one gateway while retaining the supervisory applications and field devices.

For example, the gateway could permit reads from a defined register range while rejecting writes from a monitoring client. Network-facing code would communicate with the field-side service through a constrained interface, rather than having unrestricted access to the serial device.

This protects a specific path into the equipment. It does not remove vulnerabilities from the supervisory software, prevent every misuse by an authorized client, or protect an alternate connection that bypasses the gateway. Those limits define what the system must address next.

What seL4 assures—and what still needs engineering

seL4's machine-checked proofs establish kernel properties for supported, verified configurations. The applicable guarantees depend on the chosen platform, kernel configuration, and the assumptions of each proof.

They do not automatically verify the drivers, network protocols, cryptography, or application policy built above the kernel. The proof assumptions also make hardware, boot, and DMA behavior relevant to the assurance argument. Key management, updates, recovery, and deployment configuration remain system responsibilities.

That is where our engineering work fits: define the boundary, select the components that enforce it, integrate them with the existing environment, and validate behavior against the project's requirements.

seL4 consulting and custom networking engineering

We work on system architecture, Microkit component integration, device and protocol interfaces, and testing of the paths between them. Engagements can focus on a specific component or on a networking boundary that connects existing equipment and software.

A useful starting point is the equipment and protocols involved, which systems must remain in place, and the operations that should be permitted across the boundary. From there, we can discuss scope, platform constraints, and the evidence needed to support the design.