Re: [seL4] UX/RT - an seL4-based OS in the style of QNX and Plan 9

Cool and challenging project! You might want to look at Cogent for writing file systems. Naive question: Why stick with the Unix model, which is a bit dated by now, especially the coarse-grain protection model that ACLs provide (and that lead to inevitable problems, such as confused deputies)? Gernot

On 3 Sep 2017, at 19:14, Andrew Warkentin wrote:

I mentioned this here earlier, but I haven't really gone into a lot of detail about it here. I am planning to write an seL4-based OS similar to QNX and Plan 9 called UX/RT. I am intending it to be both an embedded OS (mostly for the larger types of embedded systems where QNX or Linux would be used, as opposed to simpler ones) as well as a desktop OS. I plan to use as much third-party code as possible to avoid making lots of extra work (likely LKL https://github.com/lkl/linux and/or the NetBSD rump kernel for device drivers, disk filesystems, and the network stack; a libc based on musl; and basic commands forked from those of FreeBSD). UX/RT will be a pure Unix-like system with no concept of "personality-neutral" services, and the root server will implement a subset of the Unix API directly (as in QNX, although the root server will be completely separate from the kernel of course, unlike that of QNX). However, there will be a Linux compatibility layer implemented with libraries and filesystem servers. I am going to avoid C for new code as much as possible for security, preferring Rust for anything performance-critical.

The main concept behind the design will be to take "everything is a file" as far as it possibly can go. Nearly all resources in the system will appear in the filesystem, even things like process memory (kernel memory and the interface to the root server will be among the few non-files in the system, although the API of the root server will be implemented with an anonymous FD internally). The filesystem will be a combination of a thin layer on top of L4 IPC with read() and write() calling L4 IPC directly (short transfers will probably be sent entirely in message registers and long ones sent by using shared pages), and a memory mapping layer. The VFS will implement the name service and memory mapping parts of the filesystem; read() and write() will bypass the VFS layer entirely and will use seL4 IPC to communicate directly with the other thread. There will also be APIs that expose message registers and shared pages more directly although they will do it in a way that interoperates with read() and write() (these will mostly be used with a new "message-special" file type that preserves message boundaries but otherwise acts like a normal byte stream if used with read() or write()). No provisions will be made for use of IPC or capabilities outside the filesystem.

Security will be based on an ACL-per-process model, where the root server will have an in-memory list of files for each process specifying which files it is allowed to access, as opposed to a hierarchical pure-capability model like other L4-based systems (a pure capability model seems like it would be a poor fit for a pure Unix-like system). It will be possible to either specify rwx permission bits explicitly or use the mode from the filesystem; it will also be possible for an ACL entry to specify all files under a particular directory. File descriptors will be implemented as groups of capabilities, and the root server will hand them out when a process successfully opens a file (unlike in QNX there will be no need for individual filesystem servers to check whether the client process is authorized to access a file). There will be an ACL management server that will persistently associate permissions with programs, and it will also be possible for sufficiently privileged processes to dynamically modify the ACLs of other processes.

I currently have a bootloader, some basic infrastructure for building boot ISO images, and a patch for seL4 to support QNX-like XIP single-image boot using a variant of Multiboot2. I can build a boot ISO with a system image containing only the kernel, but it crashes with a triple fault somewhere in either the bootloader or the kernel (I haven't yet tried to track down where it's occurring). Once I move on to user mode code, I'm going to be using the Rust libraries from Robigalia as a basis for the root server (higher-level Rust-based components will use a normal Unix build of the Rust standard library instead).

The code I have so far can be found at https://gitlab.com/uxrt for UX/RT itself and https://gitlab.com/uxrt-bos for the bootloader. I have some (long and not particularly well-organized) notes on my plans for UX/RT's architecture at https://gitlab.com/uxrt/uxrt-toplevel/blob/master/architecture_notes. Anybody is more than welcome to contribute if they want.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel