CQual
 A tool for adding type qualifiers to C

[ Introduction | Download | Applications | Screenshots | Related Projects | Publications ]

New! We have switched the project over to subversion rather than cvs, so you should use that if you wish to check out the latest version.

Oink is a new C/C++ toolkit that includes Cqual++, a C/C++ frontend for Cqual. Oink was developed by Dan Wilkerson.

Version 0.991, a bugfix version, is available. (If you want to use flow-sensitive qualifiers, you should use version 0.981 instead.)

For questions or comments about Cqual, send e-mail to cqual at cs.umd.edu.

Introduction

Cqual is a type-based analysis tool that provides a lightweight, practical mechanism for specifying and checking properties of C programs. Cqual extends the type system of C with extra user-defined type qualifiers. The programmer adds type qualifier annotations to their program in a few key places, and Cqual performs qualifier inference to check whether the annotations are correct. The analysis results are presented with a user interface that lets the programmer browse the inferred qualifiers and their flow paths.

The source code for Cqual is available under the GPL license. Here is the user's guide, which is also included in the distribution.

Cqual has a number of features:

The technical idea behind Cqual is constraint-based type inference. To analyze a program, Cqual traverses the program's abstract syntax tree and generates a series of constraints that capture the relations between type qualifiers. A solution to the constraints gives a valid assignment of type qualifiers to the variables in the program. If the constraints have no solution, then there is a type qualifier inconsistency, indicating a potential bug.

Download

Cqual is available for download under the GNU General Public License. The code has been tested under various versions of RedHat Linux, and should be compatible with most standard unix environments. There are several flavors of the tool, depending on what language you are interested in:

Cqual is the version used for the example applications mentioned below, and it handles C code (ANSI and GNU C). Cqual is currently hosted on sourceforge. Go to http://sourceforge.net/projects/cqual/ for the current releases and for SVN access to the latest version. (The CVS version is deprecated.) You can go directly to the list of releases here

If you would like to apply type qualifiers to C++ code, you can download Oink, a new C/C++ toolkit that includes Cqual++, a C/C++ frontend for Cqual. Oink was developed by Dan Wilkerson.

If you would like to apply type qualifiers to Java code, a Jqual tool is in active development. You can access the current version (which most likely will not do anything) in the cqual CVS repository on sourceforge.

Contributors

Jeff Foster Rob Johnson John Kodumal
Tachio Terauchi Umesh Shankar Kunal Talwar
David Wagner Alex Aiken Martin Elsman
Chris Harrelson and others...

For questions or comments about Cqual, send e-mail to cqual at cs.umd.edu.

Example Applications

Here are a few of the many possible applications of Cqual.

Screenshots

The current release of Cqual includes an emacs-based user interface. Below are two sample screenshots. Click on each screenshot for the full image.

[Screenshot 1]
Finding a format string bug
[Screenshot 2]
Viewing a taint flow path
[Screenshot 3]
Tracing a user/kernel error

Related Projects

Publications

[JW04] Finding User/Kernel Pointer Bugs With Type Inference [ ps | slides ]
Rob Johnson and David Wagner In 13th USENIX Security Symposium, August 2004.

[AFKT03] Checking and Inferring Local Non-Aliasing [ pdf | ps | ps.gz ]
Alex Aiken, Jeffrey S. Foster, John Kodumal, and Tachio Terauchi. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'03). San Diego, California. June 2003.

[Fos02] Type Qualifiers: Lightweight Specifications to Improve Software Quality [ pdf | ps | ps.gz ]
Jeffrey S. Foster. Ph.D. thesis, University of California, Berkeley, December 2002.

[FTA02] Flow-Sensitive Type Qualifiers [ pdf | ps | ps.gz ]
Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'02), pages 1-12. Berlin, Germany. June 2002.

[STFW01] Detecting Format-String Vulnerabilities with Type Qualifiers [ pdf | ps | ps.gz ]
Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. In 10th USENIX Security Symposium, August 2001.

[FFA99] A Theory of Type Qualifiers [ pdf | ps | ps.gz ]
Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'99). Atlanta, Georgia. May 1999.

Related Publications

[BHS03] Scrash: A System for Generating Secure Crash Information [ pdf | html ]
Pete Broadwell, Matt Harren, and Naveen Sastry. In Proceedings of the 12th Usenix Security Symposium. Washington, DC. August 2003.

[ZEJ02] Using CQUAL for Static Analysis of Authorization Hook Placement [ pdf | html ]
Xiaolan Zhang, Antony Edwards, and Trent Jaeger. In Proceedings of the 11th Usenix Security Symposium. San Francisco, California. August 2002.

Last update: November 30, 2004
This page is maintained by Jeff Foster
For questions or comments about Cqual, send e-mail to cqual at cs.umd.edu.

Valid HTML 4.01! Valid CSS!