Checker Framework Tutorial

This example uses the Tainting Checker to verify that user input does not contain SQL statements, thus preventing SQL injection.

Outline

Import personalblog-demo
Run the Tainting Checker — 1 error found
Correct the error
Re-run the Tainting Checker — a new error is found
Correct the new error
Re-run the Tainting Checker — no errors

0. Import personalblog-demo

To begin, load the personalblog-demo project into Eclipse. (Download it here.) The project has two warnings that can be ignored.

Expected Warnings

Unsupported @SuppressWarnings("untainted") ReadAction.java
Unsupported @SuppressWarnings("untainted") PersonalBlogService.java

This example has already been annotated to prevent the SQL injections. It does this by annotating PersonalBlogService.executeQuery(String) with @Untainted and providing a method, ReadAction.validate(String) , to validate the user input.

1. Run the Tainting Checker — 1 error found

Run the Tainting Checker on the entire src folder. The following warning will be produced.

incompatible types in argument.
                    "where post.category like '%", category,
  found   : @Tainted String
  required: @Untainted String   PersonalBlogService.java

The checker issues an error for getPostsByCategory() because the possibly-tainted string category is used in the query construction. This string could contain SQL statements that could taint the database. The programmer must ensure that category does not contain malicious SQL code.

2. Correct the Error

To correct this error, add @Untainted to the type of the category parameter.

  public List<?> getPostsByCategory(@Untainted String category) throws ServiceException {

This forces clients to pass an @Untainted value, which was the intention of the designer of the getPostsByCategory method.

3. Re-run the Tainting Checker — a new error is found

Run the Tainting Checker again.

incompatible types in argument.
                        pblog.getPostsByCategory(reqCategory));
  found   : @Tainted String
  required: @Untainted String   ReadAction.java

There is an error in ReadAction.executeSub(), which is a client of getPostsByCategory. The reqCategory is accepted from the user (from request object) without validation.

4. Correct the New Error

To correct, use the validate method as shown below.

    String reqCategory = validate(cleanNull(request.getParameter("cat")));

5. Re-run the Tainting Checker — no errors

There should be no errors.

For a complete discussion of how to use the Tainting Checker, please read the Tainting Checker chapter in the Checker Framework manual.

Previous Validating User Input

Finding a Security Error