Exactly. They'd need to model the correct, known error, and likely error states (eg errata inspired) of the processor. After validating that model, they need to model, test, and implement their kernel operations against it. Only then can we believe its implementation will be bug-free.
At least until another flaw is discovered on Intel's side. ;)
Note: This was approach taken in the FM9001 and Verisoft bottom-up verification programs. Those were for correctness whereas Rockwell-Collin's AAMP7G processor also verified security (eg isolation). Personally, I don't trust anything on x86 as it's too flawed. SPARC would be my choice given it's cleaner, an open standard, and has OSS implementations (eg Gaisler LEON, Oracle T1/T2).
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
Exactly. They'd need to model the correct, known error, and likely error states (eg errata inspired) of the processor. After validating that model, they need to model, test, and implement their kernel operations against it. Only then can we believe its implementation will be bug-free.
At least until another flaw is discovered on Intel's side. ;)
Note: This was approach taken in the FM9001 and Verisoft bottom-up verification programs. Those were for correctness whereas Rockwell-Collin's AAMP7G processor also verified security (eg isolation). Personally, I don't trust anything on x86 as it's too flawed. SPARC would be my choice given it's cleaner, an open standard, and has OSS implementations (eg Gaisler LEON, Oracle T1/T2).
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.