On Sun, Oct 27, 2019 at 3:56 AM Giovanni Mascellani <[email protected]> wrote:
> I was wondering whether we will ever > have operating systems that do not enforce any more security boundaries > between processes and between the kernel and the processes and map > everything to the same address space at ring 0, because loading each > process the OS verified a proof that that code would never touch > anything outside its assigned space... > I think there will always be a use for ring 3 (userland). Assuming there are no privilege escalation bugs in the hardware (unlikely, I know), it is the *only* way to run arbitrary code with controlled effects. That is, if I have a block of unknown code and jump into it, anything could happen... except that the hardware guarantees that any ring 0 stuff goes through OS syscalls. In short, it is a hardware sandbox. There is no way to achieve the same result without more overhead or more analysis of the code. (Google's Native Client was an interesting middle ground in this area, where "arbitrary" code is executed but it is first validated that all jumps go inside the program, no illegal instructions appear in the instruction stream, and a few other things so that it can sandbox without a runtime overhead.) Of course my programme proposes to prove correctness of "all the code", but as long as there is *any* unverified code on the system you have to be able to protect yourself from it, and that means sandboxing. I mention this briefly in the paper, but that's actually why the verifier is in a separate process; the "small trusted kernel" approach doesn't work unless the language is sufficiently "safe" and restrictive (and verified) that we can prove that "arbitrary" code doesn't trample on the part of the code about which properties of interest are proved (the trusted kernel). If it's in a separate process, then the unverified part of the code can throw whatever tantrums it likes but it won't be able to influence the verified checker without the OS's say-so. (The OS still has to be trusted in this scenario, though.) Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuJRqQHM%2BmQtszsUF5qd9OiV5oxXT9O__HWHY%3DOg%2BGoBQ%40mail.gmail.com.
