Stanford Checker verifying FreeBSD

Submitted by thalunil
on February 5, 2004 - 3:08am

The Stanford 'Checker' is an automated tool to check source code for high level errors such as memory leaks, buffer overflows and security problems far beyond the analysis done by general compilers.

The checker has gained fame and proved very successful checking the Linux Kernel source code. The Stanford team is now working on the FreeBSD kernel source code. They have recently announced a number of possible bugs found. This is great news for FreeBSD.


List:       freebsd-hackers
Subject:    [CHECKER] bugs in FreeBSD
From:       Paul Twohey 
Date:       2004-01-17 0:01:31

Hi,

I'm with the Stanford Metacompilation research group. We have a suite of
checkers that find bugs at compile time and we've had quite a bit of
success checking the Linux kernel code for errors. Since our checkers can
emit false alarms we filter the reports before we give them to the kernel
developers. While some false alarms slip past us to the developers, our
limited knowledge of the kernel allows us to recognize most of them.

We are currently trying to extend our checker to automatically find 
functions which allocate resources and to make sure those resources are 
properly disposed of. 

Enclosed is a list of potential bugs in FreeBSD where a value is returned 
from a function (like malloc) that should be owned by the caller and the 
caller does not properly dispose of the value with the appropriate 
disposal routine (like free).

Confirmation of these reports would be appreciated.

Thanks

Paul Twohey