On extremely brief inspection, they avoid a bunch of the problems by not actually running user mode (CPL3) code. That means no SYSRET garbage, no weird IRET states, no SWAPGS, etc.
On the other hand, using virtualization for everything means that you pay a full host/guest switch cost every time you context switch, and that's much more expensive than SYSCALL + SYSRET.
Their exception handler asm looks highly questionable, but maybe they really never have exceptions :)
The point was that they both created models of hardware, software, error states, and so on to use to ensure correctness of the software at every state. They even designed a safer, C variant and compiler to attempt to knock out that risk. Past that, they used microkernels and modular software (esp privileged) to further reduce risk + ease analysis.
So, the takeaway was that whatever code you're looking at better represent what's actually going to happen on the machine when it works and when it doesn't. Bottom-up verification methodologies like the above help to achieve that. Merely coding what you think works and proving that code has no common defects isn't enough.
Comments
On extremely brief inspection, they avoid a bunch of the problems by not actually running user mode (CPL3) code. That means no SYSRET garbage, no weird IRET states, no SWAPGS, etc.
On the other hand, using virtualization for everything means that you pay a full host/guest switch cost every time you context switch, and that's much more expensive than SYSCALL + SYSRET.
Their exception handler asm looks highly questionable, but maybe they really never have exceptions :)
The point was that they both created models of hardware, software, error states, and so on to use to ensure correctness of the software at every state. They even designed a safer, C variant and compiler to attempt to knock out that risk. Past that, they used microkernels and modular software (esp privileged) to further reduce risk + ease analysis.
So, the takeaway was that whatever code you're looking at better represent what's actually going to happen on the machine when it works and when it doesn't. Bottom-up verification methodologies like the above help to achieve that. Merely coding what you think works and proving that code has no common defects isn't enough.