Static Analysis tool for Linux kernel modules and device drivers

7
votes

I need a static analysis tool for the Linux Device Drivers I write for ARM based boards. I am considering few tools as mentioned below:

  1. Sparse is a computer software tool, already available on Linux, designed to find possible coding faults in the Linux kernel.

  2. There are two active projects of Linux Verification Center aimed to improve quality of the loadable kernel modules.

    • Linux Driver Verification (LDV) - a comprehensive toolset for static source code verification of Linux device drivers.
    • KEDR Framework - an extensible framework for dynamic analysis and verification of kernel modules.
    • Another ongoing project is Linux File System Verification that aims to develop a dedicated toolset for verification of Linux file system implementations.
  3. Enable -Werror, -Wextra and -Wall on GCC, and run with Valgrind.

Last time I played with Sparse I found the outputs to be confusing and did not find a good documentation to interpret the output. Does anyone has a good documentation on Sparse tool? What are the other Free static analysis tools I can use for my Linux driver verification? I know about LINT tool but its licensed.

2
cmemory-leakslinux-kernellinux-device-driverstatic-analysis
Try splint. It is free. Another suggestion would be to compile with -Wall and -Wextra. - Kenneth
splint is for normal C code. I need a tool which can check for linux kernel code. A common example is using a function that might sleep (or, generally, might cause rescheduling) in atomic context, that is, in interrupt handlers, in critical sections guarded by spinlocks and the like. - manav m-n
It sounds like you are mixing a lot of different concepts here. The Linux kernel is written in C, so splint is a valid static analysis tool. - Kenneth
Yes, LDV is a very powerful static analysis system, many bugs in the kernel have been found by it so far. They also have a web interface to the verifier (linuxtesting.org/ldv/online) which you can use to upload and check your driver. Not sure how do they handle ARM specifics now, but anyway - worth trying. - Eugene
As for the tools build in two other projects of Linux Verification Center, both are dynamic analysis systems rather than static analysis tools you need. KEDR Framework is currently intended for x86 only. As one of the main developers of KEDR, I've had no time so far to port it to ARM, unfortunately. Next year, I hope to be able to do this. Spruce system developed in Linux File System Verification project relies on KEDR too, to some extent. - Eugene

2 Answers

4
votes

Smatch is a static analysis tool for C that is used on the kernel. It has resulted in hundreds of patches. Quite a few have been security related or were significant enough for the stable kernel.

3
votes

If you want to write your own rules, Coccinelle is probably appropriate. If you want to use rules written by others you can use the various tools integrated into the kernel. Check section 4.2: CODE CHECKING TOOLS of Documentation/development-process/4.Coding for some suggestions.