Smatch - a Stanford Checker for the rest of us

The "Stanford Checker" (also known as "MC") is a project headed up by Stanford professor Dawson Engler; MC uses a modified version of the gcc compiler to find potential errors in C code. Occasionally, the Stanford Checker group surfaces on linux-kernel with a list of new problems found by MC; the last such posting listed a set of potential buffer overrun vulnerabilities on January 2.

The Checker postings are appreciated by the kernel developers, since they have pointed out a large number of real bugs. It would be even nicer if the Checker were available for others to use, but that is not the case. The MC group still has not released its work, which, it claims, remains incomplete. So there is little to do except to wait for the next posting.

Dan Carpenter, however, got tired of waiting and set out to create his own MC-like system. The result is Smatch, which was announced on the kernel janitors' list on January 1. Smatch attempts to duplicate the techniques used in the Stanford Checker, as derived from papers published by the MC group. It is still very much a work in progress; rather than producing nice reports, Smatch creates large amounts of raw data which must then be filtered with Perl scripts. An initial set of scripts exists, but quite a bit of work remains to be done in that area.

So Smatch probably will not be putting the Stanford Checker out of business anytime soon. But it will provide a platform for the development of freely-available checking tool with similar capabilities. With luck, and some development time, Smatch should help in the creation of more stable kernels in the near future.

---

to post comments