seL4® provides the trusted software base for your product.

Are you willing to risk your business and your clients on poor security?

You don’t have to look far to find the words “data breach” or “cyber attack” in the news. But, with a robust security solution, you can make sure your name isn’t attached to it.

The seL4® microkernel is a cost-effective, open source solution you can use to build products on a trusted software base, and DornerWorks, a founding member of the seL4 Foundation, can accelerate your integration. We are leaders in accelerating integration of seL4 as the trusted software base for your product.

How it Works

Schedule a Meeting

DornerWorks is a leader in accelerating integration of seL4 as the trusted software base for your product.

Implementation is simple, and add-on modules customize seL4 to your security needs.

Thwart hackers

The seL4 spec and binary satisfy the classic security properties of integrity and confidentiality.

Reduce costs

seL4 is open source, which means it’s free to download and use.

Restore confidence

seL4’s security is mathematically proven, and supported by a growing ecosystem of developers.

seL4 Quick Start Package

Get your products up and running on a secure platform with a 2-day training workshop and pilot projects to help you understand how to apply seL4 across your system.

Get Now

seL4 Hypervisor Distributions

It can be difficult to pull together the right resources and configure an seL4 platform from scratch.

A seL4 Hypervisor Distribution can help you overcome the complexity of seL4 development and jump start your project with an example use case.

Get Now

seL4 Add-Ons

If you are already building products with seL4, these add-ons will help you add innovative capabilities and greater customization.

Get Now

seL4 on RISC-V

Renode is helping developers build secure products on RISC-V architecture using the seL4 microkernel, and we can show you how.

seL4 on RISC-V with Renode seL4 on Polarfire SoC

"I am fortunate to work with DornerWorks as a strong systems solution partner supporting our customers across so many disparate system architectures and technical challenges."

- Senior Project Manager

Kickstart your development, lower barriers to success, and build trusted products.

What is seL4?

The world’s first formal proof of correctness of a separation microkernel.
- Formal, machine-checked verification by NICTA provides proof that:
  - Source code satisfies specification (written in Haskell)
  - Object code conforms to source code
  - Security properties (e.g., kernel will never crash, nor hang)
- http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf
Very small footprint
- 8,700 lines of C code and 600 lines of assembler
Member of the L4 family of high-performance microkernels
Hardware support: x86, ARMv6, ARMv7, RISC-V
Virtualization mode
Very limited features (purposely)
- Many typical OS features delegated to user-mode applications (granted privilege via passed capabilities)
  - Device drivers, memory management, network protocol stack, file system

Getting started with seL4 is simple

1. Schedule a consultation with us.

2. We’ll discuss your system architecture and needs.

3. We’ll deliver a secure solution that fits your product goals.

Schedule a Meeting

Find the security solution that fits your needs.

SCHEDULE A MEETING

Free Development Series

Build trusted software foundations with the seL4 microkernel

Developing systems using the seL4 microkernel can be complicated. We can guide you through it, but if you’re not ready to call us for a consultation, you can still take advantage of this free series.

DornerWorks engineers will walk you through implementing seL4 on verified hardware platforms and improving your company’s security story.

This series will teach you how to:

Download the seL4 source code and development tools
Use seL4 to build a simple web page to secure your IoT
Port seL4 to the Xilinx Zynq UltraScale MPSoC
And more