Checker Framework Tutorial

1. Import personalblog-demo

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

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.

2. 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 a warning for getPostsByCategory() because a possibly tainted string category is used in the query construction. This String could contain SQL statements that could taint the database. The programmer must require category to be untainted.

3. Correct the Error

To correct this, add @Untainted to category parameter declaration. This forces clients to pass an @Untainted value, which was the intention of the designer of the getPostsByCategory method. See the change below.

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

4. Run the Tainting Checker--a new error is found

Run the Tainting Checker again. 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. Below is the warning message.

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

5. Correct the New Error

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

6. Run the Tainting Checker--no errors

There should be no errors.