For the past ten years I have been working on a side project which I have taken to call Neptune OS [1], named after the ill-fated Microsoft Windows codename. Neptune OS is a Windows NT-like operating system built on the seL4 microkernel. The project has reached a point where it can run non-trivial, unmodified or minimally modified Windows or Linux kernel drivers as native (ie. NOT in a VM), unprivileged userspace processes on seL4. For instance, here [2] is amdgpu and i915 (from the Linux kernel DRM subsystem) successfully performing mode-setting on Haswell+Radeon RX560 for hotplugged monitors. The linked youtube channel has more demos for storage, networking, and power management drivers.
Why I started working on this and why I think it is interesting:
If you were familiar with early Windows NT development history, you'd probably know that NT was (allegedly) supposed to be a microkernel OS, where system services exist as user-mode servers sitting on top of a Mach-style port-based IPC. Unfortunately the late 1980s' computing technology prevented Microsoft from realizing this vision, and as a result the Windows we see today has everything dumped into kernel space (they even put an HTTP server in kernel mode!), leading to stability and security issues.
This unrealized potential of the NT architecture never sat right to me, so when the seL4 microkernel was open-sourced back in 2014, I immediately thought, well perhaps one could rewrite NT as a personality on top of seL4. This "re-imagined" NT on seL4 will have the NT system call services implemented as a userspace process that talks to client processes via the high performance, formally verified seL4 IPC. Device drivers will then also run in isolated, unprivileged user processes, the crash of which will not lead to a BSOD-inducing full system crash.
Another feature of the NT architecture I find very interesting is its so-called Environment Subsystems. These sit on top of the NT native system call services and expose them as more friendly user-facing APIs, such as Win32 and POSIX. I always thought it was a real shame that Microsoft has essentially given up on this idea and today's Windows is Win32-only (WSL1 being a much-needed redemption, but was then mercilessly dropped). With this seL4 rewrite of NT, I thought I could take this idea one step further and expand these environment subsystems to include device drivers, as they now run in userspace where they should have belonged.
The result is the Linux Driver Subsystem in the latest v0.4 release of the project. In addition to native Windows drivers (which now run in userspace), this subsystem allows unmodified (or very minimally modified) Linux kernel drivers to run as native user processes on seL4. Note these are not virtual machines --- they are just regular, unprivileged processes. More technical details can be found in the mailing list announcement [3], but the basic idea is to add a new arch port to the Linux kernel similar to that of UML and the lkl (Linux-kernel-as-a-library) project. When compiled for this architecture, a reduced Linux kernel binary will essentially run as a regular program, requesting resources from the underlying host OS via the seL4 IPC. This binary communicates with the host OS via a carefully defined interface, which is in fact not tied to seL4 specifically, meaning our work can potentially be reused for other NT-like OSes (including Windows itself), or even other non NT-like OSes (with some more effort).
Anyway, if you have read this far, I hope you find this project interesting. What do you think? What kind of applications do you think Neptune OS can potentially have? Do you think the project has sufficient industrial relevance to go beyond a hobby operating system? Let me know in the comments below.
Why I started working on this and why I think it is interesting:
If you were familiar with early Windows NT development history, you'd probably know that NT was (allegedly) supposed to be a microkernel OS, where system services exist as user-mode servers sitting on top of a Mach-style port-based IPC. Unfortunately the late 1980s' computing technology prevented Microsoft from realizing this vision, and as a result the Windows we see today has everything dumped into kernel space (they even put an HTTP server in kernel mode!), leading to stability and security issues.
This unrealized potential of the NT architecture never sat right to me, so when the seL4 microkernel was open-sourced back in 2014, I immediately thought, well perhaps one could rewrite NT as a personality on top of seL4. This "re-imagined" NT on seL4 will have the NT system call services implemented as a userspace process that talks to client processes via the high performance, formally verified seL4 IPC. Device drivers will then also run in isolated, unprivileged user processes, the crash of which will not lead to a BSOD-inducing full system crash.
Another feature of the NT architecture I find very interesting is its so-called Environment Subsystems. These sit on top of the NT native system call services and expose them as more friendly user-facing APIs, such as Win32 and POSIX. I always thought it was a real shame that Microsoft has essentially given up on this idea and today's Windows is Win32-only (WSL1 being a much-needed redemption, but was then mercilessly dropped). With this seL4 rewrite of NT, I thought I could take this idea one step further and expand these environment subsystems to include device drivers, as they now run in userspace where they should have belonged.
The result is the Linux Driver Subsystem in the latest v0.4 release of the project. In addition to native Windows drivers (which now run in userspace), this subsystem allows unmodified (or very minimally modified) Linux kernel drivers to run as native user processes on seL4. Note these are not virtual machines --- they are just regular, unprivileged processes. More technical details can be found in the mailing list announcement [3], but the basic idea is to add a new arch port to the Linux kernel similar to that of UML and the lkl (Linux-kernel-as-a-library) project. When compiled for this architecture, a reduced Linux kernel binary will essentially run as a regular program, requesting resources from the underlying host OS via the seL4 IPC. This binary communicates with the host OS via a carefully defined interface, which is in fact not tied to seL4 specifically, meaning our work can potentially be reused for other NT-like OSes (including Windows itself), or even other non NT-like OSes (with some more effort).
Anyway, if you have read this far, I hope you find this project interesting. What do you think? What kind of applications do you think Neptune OS can potentially have? Do you think the project has sufficient industrial relevance to go beyond a hobby operating system? Let me know in the comments below.
[1] https://github.com/cl91/NeptuneOS [2] https://youtu.be/BJIrUZIGgBc [3] https://lists.sel4.systems/hyperkitty/list/devel@sel4.system...