On 2017-03-03 16:23, Moritz Maxeiner wrote:
That would be a good next step from an engineering standpoint, I agree, to proceed to minimize the amount of trust in people you need to have vs verifiable safety. I have considered porting something like seL4[1] to Rust, but ultimately this would take a significant amount of time and even if done you'd then have the biggest problem any new kernel faces: Hardware support. Driver development is AFAIK mostly done by people working for the hardware manufacturer and you're going to have a hard (probably closer to impossible) time convincing them to spend money on driver development for you. And if they don't you'll have close to 30 years of hardware support to catch up on by yourself. But suppose you limit yourself to a single (or at most a handful of homogeneous) platform(s) like [2], e.g. a new AArch64 board. Suppose you even take one where the hardware is open so you can audit its schematics, then you'll *still* either have to use proprietary firmware for the (partially onboard) periphery (and have unsafe interfaces to them), or - once again - write all the device firmware yourself. And once you've done all of that you're still missing userspace, i.e. you have a nice new OS without any actual use for it (yet). So you either start writing your own incompatible, safe userspace, or you're going to decide to integrate the userspace of existing OSs (probably POSIX?) to your new OS, so you're going to be writing your own (safe) libc, (safe) pthread, etc, exposing (once again) unsafe APIs to the top. It will be safer than what we currently have on e.g Linux since you can probably make sure that unsafe use of them won't result in kernel exploits, though; this will, of course, take even more time. Finally, at the arduous end of your journey you're likely going to notice what - in my experience - most new OSs I've observed of the years experience: Essentially nobody is interested in actually switching to a volunteer-based OS. Honestly, I think you need serious corporate backing, a dedicated team, and like 5-10 years (low estimate) of guaranteed development time to have a snowballs chance in hell to pull this off and the only possible sponsors for this I'm both aware of and would currently trust not to cut you off in the middle are either already working on their own OS[3], or have dedicated their R&D to other things[4].
I agree. The only potential hope I see would be to port Linux to a memory safe language.
-- /Jacob Carlborg
