JQual User's Guide ********************************************************************* ********************************************************************* JQual is a general framework for performing type qualifier inference on Java programs. It allows the user to define a set of qualifiers, annotate types in a program with those qualifiers and infer the qualified types for all of the locations in the program. For example, it can be used to track suspect "tainted" values through a program and check that they are not used in sensitive "untainted" locations. Another application of JQual is to infer immutability properties "readonly" and "final" in a Java program. JQual produces warnings for locations that cannot be typed consistently with the given annotations and lists the set of constraints, i.e. the "inference path", used to infer the inconsistency. JQual operates on source code and can analyze Java versions 1.4 and earlier. It does not provide sound analysis of native calls or calls to classes for which source code is not available, although it is possible to create annotated stub versions of such code and include it in the analysis. Calls made via reflection are also not handled soundly. A more detailed description of JQual and its applications are available at: http://www.cs.umd.edu/projects/PL/jqual For questions or assistance, email dgreenfi(at)cs.umd.edu **************************************************************************** * Running JQual * **************************************************************************** JQual analyzes Java source code. It can be run on a single .java file or a collection of files. The "Run JQual" button on the tool bar runs JQual on the file currently selected in the Java editor pane. To run on a collection of files, select those files in the Package Explorer pane and choose "Run JQual" from the context menu. The selection can include individual .java files, packages, and Eclipse projects. In the case of packages and projects, all of the contained .java files are included in the analyzed body of code. JQual performs type qualifier inference on the files according to the parameters in the JQual preferences and the qualifiers defined in a lattice file. Preferences and lattice files are described below. If JQual infers any inconsistent qualifiers it prints warnings to the console pane. JQual can also be configured to produce a complete record of the qualifiers inferred on the program. If so, this is output to a file called inferredResultsLog in the root directory of the workspace. **************************************************************************** * Example * **************************************************************************** Below is an example Java program that illustrates a very simple error case. It comes from the file Assignment.java included in the jqual-test project. /* * t and u are inferred to be both tainted and untainted */ public class Assignment { /** @qual tainted **/ int t; /** @qual untainted **/ int u; void f(){ u = t; } } The qualifiers in this example are tainted and untainted. These are defined in the lattice file included with the JQual distribution as: partial order { untainted [level = value, sign = neg] tainted [level = value, sign = pos] untainted < tainted } The qualifier untainted is declared to be a subtype of the qualifier tainted, since untainted data can be used in place of tainted data, but not vice-versa. Both qualifiers are defined to be applied to the value level of the locations they qualify. Untainted is designated as having a negative sign, which means that the values it qualifies are constrained to be less than untainted. Tainted has a positive sign, indicating that the values it qualifies are greater than tainted. These signs make sense given the subtyping relationship between the qualifiers. In the example, the field t is qualified as tainted and the field u as untainted. When a variable y is assigned to a variable x, JQual makes a constraint Ty <= Tx, where Ty is the type of y and Tx is the type of x. Thus, at the statement u = t, the constraint t <= u is created. As a result, t and u are inferred to be both tainted and untainted, which violates the partial order defined in the lattice file. JQual generates these warnings: Qualifier constraint errors were detected: Assignment.java:14 Assignment violates qualifier rules TAINTED.ASSIGNMENT.t: tainted untainted Assignment.java:7 tainted <= TAINTED.ASSIGNMENT.t Assignment.java:14 <= TAINTED.ASSIGNMENT.u Assignment.java:8 <= untainted Assignment.java:14 Assignment violates qualifier rules TAINTED.ASSIGNMENT.u: tainted untainted Assignment.java:7 tainted <= TAINTED.ASSIGNMENT.t Assignment.java:14 <= TAINTED.ASSIGNMENT.u Assignment.java:8 <= untainted The first line of each warning names the value that has contradictory qualifiers and what those qualifiers are. The rest of the warning shows the inference path, i.e. the series of constraints that were used to infer the qualifiers. Each <= represents one constraint. At the left of each line is the location at which the constraint arose. In this example, both inference paths consist of three constraints: u <= untainted // from annotation on u t <= u // from assignment statement tainted <= t // from annotation on t **************************************************************************** * Lattice File Format * **************************************************************************** The lattice file defines the qualifiers that can appear in a program being analyzed. The file consists of a collection of partial orders. Each partial order defines a set of qualifiers and the subtyping relationships between them. It can optionally specify the level and sign of each qualifier. The level can be either "ref" to indicate that the qualifier is applied at the reference level of the variables it qualifies or "value" to indicate the value level. The default is "ref". (For a discussion of reference and value qualifiers in qualified types, see JQual.pdf.) The level can be overridden with special annotations (described below) for qualifiers that can be used at both levels. The sign can be either "neg", which means that the values it qualifies are constrained to be less than it. For example, because of the untainted qualifier annotation, u is assigned a type "q u" such that q <= untainted, and since nothing is smaller than untainted, that makes q untainted. The alternative, "pos", means that the values it qualifies are greater than the qualifier. Because of the tainted qualifier annotation, t is assigned a type "q t" such that tainted <= t, and since nothing is smaller than tainted, that makes t tainted. The default sign is "pos". The example lattice file included in jqual-tests, which JQual uses by default at installation, defines two partial orders: untainted/tainted, which can be used for tainting analysis, and mutable/readonly, which can be used in the readonly analysis included with JQual. For a complete specification of the lattice file format, see the CQual User's Guide, available at: http://www.cs.umd.edu/~jfoster/cqual/user-guide-0.991.pdf **************************************************************************** * Annotating Code * **************************************************************************** Type qualifier annotations are added to Java code as Javadoc-style comments with custom tags @qual, @qthis, and @qreturn. Methods, fields, variables, and type casts can be annotated. In addition, fields can be annotated with @FieldSensitive to indicate they should be tracked in a selective field-sensitive analysis, as described below. The file ManyAnnotations.java included in jqual-tests demonstrates how to annotate the various parts of a program: public class ManyAnnotations { /** @qual tainted **/ int f1; /** @FieldSensitive **/ int f2; /** qualifiers for method: * * @qthis tainted * @qreturn untainted */ String f(/** @qual untainted **/ int p1, /** @qual tainted **/ int p2){ /** @qual tainted **/ String v1 = null; return (/** @qual untainted **/ String) v1; } } In addition, the tags @refqual and @valqual have the same effect as @qual, except that they override the level defined for the qualifier in the lattice file. This is useful for qualifiers that can be meaningfully applied at both the reference and value level. An alternative to including qualifier annotations in the method signature is to use the @qparam tag in the javadoc comment of the method, in the same manner as @qthis and @qreturn. The @qparam tag takes the name of the parameter as an argument: @qparam p1 untainted **************************************************************************** * Preferences * **************************************************************************** The JQual preferences dialog is accessed from the general Eclipse preferences dialog. Lattice File Location --------------------- To use a different lattice file, the lattice file path can be set in the preferences dialog. Context Sensitivity ------------------- Context sensitivity controls whether JQual calculates different qualified types for methods depending on their calling context. Alternately, it can be thought of as allowing methods to be polymorphic (or "generic") in their inputs and outputs. Enabling context sensitivity will typically make JQual more precise but will generally make the analysis take longer and use more memory. The example class CSExample shows a situation in which context sensitivity alters the precision of the analysis results. Field Sensitivity ----------------- Field sensitivity controls whether JQual tracks the fields of objects individually or whether all instances of a class share a single type for each of their fields. Field-sensitive analysis, which tracks fields separately, is generally more precise but takes longer and uses more memory. JQual field-sensitive analysis on a typical machine can only run to completion on small programs. Another option is selective field-sensitivity which separately tracks only those fields which are annotated with @FieldSensitive. This provides the precision of field sensitivity where the user believes it will be beneficial without incurring the costs of full field sensitivity. To use selective field sensitivity, enable the option "Obey f/s annotations on individual fields". An example of a situation for which field sensitivity alters the results is shown in FSExample. Note that an analysis must be context sensitive for field sensitivity to have an effect. Otherwise all object fields are merged at the constructor return. Transitive Closure and Libraries -------------------------------- If the classes selected for analysis make use of classes that have not been selected, the extra code can be included in the analysis if the transitive closure options are enabled. This extra code can come from the standard libraries or from other classes in the Eclipse projects being analyzed. If the "Calculate transitive closure" option is enabled, JQual will pull in any classes from that are used by the core set that are in the eclipse projects containing the core set, as well as the transitive closure of classes used by that code. To include code for calls to the standard library classes, the user must create an Eclipse project called "javalib" containing the source code for the libraries and enable the "Analyze Java libraries" option (as well as the "Calculate transitive closure" option.) JQual uses a conservative policy for calculating the transitive closure. Any class that is used at all will be included in its entirety. Methods that are not actually called may be included in the analysis set, as well as extra classes called by those methods. As a result, the analysis set can grow quite large when the full libraries are included, increasing analysis times and memory use significantly - especially when a field-sensitive analysis is used. An alternative is to include only key packages in the javalib project, for example java.lang and java.util. Output Options -------------- Any warnings that occur are displayed in the Eclipse console pane. In addition The "Log inferred types" option makes JQual produce a text file called "inferredResultsLog" listing the qualified types for the analyzed program. The option "log constraints" makes JQual produce a text file called "constraintLog" listing all of the constraints generated during the analysis. This can be useful for debugging or for understanding how JQual performs inference. Both of these files are created in the root directory of the workspace. Readonly Analysis ----------------- JQual includes an analysis to infer readonly and final for reference variables in Java programs. This analysis uses the qualifiers readonly and mutable. By default this analysis is not performed when JQual is run, but it can be activated by enabling the option "Perform readonly analysis". The distribution includes stubbed library files used to increase the precision of the readonly analysis. These are in the file readonlyLibraryStubs.jar. Before running the readonly analysis, import this file into the workspace as a project called readonlyLibraryStubs. **************************************************************************** * Modifying Qualifier Semantics * **************************************************************************** JQual uses data flow semantics for propagating qualifiers through a program. That is, constraints between variables are mainly generated at assignment statements and method invocations. For some analyses, it may be necessary to have different constraints arise from other expressions. For example, in the readonly analysis a variable that is assigned to must be constrained to be mutable. Changing the semantics of JQual qualifier inference requires modifying the code of JQual itself. A full discussion of how to do this is beyond the scope of this guide, but the modifications required are typically made to the class ConstraintVisitor. This class contains visitor methods for the nodes of abstract syntax trees. Modifying these methods will change the semantics of qualifier inference. Source code for the JQual plugin is included in the jqual_1.0.0.jar file. To edit the plugin, import the jar file as a Plug-in Development Project in Eclipse.