Comment by ryao
9 days ago
Drivers can crash the rest of the kernel in Windows 7. People playing games during the Windows 7 days should remember plenty of blue screens citing either graphics drivers (mainly for ATI/AMD graphics) or their kernel anticheat software. Second, a “proof of correctness” has never been made for any kernel. Even the seL4 guys do not call their proof a proof of correctness.
Not the operating system:
https://en.m.wikipedia.org/wiki/Driver_Verifier
Driver Verifier is a tool that developers can choose to use for testing and debugging purposes.
It's not used on production machines and it does nothing to prevent a badly written driver from crashing the kernel.
Kernel drivers have to be verified by the driver verifier to pass Windows Hardware Qualification Labs certification and get signed with the Windows signing key that lets them load without warnings. There are fewer outside kernel drivers today, though, because plugging random peripheral cards into PC buses is no longer a big thing.
2 replies →
My PC used to regularly crash Windows 10 because of buggy Nvidia driver. Eventually they fixed the bug, but until then, I had a crash every few days.
From your own link:
"Driver Verifier is not normally used on machines used in productive work. It can cause ... blue screen fatal system errors."
I lost less time to bluescreens than I have to forced updates and sidestepping value add nonsense like one drive, edge.
They didn't "prove the kernel is correct", they built a tool to prove that a single driver maintains an invariant throughout execution.
It does not prove that the driver will not crash the kernel. It should be fairly easy to find a driver that passed QA testing under that tool, yet still crashed the kernel. You just need one of the many driver developers for Microsoft Windows to admit to having used that tool and fixed a crash bug that it missed, and you have an example. Likely all developers who have used that tool can confirm that they have had bugs that the tool missed.