Defective Taint Analysis

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Consider UserRepository classe from the attached file.
2. Run the Taint Analysis via the Checker Framework Eclipse Plugin

What is the expected output? What do you see instead?
The u1 variable is defined in line 19 as @Tainted and the parameter in line 35 
is defined as @Untainted. Checker framework should show the type problem when 
passing u1 in line 21. However, no error nor warning is shown.

What version of the product are you using? On what operating system?
Eclipse: Juno Service Release 2, Build id: 20130225-0426
Mac OS X: Mavericks
Checker framework plugin: 1.7.4

Please provide any additional information below.

Original issue reported on code.google.com by rodrigo...@gmail.com on 8 Apr 2014 at 5:58

Attachments:

• toy-example.zip

[GoogleCodeExporter]

Thanks for your report.
I think the issue is insufficient documentation of how annotations on 
constructor results are interpreted.

Class User has constructors like this one:

@Tainted public User() ...

However, this only gives an upper bound for possible instantiations of class 
User. It is not interpreted as making all instantiations @Tainted.

In UserRepository this line:

@Tainted User u1 = new User(...);

uses normal defaulting rules and is then interpreted as:

@Tainted User u1 = new @Untainted User(...);

As the annotation on the instantiation is a subtype of the annotation on the 
constructor result, the instantiation is valid.

Next, the declared type of u1 is refined by the type of the right-hand side, 
resulting in u1 being @Untainted.
Therefore, the call on the next line is valid.

To create a @Tainted object, you have to provide that annotation explicitly 
with the instantiation.
Similarly, if you use a @Tainted parameter, you will get the expected errors.

We have discussed alternative interpretations for constructor results and maybe 
we should restart that discussion.

Original comment by wdi...@gmail.com on 10 Apr 2014 at 1:47

• Changed state: Invalid

[GoogleCodeExporter]

Thanks for your quick reply.

How do I provide the @Tainted annotation explicitly with the instantiation so 
that the declared type is not refined by the type of the right-hand side? 

Original comment by rodrigo...@gmail.com on 10 Apr 2014 at 7:02

[GoogleCodeExporter]

I don't think your bug has anything to do with the constructor annotation.  I 
tried the tainting checker on your example and got the following error:

domain/User.java:32: error: annotation type not applicable to this kind of 
declaration
    @Tainted public void setLogin(@Tainted String login) {
    ^

@Tainted is a type annotation, so it cannot be applied to a method declaration. 
 In the above example, the first @Tainted should be removed.  The second 
@Tainted is in a valid location and can remain. 

In general, annotations should appear immediately before the type they qualify, 
so loggingUsers should be annotated as follows:

    private @Untainted String loggingUsers(@Untainted User user) {

For constructors, this is the name of the method:

    public @Tainted  User() {

Also, because @Tainted is the default annotation, you there is no need to write 
it any where in your code.   (Tainted has the @DefaultQualifierInHierarchy 
meta-annotation so it is the default, not @Untainted.)

These errors are preventing the annotation on the parameter of loggingUsers 
from being read/used, so the default, @Tainted, is applied and no warning is 
used.

I corrected  these annotatoins and the TaintingChecker output this warning 
(among others):
/toy-example-password/src/util/UserRepository.java:23: warning: 
(argument.type.incompatible) 
        loggingUsers(u1);
                     ^
  found   : @Tainted User
  required: @Untainted User

I used the latest version of the Checker Framework plug-in, so if you make 
these changes and still do not see the warning, you may need to update the 
plug-in.  If you do so, you'll need the new checkers-quals.jar, which has been 
renamed to checker-qual.jar.  And you will need to update the import statements 
to:
import org.checkerframework.checker.tainting.qual.Tainted;
import org.checkerframework.checker.tainting.qual.Untainted;

Please let us know if you have further problems.

Original comment by Suzanne....@gmail.com on 10 Apr 2014 at 9:08

[GoogleCodeExporter]

I got it right now. Thanks!

Original comment by rodrigo...@gmail.com on 11 Apr 2014 at 8:12