Comment by TheLoneWolfling | Hacker News Reader

Comment by TheLoneWolfling | Hacker News Reader

TheLoneWolfling

This is slightly tangential, but ah well.

Thinking of a hypothetical OS here. As much of the OS as possible, and all userland components are bytecode. This bytecode is split into two categories - "safe" bytecode, where none of the operations could cause issues (read: runtime arrays bounds checks, that sort of thing), and "unsafe", which includes a formal proof of "correctness" - that is, a formal proof that it doesn't access memory it hasn't initialized, etc, which the compiler checks for correctness. (Note: the kernel does not do any attempt at making a proof, "just" checking it) The kernel compiles bytecode to machine code before execution, with caching as appropriate (similar to how Python handles compilation, for example).

The advantage here is that you can end up running native code everywhere (and also potentially not having to worry about usermode <-> kernel switches, memory segmentation, etc), without having to worry about malicious code. Also, it'll be a lot easier to port. Yes, it's going to be slower. (Although some of that may be offset by lack of context switches and not having to be paranoid about kernel arguments, etc. Considering that the attack surface is small ("just" the bootstrap code and bare-bones HAL), it may be possible to just run everything in ring 0 / cooperative multitasking / flat memory model.)

This OS isn't completely hypothetical--what you describe is similar to the design of Singularity OS, a (now-dormant?) project at Microsoft Research. Large parts of the OS were written in managed code (related to C#), and programs did require proofs that certain invariants were maintained. As you say, most (all?) code was run in ring 0, with security maintained by software rather than hardware.

http://en.wikipedia.org/wiki/Singularity_(operating_system)

This is exactly how Windows' device drivers work. What you are asking for is the same functionality be extended to userland programs.

The primary problem for this is proof generation. Programming paradigms where proofs are easy to generate would be too limiting. So, although we gain security, our flexibility is tarnished.

Again, "safe" versus "unsafe" bytecode. The "safe" code does all of the checking at runtime. Effectively: write code mainly in "safe" code, or code that compiles down to "safe" code, with your compiler doing as many optimizations from "safe" to "unsafe" code as it can. It's only when you're trying to optimize for speed / ensure correctness that it becomes necessary to write "unsafe" code.

So if your compiler to bytecode has issues with generating proofs, "all" that happens is that the resulting code is slower.

Layers are useful for containing failures. What will happen when you get an undetected memory read error? A precondition of the proofs just left.

Hmm. Yeah, that would be a problem, wouldn't it. There are failures that cannot be proven to not occur at compile time, namely, as you mention, hardware errors. ECC will prevent some of these, but not all. So perhaps it should still be layered at the hardware level.

(Reminds me of the JVM exploit that relied on waiting for random bitflips in RAM.)

(Of course, this is a problem for traditional OSs as well, although the vulnerable area of memory (ring0 data structures / stack / etc) is smaller.)

I wonder. It might be possible to express some of that in the proof requirements - "this program must not write to memory owned by another process even if a single bitflip occurs anywhere" - although that would probably balloon the complexity of the proof.

Reply on news.ycombinator.com