The Tainting Checker prevents certain kinds of trust errors. A tainted, or untrusted, value is one that comes from an arbitrary, possibly malicious source, such as user input or unvalidated data. In certain parts of your application, using a tainted value can compromise the application’s integrity, causing it to crash, corrupt data, leak private data, etc.
For example, a user-supplied pointer, handle, or map key should be validated before being dereferenced. As another example, a user-supplied string should not be concatenated into a SQL query, lest the program be subject to a SQL injection attack. A location in your program where malicious data could do damage is called a sensitive sink.
A program must “sanitize” or “untaint” an untrusted value before using it at a sensitive sink. There are two general ways to untaint a value: by checking that it is innocuous/legal (e.g., it contains no characters that can be interpreted as SQL commands when pasted into a string context), or by transforming the value to be legal (e.g., quoting all the characters that can be interpreted as SQL commands). A correct program must use one of these two techniques so that tainted values never flow to a sensitive sink. The Tainting Checker ensures that your program does so.
If the Tainting Checker issues no warning for a given program, then no tainted value ever flows to a sensitive sink. However, your program is not necessarily free from all trust errors. As a simple example, you might have forgotten to annotate a sensitive sink as requiring an untainted type, or you might have forgotten to annotate untrusted data as having a tainted type.
To run the Tainting Checker, supply the -processor TaintingChecker or -processor org.checkerframework.checker.tainting.TaintingChecker command-line option to javac.
The Tainting type system uses the following annotations:
@Untaintedindicates a type that includes only untainted (trusted) values.
@Tainted
indicates a type that may include tainted (untrusted) or untainted (trusted) values. @Tainted is a supertype of @Untainted. It is the default qualifier.
@PolyTaintedindicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 32.2.
@Untainted annotations Most programs are designed with a boundary that surrounds sensitive computations, separating them from untrusted values. Outside this boundary, the program may manipulate malicious values, but no malicious values ever pass the boundary to be operated upon by sensitive computations.
In some programs, the area outside the boundary is very small: values are sanitized as soon as they are received from an external source. In other programs, the area inside the boundary is very small: values are sanitized only immediately before being used at a sensitive sink. Either approach can work, so long as every possibly-tainted value is sanitized before it reaches a sensitive sink.
Once you determine the boundary, annotating your program is easy: put @Tainted outside the boundary, @Untainted inside, and @SuppressWarnings("tainting") at the validation or sanitization routines that are used at the boundary.
The Tainting Checker’s standard default qualifier is @Tainted (see Section 33.5 for overriding this default). This is the safest default, and the one that should be used for all code outside the boundary (for example,
code that reads user input). You can set the default qualifier to @Untainted in code that may contain sensitive sinks.
The Tainting Checker does not know the intended semantics of your program, so it cannot warn you if you mis-annotate a sensitive sink as taking @Tainted data, or if you mis-annotate external data as @Untainted. So long as you correctly annotate the sensitive sinks and the places where
untrusted data is read, the Tainting Checker will ensure that all your other annotations are correct and that no undesired information flows exist.
As an example, suppose that you wish to prevent SQL injection attacks. You would start by annotating the Statement class to indicate that the
execute operations may only operate on untainted queries (Chapter 36 describes how to annotate external libraries):
public boolean execute(@Untainted String sql) throws SQLException;
public boolean executeUpdate(@Untainted String sql) throws SQLException;
@Tainted and @Untainted can be used for many purposes
The @Tainted and @Untainted annotations have only minimal built-in semantics. In fact, the Tainting Checker provides only a small amount of functionality beyond the Subtyping Checker (Chapter 30). This lack of hard-coded behavior has two consequences. The first consequence is that the annotations can serve many different purposes, such as:
• Prevent SQL injection attacks: @Tainted is external input, @Untainted has been checked for SQL syntax.
• Prevent cross-site scripting attacks: @Tainted is external input, @Untainted has been checked for JavaScript syntax.
• Prevent information leakage: @Tainted is secret data, @Untainted may be displayed to a user.
The second consequence is that the Tainting Checker is not useful unless you annotate the appropriate sources, sinks, and untainting/sanitization routines.
If you want more specialized semantics, or you want to annotate multiple types of tainting (for example, HTML and SQL) in a single program, then you can copy the definition of the Tainting Checker to create a new annotation and checker with a more specific name and semantics. You will change the copy to rename the annotations, and you will annotate libraries and/or your code to identify sources, sinks, and validation/sanitization routines. See Chapter 37 for more details.
Misuse of polymorphism can lead to unsoundness with the Tainting Checker and other similar information flow checkers. To understand the potential problem, consider the append function in java.lang.StringBuffer:
public StringBuffer append(StringBuffer this, String toAppend);
Given these declarations:
@Tainted StringBuffer tsb;
@Tainted String ts;
@Untainted StringBuffer usb;
@Untainted String us;
both of these invocations should be legal:
tsb.append(ts);
usb.append(us);
That suggests that perhaps the function should be annotated as polymorphic:
// UNSOUND annotation -- do not do this!
public @PolyTainted StringBuffer append(@PolyTainted StringBuffer this, @PolyTainted String toAppend);
The problem with the above annotation is that it permits the undesirable invocation:
usb.append(ts); // undesirable invocation
This invocation is permitted because, in the expression, all @PolyTainted annotations on formal parameters are instantiated to @Tainted, the top annotation, and each argument is a subtype of the corresponding formal parameter.
Beware this problem both in code you write, and also in annotated libraries (such as stub files). The correct way to annotate this class is to add a class qualifier parameter; see Section 32.3.
(Side note: if append were purely functional (had no side effects and returned a new StringBuffer), the method call would be acceptable, because the return type is instantiated to @Tainted StringBuffer for the expression usb.append(ts). However, the
append method works via side effects, and only returns a reference to the buffer as a convenience for writing “fluent” client code.)