sixgillsixgill is a tool for statically checking assertions in C/C++ code. It is nearly a verifier — that is, it is able to prove an assertion always holds, modulo some assumptions it makes about the code. First and foremost, it intends to be practical. The main features of sixgill are:
1. Clear Reports
sixgill's checking is comprehensive, and the great majority of its reports will be false positives. sixgill's reports are designed to be quick and easy to diagnose and fix.
False positives can be fixed using annotations, clarifying what the code does in a checkable fashion. Annotations can also be used as checkable documentation, and are simple yet extremely expressive. They are not needed all that often, though; sixgill includes a powerful and robust inference. When checking for buffer overflows (the safety of a buffer access is, conceptually, an assertion), sixgill can check 80-90% of accesses automatically. Fixing the remaining reports has, in our experience, required less than one annotation per 1000 lines of code.
sixgill's analyses are precise. The possible behaviors of a block of code can be understood with near exact precision, along with nearly anything that can be written with an assert. There are limits to this precision, which can be partially addressed using annotations. How much these limitations matter depends on the assertions being checked; for buffer overflows, 2-4% of accesses may be affected.
sixgill uses a sound model of the code (completely modelling its possible behaviors), with some exceptions. These exceptions can cause it to miss bugs, claiming an assertion always holds when in fact it might not. While we think the number of missed bugs is small, we don't know; we can, however, describe the conditions when sixgill will miss a bug, and all its unsoundnesses are fixable.
sixgill's analyses are designed to scale to arbitrarily large programs. The largest program we have used sixgill on is the Linux kernel, including all drivers. (There are likely to be engineering issues with analyzing larger programs, though these can be fixed).
Releasessixgill is freely available under the GPL, version 3.
Current release: xgill-0.9.1.tar.gz
Anonymous SVN access: svn checkout http://svn.sixgill.org/trunk xgill
Mailing ListsRelease announcements: firstname.lastname@example.org
General discussion and bug reports: email@example.com
bhackett at stanford.edu