> Microsoft got drivers under control with the Static Driver Verifier, which uses automatic formal proofs of correctness to determine whether a driver can crash the kernel. ... Linux has no comparable technology.
That's a pretty cool idea (also similar to the static verification in NaCl.) Is there a reason one couldn't implement a static verifier for Linux drivers? Would the problem be harder in any sense for Linux, because of e.g. number of exposed kernel APIs? Or could a static verifier "read off" the kernel's API with no manual annotation required?
That's a pretty cool idea (also similar to the static verification in NaCl.) Is there a reason one couldn't implement a static verifier for Linux drivers? Would the problem be harder in any sense for Linux, because of e.g. number of exposed kernel APIs? Or could a static verifier "read off" the kernel's API with no manual annotation required?