The Checker Framework has been used to build other checkers that are not distributed together with the framework. This chapter gives an incomplete list of them. (If you know of others, or if you want this chapter to reference your checker, please send us a link and a short description.) Many of the publications in Section 41.7 provide implementations, which are not necessarily listed here yet.
These tools are externally-maintained, so if you have problems or questions, you should contact their maintainers rather than the Checker Framework maintainers.
This list is in reverse chronological order; newer tools appear first and older ones appear last.
The Determinism Checker ensures that a program is deterministic across executions. A deterministic program is easier to test and to debug (for example, by comparing executions).
The Determinism Checker focuses on sequential programs. It detects nondeterminism due to the iteration order of a hash table (or on any other property of hash codes), default formatting (such as Java’s Object.toString(), which includes a memory address), random, date-and-time
functions, and accessing system properties such as the file system or environment variables.
The paper “Verifying determinism in sequential programs” [MWME21] describes the Determinism Checker.
Interval analysis estimates the run-time values of numerical expressions in the source code by computing a lower bound and an upper bound. The Constant Value Inference project is a whole-program inference approach for integral range analysis (interval analysis).
The thesis “Interval Type Inference: Improvements and Evaluations” [Wan21] describes Constant Value Inference.
The Crypto Checker can help you find whether your program uses any weak or unsupported crypto algorithms or unsupported algorithm providers. If the Crypto Checker issues no warnings for a given program, then you have a guarantee that your program at run time will never have these issues. This is similar to the earlier AWS Crypto Policy Compliance Checker (Section 31.4).
The paper “Ensuring correct cryptographic algorithm and provider usage at compile time” [XCD21] (FTfJP 2021) and the thesis “Light-weight verification of cryptographic API usage” [Xin20] describe the Crypto Checker.
The AWS crypto policy compliance checker checks that no weak cipher algorithms are used with the Java crypto API.
The paper “Continuous Compliance” [KSTE20] (ASE 2020) describes several custom Checker Framework checkers in the context of a compliance regime at Amazon Web Services.
The AWS KMS compliance checker extends the Constant Value Checker (see Chapter 24) to enforce that calls to Amazon Web Services’ Key Management Service only request 256-bit (or longer) data keys. This checker can be used to help enforce a compliance requirement (such as from SOC or PCI-DSS) that customer data is always encrypted with 256-bit keys.
The KMS compliance checker is available in Maven Central. To use it in build.gradle, add the following dependency:
compile("software.amazon.checkerframework:aws-kms-compliance-checker:1.0.2")
Other build systems are similar.
The paper “Continuous Compliance” [KSTE20] (ASE 2020) describes several custom Checker Framework checkers in the context of a compliance regime at Amazon Web Services.
The PUnits system can check the correctness of a program or annotate a program with units of measurement. It is described in the paper “Precise inference of expressive units of measurement types” (OOPSLA 2020) [XLD20].
JaTyC, Java Typestate Checker, ensures that methods are called in the correct order. The sequences of method calls allowed are specified in a protocol file which is associated with a Java class by adding a
@Typestate annotation to the class. It is described in “Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language” [BFG+20], and the implementation is an
extension of Mungo (https://www.dcs.gla.ac.uk/research/mungo/index.html).
NullAway is a fast type-checker for only nullness properties. It is built on top of Error Prone and the Checker Framework’s Dataflow Framework. See Section 40.10.3 for a comparison between NullAway and the Nullness Checker. NullAway is described in the paper “NullAway: Practical type-based null safety for Java” [BCS19].
The Nullness Rawness Checker is a variant of the Nullness Checker that uses a different type system for initialization. It was distributed with the Checker Framework through release 2.9.0 (dated 3 July 2019). If you wish to use it, install Checker Framework version 2.9.0.
The paper “Inference of field initialization” [SE11] describes inference for the Rawness Initialization Checker.
The Rx Thread & Effect Checker enforces UI Thread safety properties for stream-based Android applications. The paper “Safe Stream-Based Programming with Refinement Types” [SCSC18] describes the Rx Thread & Effect Checker.
Practical Immutability For Classes And Objects (PICO) is a type system that supports class-level and object-level immutability, based on the Checker Framework. The implementation is available at https://github.com/opprop/immutability, and a docker image is available at https://hub.docker.com/repository/docker/lnsun/pico.
The theses “Context Sensitive Typechecking And Inference: Ownership And Immutability” [Ta18] and “An Immutability Type System for Classes and Objects: Improvements, Experiments, and Comparisons” [Sun21] describe PICO.
The InputStream.read() and Reader.read() methods read a byte (or character) from a stream. The methods return an int, using -1 to indicate the end of the stream. It is an error to cast the value to a byte (or character) without first checking the value against -1. This is
rule CERT-FIO08-J. The Read
Checker and/or Cast Checker enforces it.
The paper “Don’t miss the end: Preventing unsafe end-of-file comparisons” [CD18] and the thesis “Pluggable Properties for Program Understanding: Ontic Type Checking and Inference” [Che18] describe the Read Checker.
The Ontology type system groups related types into coarser concepts. For example, the SEQUENCE concept includes Java’s Array, List, and their subtypes. Other examples are VELOCITY and
FORCE.
The thesis “Pluggable Properties for Program Understanding: Ontic Type Checking and Inference” [Che18] describes the Ontic type system.
Glacier enforces transitive class immutability in Java. According to its webpage:
• Transitive: if a class is immutable, then every field must be immutable. This means that all reachable state from an immutable object’s fields is immutable.
• Class: the immutability of an object depends only on its class’s immutability declaration.
• Immutability: state in an object is not changeable through any reference to the object.
Glacier is described by the paper “Glacier: Transitive class immutability for Java” (ICSE 2017) [CNA+17] and the PhD thesis “User-Centered Design of Principled Programming Languages” [Cob20].
jOOQ is a database API that lets you build typesafe SQL queries. jOOQ version 3.9.0 and later ships with a SQL checker that provides even more safety: it ensures that you don’t use SQL features that are not supported by your database implementation. You can learn about the SQL checker at https://blog.jooq.org/jsr-308-and-the-checker-framework-add-even-more-typesafety-to-jooq-3-9/.
Javari [TE05], IGJ [ZPA+07], and OIGJ [ZPL+10] are type systems that enforce immutability constraints. Type-checkers for all three type systems were distributed with the Checker Framework through release 1.9.13 (dated 1 April 2016). If you wish to use them, install Checker Framework version 1.9.13.
They were removed from the main distribution on 2016-06-01 because the implementations were not being maintained as the Checker Framework evolved. The type systems are valuable, and some people found the type-checkers useful. However, we wanted to focus on distributing checkers that are currently being maintained.
IGJ and OIGJ are described in the papers “Object and reference immutability using Java generics” [ZPA+07] (ESEC/FSE 2007) and “Ownership and immutability in generic Java” [ZPL+10] (OOPSLA 2010). The Javari type system is described in “Javari: Adding reference immutability to Java” [TE05] (OOPSLA 2005); for inference, see “Inference of reference immutability” [QTE08] (ECOOP 2008) and “Parameter reference immutability: Formal definition, inference tool, and comparison” [AQKE09] (J.ASE 2009). The paper “Practical pluggable types for Java” [PAC+08] (ISSTA 2008) describes case studies in which the Javari and IGJ Checkers found previously-unknown errors in real software.
JCrypt is a static program analysis which transforms a Java program into an equivalent one, so that it performs computation over encrypted data and preserves data confidentiality. It is described in the paper “JCrypt: Towards computation over encrypted data” [DMD16a].
DroidInfer determines the Android library sources (e.g., location access, phone state) and sinks (e.g., Internet access) used by a program, and determines whether there is impermissible information flow between them. It is described in the paper “Scalable and Precise Taint Analysis for Android” (ISSTA 2015) [HDMD15].
Error Prone is a linter or bug detector for Java. It reports violations of style rules. It is built on top of the Checker Framework’s Dataflow Framework. See Section 40.10.1 for a comparison between Error Prone and the Nullness Checker.
SPARTA is a security toolset aimed at preventing malware from appearing in an app store. SPARTA provides an information-flow type-checker that is customized to Android but can also be applied to other domains. The paper “Collaborative verification of information flow for a high-assurance app store” [EJM+14] (CCS 2014) describes the SPARTA toolset and information flow type-checker.
SFlow is a context-sensitive type system for secure information flow. It contains two variants, SFlow/Integrity and SFlow/Confidentiality. SFlowInfer is its worst-case-cubic inference analysis.
The paper “Type-based taint analysis for Java web applications” (FASE 2014) and the thesis “An Inference And Checking Framework For Context-Sensitive Pluggable Types” (2014) describe SFlow and SFlowInfer.
CheckLT uses taint tracking to detect illegal information flows, such as unsanitized data that could result in a SQL injection attack.
EnerJ is an extension to Java that exposes hardware faults in a safe, principled manner to save energy with only slight sacrifices to the quality of service. More details appear in the paper “EnerJ: Approximate Data Types for Safe and General Low-Power Computation” [SDF+11] (PLDI 2011).
A checker and inference tool for ReIm [HMDE12, Hua14], an immutability type system, is available at https://github.com/proganalysis/type-inference.
The “SFlow × ReIm” system combines information flow and reference immutability. It is described in the paper “Composing polymorphic information flow systems with reference immutability” [MH13].
A checker for Generic Universe Types [DEM11], a lightweight ownership type system, is available from https://ece.uwaterloo.ca/~wdietl/ownership/ and https://github.com/opprop/universe.
The paper “Tunable static inference for Generic Universe Types” [DEM11] (ECOOP 2011) describes inference for the Generic Universe Types type system. Another implementation of Universe Types and ownership types is described in “Inference and checking of object ownership” [HDME12] (ECOOP 2012).
A checker for Safety-Critical Java (SCJ, JSR 302) [TPV10, TPNV11] is available at https://sss.cs.purdue.edu/projects/oscj/checker/checker.html. Developer resources are available at the project page https://code.google.com/archive/p/scj-jsr302/.
Loci is a checker for thread locality. For more details, see the paper “Loci: Simple thread-locality for Java” [WPM+09] (ECOOP 2009) and the thesis “The Design, Implementation and Evaluation of a Pluggable Type Checker for Thread-Locality in Java” [She11].
A checker for units and dimensions was available at https://www.lexspoon.org/expannots/.
Unlike the Units Checker that is distributed with the Checker Framework (see Chapter 20), this checker includes dynamic checks and permits annotation arguments that are Java expressions. This added flexibility, however, requires that you use a special version both of the Checker Framework and of the javac compiler.
In a regular type system, a variable has the same type throughout its scope. In a typestate system, a variable’s type can change as operations are performed on it.
The most common example of typestate is for a File object. Assume a file can be in two states, @Open and @Closed. Calling the close() method changes the file’s state. Any subsequent attempt to read, write, or close the file will lead to a run-time error. It
would be better for the type system to warn about such problems, or guarantee their absence, at compile time.
Accumulation analysis (Chapter 38) is a special case of typestate analysis. One instantiation of it is the Called Methods Checker (Chapter 7), which can check any property of the form “call method A before method B”. It also ensures that builders are used correctly.
JaTyC (Section 31.7) is a Java typestate checker.
The Checker Framework’s flow-sensitive type refinement (Section 33.7) implements a form of typestate analysis. For example, after code that tests a variable against null, the Nullness Checker (Chapter 3) treats the variable’s type as @NonNull T, for some T.
For many type systems, flow-sensitive type refinement is sufficient. But sometimes, you need full typestate analysis. This section compares the two. (Unused variables (Section 33.10) also have similarities with typestate analysis and can occasionally substitute for it. For brevity, this discussion omits them.)
A typestate analysis is easier for a user to create or extend. Flow-sensitive type refinement is built into the Checker Framework and is optionally extended by each checker. Modifying the rules requires writing Java code in your checker. By contrast, it is possible to write a simple typestate checker declaratively, by
writing annotations on the methods (such as close()) that change a reference’s typestate.
A typestate analysis can change a reference’s type to something that is not consistent with its original definition. For example, suppose that a programmer decides that the @Open and @Closed qualifiers are incomparable — neither is a subtype of the other. A typestate analysis can specify
that the close() operation converts an @Open File into a @Closed File. By contrast, flow-sensitive type refinement can only give a new type that is a subtype of the declared type — for flow-sensitive type refinement to be effective, @Closed would need to
be a child of @Open in the qualifier hierarchy (and close() would need to be treated specially by the checker).