I'd like to see someone re-implement the QNX real-time microkernel in Rust. That would be useful. We need a QNX-like OS for embedded devices. Linux is really the wrong tool for the job. Too much extra stuff which allows attacks.
I agree. That or at least MINIX 3's core components as there's already source available. Plus, that would likely get extended by all the people building servers and stuff. Be two versions like with Linux.
seL4 is quite good, but their approach to message passing has a problem. Messages are limited to a few bytes passed in registers. Anything bigger has to be done through shared memory between processes. This is great for the kernel; it never has to do a long operation like a big copy, so there's an upper bound on the time for each kernel operation. But with shared memory, one process may be able to mess up another. The usual library for L4 shared memory puts multiple "chunks" into one shared memory area, with an allocator. "A shared memory area can have multiple chunks."[1] Messing with the chunk structure or the wrong chunk from one process may adversely affect another one. That's a bad kind of attack surface.
So, although the kernel is secure, server processes with higher privileges than their callers may not be. Since this is how processes talk to file systems and drivers, it's an obvious way to attack.
QNX copies data from one process space to another. This adds copying overhead, but it's usually not too bad, because 1) most messages are short, and 2) if you just created a message and sent it, it's in the cache. In practice, the big overhead item today is context switching.
Do you think anything could be done to mitigate or fix that? I've only recently started digging into seL4 so I don't know if this is an unavoidable problem (in terms of proving correctness) or if it even needs to be solved in-kernel.
I asked, both before QS sold it to RIM and after the deal, in both cases I didn't even get an answer (and I would have been in a position to put up a substantial chunk of money in order to get a dual license deal in place). Real pity, but maybe it will still happen.
QnX is one of the most elegant OSs out there and having a public domain or GPL'd version of it would be a great thing.