If you’ve ever found yourself wondering if your IP was secure enough, you’re not alone.
If you’ve ever wondered how to make it more secure, the seL4 microkernel offers an answer.
The traditional approach to showing security in your system involves very detailed design and penetration testing. This also leads to long development cycles, and seemingly endless loops of design, development, pen. testing, bug/vulnerability fixes, and so on. Even then, after you are ready for release, security vulnerabilities and bugs are often still discovered. This results in long-term maintenance and providing customers with frequent security patches, leaving them to ask, “Is this actually secure?”
The seL4 Microkernel, developed by Data61, enables verified extreme security on the i.MX6 SOC Sabre Lite platform, and functionally correct security on the x64 PC99 (64-bit) and NVIDIA Tegra K1 TK1-SOM platforms. It works on a number of other ARM and x86 platforms as well, though full verification may not be available.
Data61 developed seL4 in about 12,000 lines of C and assembly code to “provide a reliable, secure, fast, and verified foundation for building trustworthy systems.” DornerWorks has furthered Data61’s work by providing open source libraries for the microkernel, as well as expanding the seL4 ecosystem through key partnerships with organizations aligned with aerospace and defense.
The formal proof of seL4 provides confidence to you and your customers that core aspects of your system are actually, and extremely, secure. The binary code of the seL4 microkernel correctly implements the behavior described in its abstract specification and nothing more. This prevents the following in the kernel:
The specification and the seL4 binary satisfy the classic security properties of integrity and confidentiality. Integrity means that data cannot be changed without permission, and confidentiality means that data cannot be read without permission. These properties are crucial in any system that requires extreme security and/or safety. They are the backbone for systems that rely on isolation. Moreover, this makes seL4 an attractive solution for systems that may not have extreme security requirements, but still want proven isolation between separate software components.
In addition, seL4’s security and core functionality is backed by mathematical proof.
Most solutions that come with a security certification also come with expensive licensing costs. These solutions also still use a traditional approach and may not provide as strong of a security story as formal methods.
seL4 is an open source solution.
The seL4 kernel is licensed under GPLv2, while its libraries and tools are mostly licensed under BSD. This means seL4 has no licensing costs and is free to use. However, cost-effectiveness is just one of the benefits of using open source tools in your design. There are several others, all discussed in this post, “Open Source Software Can Enable These 9 Benefits in Your Technology Development.”
The proof of seL4 informs its design. Therefore, it is important to understand some of its less conventional implementations.
Kernel space and user space are well known concepts for all operating systems, but since seL4 is a microkernel, a specific approach is taken. The kernel is left as small as possible and components that would traditionally be in a monolithic kernel are pushed out to the user space.
Examples of kernel functionality delegated to User Space include:
The advantage of this architecture is that unlike a monolithic kernel, which can be affected by a fault in a device driver, the components in a microkernel are isolation from each other. This means that if a component fails or becomes compromised, another monitor service could restart it or perform some other diagnostic action.
The seL4 kernel provides a strong promise of isolation between these separate components if the system designer takes advantage of the mechanisms offered by seL4.
Capabilities are used to grant access to specific resources in a system. They also form the basis of security in seL4.
The kernel keeps track of everything in the capability derivation tree (CSpace). Capabilities are required for any operation on a kernel object. This prevents bad actor threads from gaining access to a resource in another thread that they aren’t already given access to.
Endpoints allow small amounts of data and capabilities to be transferred between two threads, and can be invoked with seL4 kernel system calls. They also handle the following:
Messages within an seL4 application can be sent to either an “endpoint” or other kernel objects
After the seL4 kernel boots, all of the unused memory it knows about is given to the root thread. It is up to the application running as the root thread to “Re-Type” this memory as other kernel objects which can then be passed around to build up and architect the system. This is the building block for virtual memory spaces, capability spaces, thread control blocks, and other kernel objects.
A system designer must be aware of the API to the system. In order to build a secure system they must make use of the primitives and mechanisms made available by the seL4 kernel. While the API provided by seL4 is spartan compared to other APIs that developers may be used to, such as the terminal shell or POSIX standard interface, the system designer can develop their applications to adhere to seL4 system API calls, or develop a higher level API on top of these system calls, to take advantage of the isolation and security properties offered by the seL4 kernel.
From these building blocks a system designer can create isolated environments and dole out access to resources and other seL4 mechanisms protected by capabilities. While it is not impossible to start a system from here, there are other tools that aid in auto generating setup and plumbing code so that a system designer can focus on the high-level concepts. Data61 has developed a system called CAmkES (Componentized Architecture for microkernel Embedded Systems) which allows you to think about your system as isolated components and connections. DornerWorks can help architect a system either way and has experience porting applications running on other operating systems to seL4 and/or CAmkES.
Half-measures and fragile security systems are a thin defense against the leaking of your data to any interested party. And, that’s why the seL4 microkernel is so important to modern technology development.
seL4 offers extreme security with mathematical proof, and keeps companies steps ahead of costly, brand- damaging cyber threats. Product developers in aerospace, defense, medical, and consumer markets who are already implementing the seL4 microkernel into their products, can attest to its stability and value.
seL4 isn’t for everyone. It’s a complex technology and may require many hours of engineering to configure to your specifications and port to the seL4 API. But, if you are concerned with managing a proprietary solution on your own, looking for a more cost-effective option, or even hoping to strengthen your security story after previous experiences, seL4 is for you.
For a more in-depth overview of the seL4 microkernel, check out this webinar from embedded engineers Robbie VanVossen and Jesse Millwood.
seL4 has already been proven secure, so you don’t have to do the extreme math yourself. DornerWorks will help you fill in the gaps to enhance your security story.
You can download the seL4 source code and tools to get started developing your own project with the instructions provided by Data61 here:
And the specialized seL4 tools DornerWorks has contributed to by extending Data61’s seL4 tools repository here:
When you’re ready to start building your next innovation, contact us and we’ll help you deliver extreme security to your products and your customers.
Good Luck and happy coding!