Nebulet: A Rust Microkernel Running WebAssembly In Ring 0

[carewolf]

I am for some reason reminded of this https://xkcd.com/2030/ at least that was my initial reaction

[carewolf]

Second reaction: Is this just a new twist on an exokernel? (a kernal that can load provenly safe user kode into the kernel space and evaluate it there).

[silmeth]

Can someone explain to me why this is only possible with WebAssembly? If I understand it correctly, the WebAssembly language itself does not support reading or writing to memory locations that are not assigned to the application. If that's true, then programs would not have to be checked, because they are safe by design. But the GitHub repo says the WebAssembly code is still verified. Why?

As I understand it security model of WebAssembly is built on binary verification before execution. If your code compiles to correct WebAssembly, it should be safe – but in case something made the final binary unsafe (eg. one manually edited the byte-code or bad compiler was used), the WebAssembly virtual machine is responsible to again verify that it’s a correct wasm program before execution, eg. ensure that all call instructions invoke actually existing functions with corresponding signatures (and not to some arbitrary memory addresses). What cannot be verified statically (eg. dynamically dispatched function calls) have to use different instructions that get run-time checks injected by the virtual machine.

And:
- is WebAssembly seriously the first language to provide this safety?
- does this mean that on a computer running this kernel, the only native program will be the kernel itself, and the rest has to be written in WebAssembly, or interpreted by a program written in WebAssembly?

That’s basically how I understand it, but I’d expect some kind of JIT (or maybe ahad-of-time during installation) compilation to native code. I’d expect the kernel to validate the WASM binary, then run the bytecode directly OR compile it in-memory (possibly with hard-drive caching) to machine code and then run the freshly-compiled native code – so the code is as fast as any native code, but the start-up is slower.

I believe that’s what Android RunTime does (apks are compiled from Dalvik byte code to native ARM or x64 during installation).

[GunpowaderGuy]

silmeth at least until jit support is introduced ( which nebulet devs dont want for the following reason ) , code will always be compilable and verifyable in a one time pass

[VanCoding]

silmeth thanks If that's true, then this is absolutely brilliant and a much bigger thing than one would expcect. I mean this could completely revolutionize how kernels are written. I'm just surprised that it's 2018 and noone had the idea to create a specific programming language that is safe to run in ring 0 alongside the kernel and making any hardware memory protection systems obsolete :/ I hope this gets the attention it deserves!

[paulpach]

This is very similar to Singularity, the research project from Microsoft to write a kernel that runs managed code in kernel space and avoids context switches.

Essentially the isolation between processes is done by software, not hardware. When code is loaded, it is JIT compiled. The JIT and verifier guarantee that the process wont touch memory it is not allowed to.

[silmeth]

silmeth at least until jit support is introduced ( which nebulet devs dont want for the following reason ) , code will always be compilable and verifyable in a one time pass

So, validation and compilation at each start of the binary? Will add some start-up overhead, but sounds reasonable, keeps safety and still the final running code is a fast native one.

Oh I see it even mentions the compiler used in the README:

The Cranelift compiler is used to compile WebAssembly to native machine code. Once compiled, there are no complex interactions between the application and the runtime (unlike jit compilers, like v8) to reduce surface area for vulnerabilities.

[pabloski]

I'm just surprised that it's 2018 and noone had the idea to create a specific programming language that is safe to run in ring 0 alongside the kernel and making any hardware memory protection systems obsolete :/ I hope this gets the attention it deserves!

There were several experimental projects that tried it. Singularity/Midori, JavaOS, CosmOS ( this one is alive ). Everyone of them has failed because:

1. you need a complex virtual machine ( a lot of code that runs in ring 0 and creates a big attack surface )
2. performance are subpar in respect to hardware switching in normal ( and even micro ) kernels

The best paper on the subject has been written by the developers behind OKL4, who have tested Singularity and their OS.

[fuzz]

- is WebAssembly seriously the first language to provide this safety?

WebAssembly isn't a language. It's just an instruction format and compilation target.

[GunpowaderGuy]

pabloski
Also , an alternative to software based memory protection ( which negates the need for rings but incurs in a runtime cost ) and basic software type checking ( https://webassembly.org/docs/security/ ) ; Is proof carrying conde . An structure attached to an untrusted program that is used to verify that it wont fail or commit illegal behavior , that is type safe in a broader sense that includes memory safety . This Is becoming practical because of the rise in popularity of borrow checker and functional based languages which are particularly easy to subject to theorem provers and are safe by default in that aforementioned way