On 11/5/18, Anna.Lyons@data61.csiro.au
The boot code of seL4 is currently unverified, but we do have ambitions for verification in the future. As such, we'd want to keep a minimal, static boot environment. That said, we'd be more than happy to take a look at any patches you have in more detail.
My patches make relatively minor changes and probably wouldn't break any future boot code verification efforts.
I'm curious as to why you need to place your desired functionality into the boot loader, rather than at user level in a root task or some kind of chain loader? How much trust is placed into your boot loader?
UX/RT will be a full self-hosting general-purpose OS that runs on workstations/servers as well as embedded systems, and the components required at boot will be split across several deb packages (except for minimal embedded systems without dpkg), so the boot image will be rebuilt any time any included package is installed/upgraded. I want to keep the image building process as simple as possible (think Linux initramfs) and don't want to have to include a linker on every system just to link the boot modules into the root server. I want to be able to treat the kernel and root server as normal files that are placed at fixed physical addresses within the filesystem image (much like QNX does), since that is simpler than having to link the modules into the root server and then possibly update a bootloader configuration file. Also, as I said before, it is more convenient to manually boot an image for recovery or testing if you just have to specify one file rather than two (and basically guarantees that you're not accidentally booting a mismatched kernel and root server). The changes I made (only on x86/PC, which is the initial development platform; once I port UX/RT to ARM and RISC-V I will port the Multiboot2 code to those platforms): - Perform a few bounds checks on the boot FS image (a module tag for the whole image with a different type code is created by the bootloader) - Disable boot module relocation if an FS image is present (the image specifies a starting physical address in its headers and is already placed there by the bootloader, and the kernel and root server are already placed at the proper addresses within the FS image) - Accept a root server module that's already been ELF-loaded by the bootloader, much like what the elfloader does on non-PC platforms (with an extended module tag specifying the section placement) - Create a new extra boot info structure specifying the address of the MBI, which is required to follow the boot FS image - Replaced the magic numbers in the Multiboot2 header assembly with proper symbolic constants, just like for the Multiboot1 header No parsing of the boot image FS is added to the kernel and any format will work as long as files are contiguous and page-aligned (the UX/RT root server is also completely independent of the boot FS format as well, and will create an initial filesystem for the init process out of the Multiboot modules, and a normal user program will mount the image filesystem to get access to the full image FS contents and full Unix FS features). The existing boot code paths are not disabled (although I may add CMake configuration options to disable them).
When you say "implement a full disk-based bootloader" -- this would be at user-level, right? We definitely don't want to have to trust disk drivers to boot seL4 + the root task.
My disk-based bootloader will be comparable to GRUB or syslinux/isolinux (except more Unix-like than either). The kernel won't have to trust it any more than those bootloaders.
Our current image format (cpio) is one picked for convenience/simplicity and we'd be more than happy to consider proposals for a different format. MBI passthrough is a desirable feature.
I am not using CAmkES or CapDL at all (my root server is written in Rust and is based on feL4 and some code forked from Robigalia), so I am not using your cpio code. Since the existing boot code paths are still functional, non-UX/RT OSes don't have to change their boot code even with my patches in place. If other OSes want to change their boot code for commonality with UX/RT they can, but there's no reason why they have to (except maybe to make it easier to implement some form of limited UX/RT-compatible environment based on CAmkES, for systems where UX/RT would be overkill). UX/RT is a rather different type of OS than any other seL4-based system (it will be the only QNX-like L4-based OS ever written AFAIK; I've always wondered about why nobody else has written one, since the L3/L4 microkernel family and especially seL4 has several similarities with the QNX microkernel) and has its own requirements for the boot process that may not be priorities for other systems. Here are my patches for the seL4 kernel (the first is the main one and the second just cleans up a couple things I missed in the previous patch): https://gitlab.com/uxrt/core-supervisor/sel4-kernel/commit/a21acf9b74b41ce63... https://gitlab.com/uxrt/core-supervisor/sel4-kernel/commit/684c75cd22b6df62d... Here are the repositories for my bootloader (it is currently in-memory only): https://gitlab.com/uxrt-bos/mb2_loader https://gitlab.com/uxrt-bos/multiboot2_lib And here is the top-level repository for UX/RT (currently all the root server does is print hello world; I'm currently working on importing some of the bootinfo code from Robigalia): https://gitlab.com/uxrt/uxrt-toplevel