Minimal OS for Fobnail Project
The Fobnail Project aims to build a USB device capable of verifying trustworthiness of the platform it is connected to. The project is described more in-depth here.
According to the information presented at TrenchBoot Summit 2021 Fobnail: Attestation in Your Pocket, the minimum OS, together with the connected Fobnail Token, should allow determining the state of the platform before the target OS is launched. As we can see in the presentation, heads (here presented as a coreboot payload) could be responsible for the platform's trust control. But in this document, we want to present the results of research on the possibilities of using various operating systems running as DLME that will perform the same function.
Also it should be possible to launch minimal OS from an already running target OS, this is called late launch as opposed to early launch described above. Minimal OS would communicate with Fobnail Token, perform attestation in order to determine platform state, and then hand the control back to the main OS. Currently, only early launch will be supported, late launch is planned as a future improvement.
We pay attention to the drivers supported by each OS. We need the following drivers:
- TPM drivers
- Drivers required for communicating with Fobnail Token:
- USB host drivers - at minimum EHCI and xHCI support, however UHCI and OHCI would be good to have
- USB EEM driver - emulated Ethernet driver
- network stack with IPv4 support
Also we pay attention to OS security, ability to run in DLME, including portability between different hardware (a single binary should be able to boot on all x86 platforms with support for ACPI) and ability to chainload another, target OS.
The table below summarises OS features which are a hard requirement, though they could be implemented by us.
|USB host driver||Required for communication with Fobnail Token|
|USB EEM driver||Required for communication with Fobnail Token|
|Network Stack||Required for communication with Fobnail Token|
|TPM driver||Required to perform attestation|
|Bootloader Capabilities||Required to boot target OS|
|C library||Fobnail Attester is writen in C|
|Bootable by SKL||Whether OS can be loaded by TrenchBoot SKL without SKL or OS modification|
|License||Whether OS use open-source license, and if licese used is applicable for embedded market|
These are another features which are taken into account (soft requirements).
|Microkernel||Microkernels are more secure and are preferred|
|OS portability||Required to avoid rebuilding minimal OS for each device|
|CPU Architecture support||OS supported architectures, mostly we consider x86, ARM, RISC-V and POWER|
Different OSs propositions
The research effect is presented below. 8 systems were considered
- seL4 (with and without CAmkES)
- Little Kernel / Trusted Little Kernel
Each of them has a short description, an analysis of the launch in DLME, and the possibilities and potential problems that will have to be addressed for the Fobnail Token to be functional.
Zephyr is a well-known and supported embedded RTOS with a monolithic kernel written in C. It supports various devices ranging from Cortex-M to x86 CPUs. It's main benefits are IPv4, CoAP, and USB (including USB EEM) support which are required for communication with Fobnail Token. Other benefits are listed here.
Running in DLME
Secure launch uses a component called SKL (Secure Kernel Loader) which is responsible for booting OS in DLME (Zephyr in that case). Zephyr boots using Multiboot1 but SKL does not support it (only Multiboot2 is supported). For SKL to be able to boot Zephyr, Zephyr must gain Multiboot2 support.
Multiboot1 is hard to measure due to its tags being scattered around in memory. To properly measure Multiboot1, SKL would have to know and parse every tag as most of them contain pointers to other structures. This is not going to happen.
Also, Zephyr may have trouble with running on different hardware configurations. Some important HW-related configuration is baked into Zephyr during build:
LAPIC base is selected by
CONFIG_LOAPIC_BASE_ADDRESS, if target platform has LAPIC remapped using
IA32_APIC_BASEZephyr will break.
APIC mode (xAPIC vs x2APIC) is selected when building Zephyr and cannot be detected at runtime. Zephyr may not boot if it has different APIC mode set than firmware has.
As part of the PoC tests, the possibility of using Zephyr as a minimum OS running in DLME was checked. The results are described here.
Zephyr provides most of the drivers needed for integration:
- USB hub drivers,
- USB EEM driver,
- Network stack with IPv4 and CoAP support.
TPM driver is missing, there is a fairly recent PoC implementation of TPM2 stack, but it is intended for embedded devices and supports SPI only.
Zephyr provides good support for standard C library (newlib), which should simplify Fobnail Attester porting.
Basically runs under GPLv2 License but more information can be found here.
Xous is a microkernel-based OS written in Rust, currently in Alpha state. Xous is used as a secure microkernel for Betrusted device and is focused on RISC-V, which right now is the only architecture supported. However, x86 already contains dummy implementation which probably will be extended someday.
Running in DLME
Xous currently cannot run on x86, and DLME on RISC-V is not covered here. We have opened an issue raising the subject, among others, about x86 support.
Xous has network support but currently lacks USB host drivers and TPM support. Also, it lacks C interface for calling the kernel and lacks C library. This should not be a serious problem and may be solved by rewriting Fobnail Attester in Rust or by adding required C bindings to Rust code. It means that getting Fobnail Attester running may require some amount of work. Also, Xous needs to gain kexec-like abilities to chainload target OS.
The Xous microkernel runs under Apache 2.0 license.
seL4 is a secure L4 family microkernel written in C. It has strong security guarantees assured by formal proofs. However these proofs are still incomplete for x86; see Supported Platforms for an up-to-date verification status. Due to its microkernel nature, seL4 provides stronger isolation. A breach in one of the components (such as a USB driver or the network stack) wouldn't compromise the entire OS (contrary to monolithic kernels).
We have opened an issue about seL4 usage as secure bootloader.
Running in DLME
It should be runnable, however due to microkernel nature all programs run in unprivileged mode which complicates booting of the target OS. seL4 would have to gain kexec-like abilities. seL4 developers are willing to add kexec support.
seL4 provides virtually no drivers, except a few drivers listed
According to the page linked above,
libusbdrivers is inactive and lacks XHCI
support. seL4 has basic support for an old version of musl C library (v1.1.16).
Using seL4 would require a significant amount of work:
- Extending USB drivers,
- Implementing USB EEM driver,
- Implementing TPM driver,
- Porting Fobnail Attester,
- seL4 runs all processes in unprivileged mode, so the kernel itself would have to be modified to allow booting of another kernel.
Genode can provide many of the required drivers. See the section below for details.
CAmkES provides tools for writing seL4-native components, it also has VMM support for running virtual machines. Contrary to Genode CAmkES does not provide drivers, but VMs may provide them. However this requires virtualization and seL4 currently supports it only on Intel CPUs. See the section below for more details.
The documentation shows that the seL4 kernel itself and most of its proof is licensed under GPL Version 2.
Genode is a framework for creating
custom, specialized OSes. It can work on various kernels/hypervisors, including
seL4 and Linux. It provides many drivers, including USB drivers (including
usb-net driver which should handle USB EEM) and a network stack. When running
on Linux all components are sandboxed with seccomp, however it should be noted
that Linux drivers are used. For other kernels Genode provides sandboxed
Running in DLME
Whether Genode can run in DLME depends on the choosen kernel, however we are interested mainly in seL4. Please see seL4 section above for details.
TPM driver would have to be ported to Genode. Underlying kernel must have kexec abilities and Genode must have component capable of invoking kexec. USB and EEM drivers should work out-of-the-box.
Genode's seL4 support is considered to be in healthly state (see this comment). But it should be noted Genode with seL4 has not been used outside the lab so far.
Genode license (AGPLv3) is very restrictive and it could be a problem for the Fobnail Project.
seL4 + CAmkES
CAmkES provides tools and libraries for quickly writing seL4-native components.
seL4_libs CAmkES is planned to be formally verified (verification
is in progress).
Running in DLME
Since CAmkES is based on seL4, the same restrictions apply. See the section above for details.
CAmkES also does not provide many drivers. However it does provide VMM for virtual machines. Features:
- Support for booting Linux kernel.
- Support only for 32-bit VMs, according to
The first step is to install Ubuntu natively on the cma34cr. It’s currently required that guests of the camkes-vm run in 32-bit mode, so install 32-bit Ubuntu.
- Support for hardware passthrough, however it is severely limited and it requires manual configuration, including IO port assignment, memory mapping, interrupts setup. This is completely not portable and cannot be used in this form. Normally, VM config is written in CAmkES specific language, which is processed during build. VM config cannot be generated at runtime making robust HW passthrough impossible.
- Lack of support for AMD-V. Until this is implemented there is no virtualization on AMD CPUs.
If CAmkES had good enough virtualization we could take the following approach to build secure OS for running Fobnail Attester:
- Fobnail Attester would have to be split into 2 parts: part that communicates with Fobnail Token through network and a separate part called secure component.
- Secure component would be a program running natively under microkernel and it would be responsible for:
- Loading next stage OS into RAM (disk drivers would be located in Linux VM) and extending PCRs early during minimal OS startup.
- Starting Fobnail Attester in Linux.
- Acting as a proxy between Fobnail Attester and TPM - only operations required to perform platform provisioning/attestation like TPM quote, reading EK certificate, etc. (this must be a minimal component providing only the most basic set of features, it must be verified that it has no exploitable bugs)
- Secure component would be responsible for booting target OS after attestation is successful.
With this approach, even if VM got compromised it wouldn't break attestation. Linux VM can't boot another OS, it can only signal secure component to boot the exact OS that has been loaded earlier and nothing more. We avoid a situation when compromised VM performs successful attestation but boots something else.
Also, it could be possible to use Rump kernels instead of Linux VM. Rump is a library kernel capable of running unmodified Netbsd drivers. Usually it is used in Netbsd to test drivers in userspace, however it has been used before to provide drivers for other kernels through the Rumprun project. Please note that it is unikernel which is intended to run in VM, but Rump itself (theoretically) could be adapted to run as CAmkES/seL4 component, eliminating the need for VM.
In case of
CAmkES we can verify the licenses by checking
document on the project repository. It uses standard open source licenses.
In the case of Linux, a minimal distribution will be prepared that meets the requirements of the Fobnail Project. Yocto Project will be used for this, because it gives a lot of freedom in manipulating the elements that make up the target system.
Running in DLME
Ensuring that the operating system works in DLME can be achieved by using the TrenchBoot project. For this purpose, a Yocto meta-fobnail layer has been created that integrates the necessary elements. The effects of the tests are presented in a separate document.
At this point, the Fobnail Attester application is strongly dependent on Linux. Mainly due to the fact that its development took place on this operating system. Therefore, it is important that the created minimal OS also has an integrated attester application. The main dependencies of its operation are drivers for USB, USB EEM and TPM, but running them under Linux will not cause major problems.
The Linux Kernel runs under GPL-2.0 License which can be checked in documentation.
Linux with Busybox userspace
The main advantage of Busybox based userspace is its small size. Also booting time would be significantly faster than userspace with fully-featured init system. With Busybox, init system can be replaced by a simple shell script.
Running in DLME
Since we are still running Linux, there are no problems here.
Since busybox based userspace doesn't have big expectation of Linux feature set,
kernel can be reduced. Busybox can be compiled with only those features we need.
Currently, Fobnail Attester depends on another program to configure network
interface created by Fobnail Token. This is
systemd-networkd, but in Busybox
userspace it would have to be something else. It should be noted that
configuration should be done on hotplug event, simply using
ifconfig may be
- It won't work if Fobnail Token isn't already plugged in.
- It won't work if Fobnail Token is plugged out and back in.
Hotplug detection and interface setup could be implemented in Fobnail Attester through Netlink.
Linux with Go userspace
u-root provides an easy way to deploy Go programs as standalone initramfs images. It is used by the LinuxBoot project for creating small Linux distro that acts as bootloader for other OSes (through kexec).
Running in DLME
Since we are still running Linux, there are no problems here.
Fobnail Attester is written in C,
and it rather doesn't make sense to integrate it with Go userland. Also, it
should be noted that
u-root built initramfs contains only executable - all Go
modules are linked into a single binary. Unless we want to rewrite Fobnail
Attester there is no point in using userspace that was designed be Go-only.
Rewriting Fobnail Attester in Go may give benefits of producing less vurnelable
Little Kernel / Trusted Little Kernel
Little Kernel is a small, embedded monolithic kernel that runs on x86, ARM and RISC-V among others, provides a custom very basic libc. LK focuses on ARM platforms and lacks drivers for devices typically found in x86 platforms. LK has been used as a base for aboot (Android bootloader) and Fuchsia OS.
Trusted Little Kernel (available at
https://nv-tegra.nvidia.com/r/3rdparty/ote_partner/tlk.git, not accessible
through web browser - must be cloned with
git) is a fork of LK intended to be
run as TEE OS. It is developed by NVIDIA for Tegra platforms, support for all
other platforms has been removed.
Running in DLME
LK boots over Multiboot 1 which is not supported by SKL. The problem is similar to that with Zephyr (see Zephyr section for detail). However Multiboot2 support could be added.
Running Fobnail Attester on LK would be problematic to say the last and the reasons for that are:
- LK lacks most drivers including USB host drivers (UHCI, OHCI, EHCI, XHCI), USB EEM driver and TPM drivers.
- Lack of cryptographic library in LK. TLK does provide one (potentially could be).
- Default C library is too much constrained - provides only most basic API like string operations, printing, etc. lacks anything more complex, including networking support, there is a LK's fork of Newlib, however of unknown quality.
- TCP/IP is provided by
miniplibrary (which is part of LK), attester depends on
libcoap3which either would have to be ported to
minipwould have to be integrated with
- LK has no suitable bootloader capabilities lkboot could serve as reference to develop custom bootloader.
Little Kernel uses MIT License.
Fuchsia is a general-purpose OS developed by Google. Its purpose is to replace GNU/Linux in Google products (like Android, Chrome OS) with Zircon microkernel (used to be known as Magenta) and custom userland. Fuchsia runs on x86-64 and ARM64. There used to be an unofficial RISC-V port, however it has been unmaintained for years. Support for 32-bit architectures was dropped some time ago.
Zircon is based on LK, however similarities between these two are small and constantly decreasing. LK is a kernel intended for embedded usage, while Zircon is a general-purpose microkernel that could compete with Linux.
Running in DLME
Historically Zircon used Multiboot 1 for booting. Now it uses ZBI with a UEFI bootloader called Gigaboot. Multiboot 1 support is still present, but SKL doesn't support it anyway. See Zephyr section above for details.
Fuchsia provides a Unix-like environment with musl C library. Network is
available but there is no EEM driver, and only XHCI host driver is supported.
Since EHCI is still widely used, this is a major limitation. TPM driver is
available but without
Zircon has a kexec-like capability which allows to boot another Zircon instance.
This is known as
Following things would have to be done:
libtss2stack to Zircon.
- Bring EEM driver. There is ECM driver available, which could serve as reference.
- Bring at least USB EHCI driver, ideally should support UHCI and OHCI too.
- Figure out how to use
mexecto boot Linux.
Information can be checked here. Basically, we will be using here components under MIT, BSD and Apache 2.0 licenses.
Xen is a bare-metal hypervisor available on x86 and ARM. It is able to run Linux in a paravirtualized environment. Xen contains only drivers absolutely necessary for hypervisor and VM to boot. Control over most of the hardware is handed to the first VM known as Dom0. Usuallly Linux runs in Dom0, there are other OSes which also support running in Dom0 (BSD, Solaris), however there is no advantage of using them over Linux. Xen also has ability to run in dom0-less mode - bootloader provides VM images and Xen starts VMs on their own (see section below for details).
Running in DLME
Xen is supported by Trenchboot's GRUB and can run without any modifications. See xen-in-dlme.md for demo.
Integration with Fobnail
Domain 0 less mode eliminates need for trusted VM. Also, since Xen itself is responsible for booting multiple VMs there is no need for tools that manage Xen (which don't work on any OS besides Linux). Fobnail Attester could be integrated in a similar way that with CAmkES based VM (see CAmkES section above for details). The main difference would be that the secure component would be a separate VM.
So it look like we could use Xen while we talk about early launch but in late launch scenarios it makes no sense. And this is one of key reasons why Xen does not meet the minimal OS requirements, because implementing late launch scenarios is definitelly something that we would like to achive with the OS.
Xen Project is developed under GPL-2.0 License.
- The above report outlines 8 operating systems that should be considered candidates for Fobnail Token interoperability.
- The basic choice is Linux, the operating system based on it is created with the use of Yocto Project. All achievements can be reproduced at any time using the meta-fobnail layer.
- As part of the report, other systems were also checked. The possibility of running them in DLME and the integration of the Fobnail Attester application was checked for each of them.
- The description of an attempt to run Zephyr on PC Engines apu2 in order to verify the current state of the system to work with Fobnail Token has been included. The effects are described in the PoC test section.
- The table below contains summary of features of all OSes together with theirs scores. Please note that when comparing driver support we take into account not only drivers which are part of the kernel, but also available userspace drivers. Each score is computed using the following rules:
- if feature is present then +1,
- if feature is not present then 0, or if feature would be hard to implement then -1,
- if this is a hard requirement then multiple result by 2.
Definition of requirements can be found here.
|OS||USB host driver||USB EEM driver||Network stack||TPM driver||OS portability||Bootloader capabilities||C library||Microkernel||CPU Architecture support||Bootable by SKL||License||Score|
|Zephyr||Yes (+2)||Yes (+2)||Yes (+2)||PoC available (0)||Limited (-1)||No (0)||Yes (+2)||No (0)||Good (+1) [^4]||No (0) [^6]||OK (0)||8|
|Xous||No (0)||No (0)||Yes (+2)||No (0)||Limited (-1)||No (0)||No (0)||Yes (+1)||RISC-V only (-1)||No (0)||OK (0)||1|
|seL4||No (0) [^1]||No (0) [^2]||Yes (+2)||No (0)||Limited (-1)||No (0)||Yes (+2)||Yes (+1)||Good (+1) [^3]||Yes (+2)||OK (but problematic with Genode) (0)||7|
|Linux||Yes (+2)||Yes (+2)||Yes (+2)||Yes (+2)||Yes (+1)||Yes (kexec) (+2)||Yes (+2)||No (0)||Good (+1) [^5]||Yes (+2)||OK (0)||16|
|LK||No (0)||No (0)||Limited (-2) [^7]||No (0)||Yes (+1)||No (0)||Limited (-2)||No (0)||Good (+1) [^8]||No (0)||OK (0)||-2|
|Fuchsia||Limited (0) [^9]||No (0)||Yes (+2)||Limited (0) [^10]||Yes (+1)||Yes (mexec) (+2)||Yes (+2)||Yes (+1)||Good (+1) [^11]||No (0)||OK (0)||7|
[^1]: seL4 has an old unmaintained driver with no xHCI support. Better driver is available only from Genode.
[^2]: available from Genode only
[^3]: supports x86, ARM and RISC-V
[^4]: supports x86, ARM, RISC-V, SPARC and MIPS
[^5]: supports most of the architectures, much more than any other OS listed here
[^6]: not bootable due to of lack Multiboot1 support in SKL
[^7]: uses custom library, no integration with libc, which complicates using it
[^8]: supports x86, ARM, RISC-V and MIPS
[^9]: supports XHCI only
[^10]: TPM driver is present but there is no
[^11]: supports 64-bit x86 and ARM. Support for 32-bit architectures has been dropped a while ago and is not coming back
We want to thank the people listed below for their help in this research (listed alphabetically).