1 - 3 September | Vancouver, Canada BC View More Details & Registration The schedule is subject to change, so please check back before the event for the most up-to-date information.
Please note that all session times are listed below in Pacific Daylight Time (PDT), UTC-7.
Sign up or log in to add sessions to your schedule and sync them to your phone or calendar.
In its current form, the initialization code of the seL4 kernel dictates the policy of how resources are discovered and what capabilities are created at boot time, making it hard to integrate into existing boot infrastructure. Wepropose to delegate this policy to a pre-boot component and introduce both an interface and mechanisms for pre-boot infrastructure to communicate resources to the kernel and userspace. Not only does this pave the way for booting seL4 in a multikernel configuration where not all the nodes use the same resources, it also provides a cleaner separation between verified and unverified code.
Contrary to the rest of the design of seL4, the boot code makes several policy decisions. On x86 for example, the kernel expects to be booted in protected mode. This is the case when loaded with GRUB. All modern server platforms have an EFI pre-boot environment, which leaves the CPU already in long mode (Intel-speak for 64bit mode). On Arm platforms the physical memory regions are extracted from a device tree at compile time. While device trees are the standard for embedded systems, Arm server platforms also use EFI, which provides a memorymapthatisonlyknownatruntime. Thingswillget even morecomplicated with partitioned multikernel configurations, where the resources of the nodes need to be disjoint, and the global memory map provided by the firmware does not have enough information for the kernel to create the right capabilities. In such a setting, there will also be shared frames that userspace components use to communicate between cores. These are resources that the kernel does not touch but should just be passing to userspace. Currently, the seL4 ecosystem does not have a mechanism to pass resources at addresses that are not statically known to userspace.
One could of course add support to the kernel for all these cases that currently are not covered. We however argue, that like any other policy, a microkernel should not make these decisions but offer a mechanism that is general enough to cover all potential use cases. We therefore propose to remove all code that decides which resources are used by the kernel and what capabilities are created from the initialization of the kernel. Instead, the kernel should be getting this information from a pre-boot environment that can be tailored to specific use cases. We therefore propose a boot protocol where the kernel expects to be handed a resource map. To cover the case of pre-boot allocated resources that need to be passed to userspace, we propose to add support for named resources to CapDL. A statically created specification can e.g., specify a specific slot in a CSpace to be populated with a capability to such a resource. The rootserver will then get a mapping from these names to CPointers from the kernel and can distribute the capabilities accordingly.
An additional benefit of this approach is that the clear interface between the verified kernel and the pre-boot interface makes it easier to specify what the state is that the kernel expects to be booted in. By shipping default pre-boot environments that recreate the current initialization code, the transition to making seL4 an even more versatile tool than it already is, can even be seamless.
