I notice that recently Linus, Al Viro, and others have put a huge
effort into annotating the kernel to find user/kernel pointer bugs
with sparse. Despite this work, fewer than 1000 of the almost 13000
source files in Linux 2.6.7-rc3 contain any annotations at all.
Because of this, I think you might be interested in our tool for
finding user/kernel pointer bugs, CQual. CQual could save
months of work annotating the rest of the kernel.
Like sparse, cqual uses annotations to find bugs in software. I
don't intend for cqual to replace sparse, but for the specific problem
of user/kernel pointer bugs, I believe that cqual provides better
results with less work from programmers. The main features of cqual
are:
- cqual requires _very few_ annotations.
CQual infers most annotations from a few base annotations provided
by programmers. In theory, it's possible to check the entire kernel
with fewer than 300 annotations. In practice, cqual only requires
header files to be annotated.
- cqual requires _zero_ annotations in device drivers.
Once the generic driver interfaces have been annotated, all device
drivers can be checked against these annotations without any further
effort. This is critical, since annotating the thousands of device
drivers in linux will be extremely difficult and take months.
- cqual can verify more code than sparse.
CQual allows some struct instances to have user pointer fields and
some to have kernel pointer fields, and it automatically figures out
which are which. This means some code that sparse erroneously
reports as buggy will pass through cqual without warning. The only
way to get this sort of code to check with sparse is to have two
redundant structure definitions: one holding user pointers and the
other holding kernel pointers. This sort of code duplication will
lead to its own host of code maintainence problems. Thus, the
ability to check more code not only reduces the false positive rate,
it results in more maintainable code.
CQual supports other features, such as polymorphism, that also allow
it to verify more code.
- cqual doesn't require numerous casts.
Casts are extra annotations that pose yet another annotation burden
on the programmer. Even worse, they can silently suppress
legitimate warning messages. CQual requires far fewer casts than
sparse, so it's easier to use and less error prone.
- cqual doesn't miss any bugs.
If cqual says code is free of user/kernel pointer bugs, then it is.
- cqual works with the kernel build system
CQual ships with a script, "kqual", that makes it behave like a
drop-in replacement for sparse in the kernel build system.
- cqual is open source (GPL).
It's hosted on sourceforge and available from
http://www.cs.umd.edu/~jfoster/cqual/
I've already used cqual to find numerous real user/kernel pointer
bugs in the Linux kernel. You can read about these results in the
paper: http://www.cs.berkeley.edu/~rtjohnso/papers/cquk.ps
I look forward to receiving feedback from kernel developers on cqual.
In the long run, I hope to see cqual become the default tool for
finding user/kernel pointer bugs in Linux. Again, cqual cannot
replace sparse, because sparse performs many checks that cqual does
not, but for user/kernel pointer bugs, cqual gives better results with
far, far fewer annotations. Thanks for your feedback.
Best,
Rob Johnson
P.S. As an example, cqual has already found bugs in
drivers/char/drm/gamma_dma.c
drivers/scsi/cpqfcTSinit.c
drivers/usb/vicam.c
drivers/usb/w9968cf.c
drivers/pcmcia/{[dc]s,bulkmem}.c
drivers/i2c/i2c-dev.c
fs/ncpfs/ioctl.c
drivers/net/wan/cosa.c
drivers/net/wan/sbni.c
drivers/net/bonding.c
drivers/video/fbcon.c
drivers/i2c/i2c-dev.c
drivers/message/i2o/i2o_config.c
drivers/char/joystick.c
and probably a few others that I've forgotten.
On Mon, Jun 07, 2004 at 04:48:44PM -0700, Robert T. Johnson wrote:
> - cqual requires _zero_ annotations in device drivers.
>
> Once the generic driver interfaces have been annotated, all device
> drivers can be checked against these annotations without any further
> effort. This is critical, since annotating the thousands of device
> drivers in linux will be extremely difficult and take months.
Aha, so you have never actually bothered to read the damn things. Two words:
ioctl code.
Another thing: two weeks had been enough to practically eliminate noise in
net/*, sound/*, large parts of drivers/*. The only real difficulty I've
noticed was one with holding the breakfast down while reading some of more...
colourful code.
And one more: counting drivers that do not have a single __user in them
is meaningless for so many reasons it's not even funny.
Now would it be too much to ask the esteemed sir to piss off and not return
until sir acquires a modicum of clue?
On Mon, 2004-06-07 at 17:03, [email protected]
wrote:
> On Mon, Jun 07, 2004 at 04:48:44PM -0700, Robert T. Johnson wrote:
> > - cqual requires _zero_ annotations in device drivers.
> >
> > Once the generic driver interfaces have been annotated, all device
> > drivers can be checked against these annotations without any further
> > effort. This is critical, since annotating the thousands of device
> > drivers in linux will be extremely difficult and take months.
>
> Aha, so you have never actually bothered to read the damn things. Two words:
> ioctl code.
CQual has already found numerous bugs in driver ioctl code, all without
any explicit annotations in that code. This is possible because cqual
infers the required annotations from a few annotations I gave it.
While examining these bugs, I had to read _a lot_ of driver code, and I
agree that some of it is very colorful.
> And one more: counting drivers that do not have a single __user in them
> is meaningless for so many reasons it's not even funny.
Maybe sparse has features that I don't know about, but since lots of
device drivers have ioctl functions, doesn't that mean that lots of
device drivers need at least one __user annotation (on the ioctl "arg"
argument)? If that annotation is missing and the device driver
dereferences arg (after casting it to a pointer), won't this result in a
false negative? I agree that it's not a perfect metric, but it's a
start.
Best,
Rob
On Mon, Jun 07, 2004 at 06:03:29PM -0700, Robert T. Johnson wrote:
> CQual has already found numerous bugs in driver ioctl code, all without
> any explicit annotations in that code. This is possible because cqual
> infers the required annotations from a few annotations I gave it.
Pardon me, but I will believe it when I see your bug reports. All
I had been able to find on MARC was rather unimpressive; if that is
what you've found using cqual in several months...
> Maybe sparse has features that I don't know about, but since lots of
> device drivers have ioctl functions, doesn't that mean that lots of
> device drivers need at least one __user annotation (on the ioctl "arg"
> argument)? If that annotation is missing and the device driver
> dereferences arg (after casting it to a pointer), won't this result in a
> false negative? I agree that it's not a perfect metric, but it's a
> start.
First of all, it's nowhere near the majority of _files_. Moreover,
the taint analysis is nowhere near "if it gives no warnings, we are
guaranteed to have no user/kernel pointer mixed".
The only way to convince anybody that it's worth the trouble is to
make your annotations available, run your stuff over the patched
tree and start posting fixes. If it catches a lot of bugs - who
would argue against its usefulness? If not - too bad, but then again
there would be no questions.
Neither sparse nor cqual will catch everything that could be, in theory,
automatically caught. Same story as with optimizations - there's always
one more.
The real questions are
a) how large subset of tree can $FOO survive?
b) how many new bugs is $FOO catching?
c) how much noise does $FOO produce and how hard it is to eliminate
that noise?
d) how fast $FOO is (it _is_ important, if you hope to get a decent
code coverage, especially on non-x86 platforms).
e) is everything needed for testing available ($FOO itself, patches
needed to use it on the tree usefully)?
And that's all that matters. So far you said nothing on (a) or (d), had
rather unimpressive results posted on (b) and basically waved hands on (c).
Not sure about (e); are your initial annotations available for download?