Linux Driver Verification

My opinion is that at present and near future we won't do this. Instead we suggest that a developer checks a driver against a "correct" kernel with which the driver should be compilable.
Nevertheless we should keep in mind such the ability to check statically driver without any compilation and even without all kernel sources at all. However, I don't understand clearly how to do the last.

Why stop at discarding kernel sources? Let's check the driver without its own source code! While I do not understand how to do it as well, with such feature implemented our framework would have an extremely easy-to-use interface!

Requiring a "correct kernel" is not what we do. We want the program to be built, and we watch the build process closely to extract the build commands from it. Without these commands, it's impossible to tell what exactly is executed when the program runs, preprocessing and modularization contributing to this implausibility the most. And it's the correctness of execution of the program we try to verify! We can't know what the final source looks like unless we follow the build process the driver developer intended.

As for compiling without the kernel, driver relies on kernel data structures as well as kernel functions. While the calls to the latter could just be ignored (like any unresolved function call is at the moment), inference of data structures by source code of the using program is beyond the scope of current work, and would require a lot of change into BLAST frontend. But it's not only BLAST what requires the input to be a correct C program: Aspectator, core of which are C code transformations, naturally require the program it instruments to be correct and full.

I think that static analysis tools will remain integrated with build process in the future, and we should to tighten this integration instead of trying to drop it.