sixgill

sixgill 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.

2. Annotations
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.

3. Precision
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.

4. Soundness
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.

5. Scalability
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).

Releases

sixgill 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 Lists

Release announcements: sg-releases@sixgill.org

General discussion and bug reports: sg-discuss@sixgill.org

Contact

Brian Hackett
bhackett at stanford.edu