Secure OS (maybe in Rust?)

MaidSAFE is cool. However, what if your phone or computer leaks everything you type? Or if somebody can read all your files (e.g. mapped memory) remotely?

There are a few projects other than Lifestuff/MaidSAFE that I’ve been losely following over the years, one of which is seL4, the first (and I think still only) formally verified general purpose kernel. It’s tiny, it uses capabilities for access control, it has verified worst case timing properties (it’s a hard real-time kernel), some more goodies, but most of all: and it’s open source – the perfect thing to build a secure operating system around.

Which is exactly what a (joint) DARPA project is about, I think with actual financial support to primarily U.S. owned companies who are willing to work on it. (Please, don’t even start on how impossible it sounds that one branch of the government is trying to build a super secure open source operating system while another branch would hate if something like that existed; governments are inherently schizophrenic.)

(More info here)

Anyway, how about building an OS in Rust? An Advanced OS class in Australia is actually working on it right now, and they are not alone. I wonder, what if I larger community picked these up…

By the way, OKL4, another (closed source) L4 descendant, is used in literally billions of devices around the world, including HTC, LG, Motorola, and Samsung phones, for things like isolating the modem driver from the general purpose OS. All new iOS devices use a version of L4 as well.


You are mixing up OS and kernel.

The OS would gain safety in porting to rust, but i suspect the kernel would not gain anything noteworthy since so many parts would need to be done in UNSAFE RUST.

1 Like

I’d actually be more keen on seeing someone start a SystemV/systemd init alternative in Rust.

1 Like

I’m not sure what you mean here, but I think it might be about the line drawn between the kernel and the rest of the OS, which is very different in a microkernel and a monolithic kernel.

seL4 is a microkernel; it does the very basics, nothing more. Services that are usually part of a monolithic kernel (e.g. Linux) need to be implemented in user space (e.g. in Rust). The good thing about it is that the kernel can enforce isolation between parts of the OS that are not possible in a monolithic kernel. In seL4, even memory management is a user-space function (which allows for very interesting things, just check out Genode.)

Rust, with seL4 in the core, is a perfect candidate to implement the rest of the operating system.


… which of course would need to be part of the effort, eventually.


You are correct. I did not realize the extent of which these microkernels delegate most basic functions to userspace, like memory management.