[klee-dev] Using KLEE on Linux kernel drivers?

[Alastair Reid]

Dear KLEE-dev,

I am trying to figure out how to use KLEE on the Rust device drivers
recently proposed for addition to Linux. (LKML discussion)
<https://lkml.org/lkml/2021/4/14/1023>
I am certain that somebody must have used KLEE on Linux kernel drivers in
the past and wonder if you could point me at that work?

I am particularly interested in how to write a test harness that directly
invokes functions in the drivers because the most obvious approach of using
a usermode test program to invoke KLEE on the entire kernel is...
unappealing.

--
Alastair Reid

ps The bits that I know how to do are: build the entire kernel using wllvm;
generate bitcode for the Rust parts; write stubs to redirect Linux's
kalloc/kfree to KLEE's malloc/free (etc.); compile
klee/runtime/Freestanding with the same flags the kernel is built with, and
link a device driver together. I can then run 'klee
--entry-point=init_module  mydriver.bc'.
-------------- next part --------------
HTML attachment scrubbed and removed