1 Oct
2018
1 Oct
'18
6:26 p.m.
For UX/RT <https://gitlab.com/uxrt/>, the seL4-based OS I am writing, I
have patched seL4 to support for booting from an in-memory execute-in-place
filesystem image that contains the kernel and all user-mode programs
required to mount the root filesystem (similar to that of QNX, but
with more of the
functionality in the bootloader rather than the root server). The existing
seL4 boot process may be OK for static embedded systems that are always
cross-compiled, but UX/RT is going to be a dynamic general-purpose OS with
a boot image that will include files from multiple
separately-installed packages and
will possibly be customized to the system it is installed on.
Requiring any image
filesystem to be linked into the root server makes updating boot images
more complex than being able to use a simple filesystem builder to make an
image containing the kernel, root server, and everything else that is
required (the main special considerations being placing the kernel and root
server at fixed physical addresses and padding the image to allow for bss
sections, which are easy enough). Also, I want it to be easy to manually
boot UX/RT images, so you can just type something like "boot
(hd0,0)/uxrt.boot" (much like manually booting NetBSD, OpenBSD, or most
older Unices), and the bootloader will automatically load the kernel and
all required modules from within the image as opposed to having to type a
lot of boilerplate to load the kernel and root server (and anything else
that may be required). In addition I don't think that the root server
should need to have any support for parsing image filesystems and
should be able to obtain all the files required for early boot from
the MBI.
I am using Multiboot2 with a few custom tags added and a few extra
requirements regarding placement of modules. I currently have an
in-memory loader that implements my variant of Multiboot2, and
eventually want to
implement a full disk-based bootloader. I have also implemented a
page-oriented in-memory filesystem called XRFS (originally based on
Linux romfs) with support for placing files at fixed addresses. The
in-memory loader was parsing the filesystem and using a script to
locate the modules within the image, although I have decided that it
is overkill to do that, and it would allow the loader to be simpler if
the filesystem image has its own MBH separate from that of the kernel
(the magic number will be different from the kernel MBH as well), with
tags for the kernel and each module, so that the loader's existing
MBH-parsing code can be used to locate files in the image.
As far as my kernel patches go, they extend the existing Multiboot2
code and do not interfere with the existing boot code. Right now they
are x86-only, but I am planning to add Multiboot2 support to other
architectures eventually as well. They do not introduce any dependency
on my filesystem format in the kernel (it does know that there is an
FS image and that there are modules contained within it, and assumes
that modules are contiguous). Relocation of the root task is disabled
when an FS image is present, since it will already be placed in a
usable location in the image. Kernel-level ELF loading of modules is
also disabled when using my Multiboot2 extensions, since my loader is
capable of parsing ELF modules, loading them, and passing information
on module sections and addresses to the kernel through tags. The part
of the image containing the kernel is inaccessible to the root task
for obvious reasons, so an additional requirement is that the kernel
is the first file in the image, followed by the root server, and then
all other files (XRFS is structured to allow the remainder of the
image to be read even though the beginning is inaccessible). There is
also support for passing the MBI through to the root task, which
requires that the MBI is allocated immediately after the end of the
filesystem image (a new structure is added to the bootinfo to provide
the root server with the address of the MBI).
From what I've said, would there be any problems
with including my
patches in the mainline seL4 repository? Only the boot code is
modified. Loading the root server works, but I haven't yet tested the
MBI passthrough, so I am not quite ready to submit anything (currently
I am working on converting my bootloader from parsing the filesystem
itself to parsing an MBH in the FS image, like I said before).
6 Nov
6 Nov
9:57 a.m.
Hi Andrew,
Sorry for the late reply on this one!
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.
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?
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.
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.
Cheers,
Anna.
________________________________________
From: Devel <devel-bounces(a)sel4.systems> on behalf of Andrew Warkentin
<andreww591(a)gmail.com>
Sent: Monday, 1 October 2018 6:26 PM
To: devel(a)sel4.systems
Subject: [seL4] Support for QNX-like booting from an XIP filesystem image
For UX/RT <https://gitlab.com/uxrt/>, the seL4-based OS I am writing, I
have patched seL4 to support for booting from an in-memory execute-in-place
filesystem image that contains the kernel and all user-mode programs
required to mount the root filesystem (similar to that of QNX, but
with more of the
functionality in the bootloader rather than the root server). The existing
seL4 boot process may be OK for static embedded systems that are always
cross-compiled, but UX/RT is going to be a dynamic general-purpose OS with
a boot image that will include files from multiple
separately-installed packages and
will possibly be customized to the system it is installed on.
Requiring any image
filesystem to be linked into the root server makes updating boot images
more complex than being able to use a simple filesystem builder to make an
image containing the kernel, root server, and everything else that is
required (the main special considerations being placing the kernel and root
server at fixed physical addresses and padding the image to allow for bss
sections, which are easy enough). Also, I want it to be easy to manually
boot UX/RT images, so you can just type something like "boot
(hd0,0)/uxrt.boot" (much like manually booting NetBSD, OpenBSD, or most
older Unices), and the bootloader will automatically load the kernel and
all required modules from within the image as opposed to having to type a
lot of boilerplate to load the kernel and root server (and anything else
that may be required). In addition I don't think that the root server
should need to have any support for parsing image filesystems and
should be able to obtain all the files required for early boot from
the MBI.
I am using Multiboot2 with a few custom tags added and a few extra
requirements regarding placement of modules. I currently have an
in-memory loader that implements my variant of Multiboot2, and
eventually want to
implement a full disk-based bootloader. I have also implemented a
page-oriented in-memory filesystem called XRFS (originally based on
Linux romfs) with support for placing files at fixed addresses. The
in-memory loader was parsing the filesystem and using a script to
locate the modules within the image, although I have decided that it
is overkill to do that, and it would allow the loader to be simpler if
the filesystem image has its own MBH separate from that of the kernel
(the magic number will be different from the kernel MBH as well), with
tags for the kernel and each module, so that the loader's existing
MBH-parsing code can be used to locate files in the image.
As far as my kernel patches go, they extend the existing Multiboot2
code and do not interfere with the existing boot code. Right now they
are x86-only, but I am planning to add Multiboot2 support to other
architectures eventually as well. They do not introduce any dependency
on my filesystem format in the kernel (it does know that there is an
FS image and that there are modules contained within it, and assumes
that modules are contiguous). Relocation of the root task is disabled
when an FS image is present, since it will already be placed in a
usable location in the image. Kernel-level ELF loading of modules is
also disabled when using my Multiboot2 extensions, since my loader is
capable of parsing ELF modules, loading them, and passing information
on module sections and addresses to the kernel through tags. The part
of the image containing the kernel is inaccessible to the root task
for obvious reasons, so an additional requirement is that the kernel
is the first file in the image, followed by the root server, and then
all other files (XRFS is structured to allow the remainder of the
image to be read even though the beginning is inaccessible). There is
also support for passing the MBI through to the root task, which
requires that the MBI is allocated immediately after the end of the
filesystem image (a new structure is added to the bootinfo to provide
the root server with the address of the MBI).
From what I've said, would there be any problems
with including my
patches in the mainline seL4 repository? Only the boot code is
modified. Loading the root server works, but I haven't yet tested the
MBI passthrough, so I am not quite ready to submit anything (currently
I am working on converting my bootloader from parsing the filesystem
itself to parsing an MBH in the FS image, like I said before).
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
9:17 p.m.
On 11/5/18, Anna.Lyons(a)data61.csiro.au <Anna.Lyons(a)data61.csiro.au> wrote:
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/a21acf9b74b41ce63391c465229ef0c47a1a2dfb>
<https://gitlab.com/uxrt/core-supervisor/sel4-kernel/commit/684c75cd22b6df62d13665abf3df18605c0d7ef9>
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>
8 Nov
8 Nov
9:11 a.m.
Hi Andrew,
I had a quick look and the changes seem ok on brief inspection, although if you were to
put up a pull request for merging we'd need to do a lot more testing.
As an aside, I encourage you to consider listing your project on our Community Projects
[1] page. We want to provide visibility for our community projects as well as track how
far use of seL4 is going.
Cheers,
Anna.
[1] https://docs.sel4.systems/CommunityProjects.html
1326
days inactive
1363
days old
3 comments
2 participants
participants (2)
-
Andrew Warkentin -
Anna.Lyons＠data61.csiro.au