How can one ensure security without formal verification of a program that runs in ring0? Could a VM be used without differing userspace kernelspace?
A:
The question is slightly confusing, but I'll do my best to answer.
Running any untrusted code in a privileged mode is unlikely to be "secure" in the sense that most people understand it. As you correctly surmise, however, it is possible to use something akin to a virtual machine in order to moderate the actions which an untrusted process can take within that environment. This is the principle upon which modern "hypervisors" operate - access to the hardware (or memory) is moderated by some piece of "monitor" software or hardware.
That said, if you are taking that approach, it's likely to be the case that formal verification of the virtual machine is highly desirable. Otherwise it seems possible that a maliciously constructed program could find a way to escape from the virtual machine, or make the virtual machine behave in undesirable ways.
A reasonable modern approach to this problem is to use proof carrying code, in which a piece of untrusted code carries with it a machine-checkable proof that it behaves according to some security policy. All the host operating system needs to do at that point is to check the proof against the code (a reasonably computationally cheap operation), and then it is safe to run that code without needing to virtualise it or do any runtime checking.
Gian
2010-07-18 22:00:53