\htmlhr
\chapterAndLabel{Third-party checkers\label{external-checkers}}{third-party-checkers}

The Checker Framework has been used to build other checkers that are not
distributed together with the framework.  This chapter mentions just a few
of them.  They are listed in reverse chronological order; newer ones appear
first and older ones appear last.

They are externally-maintained, so if you have problems or questions, you
should contact their maintainers rather than the Checker Framework
maintainers.

If you want this chapter to reference your checker,
please send us a link and a short description.


% Note to maintainers:
% Sections are added to this chapter in reverse chronological order, at the top.


\sectionAndLabel{Determinism checker}{deteriminism-checker}

The
\href{https://github.com/t-rasmud/checker-framework/tree/nondet-checker}{Determinism
  Checker} ensures that a program is deterministic across executions.  A
determinismic program is easier to test, and it is easier to debug (such as
comparing executions).

The Determinism Checker focuses on sequential programs.  It detects
determinism 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.


\sectionAndLabel{AWS crypto policy compliance checker}{crypto-policy-compliance-checker}

The
\href{https://github.com/awslabs/aws-crypto-policy-compliance-checker}{AWS
  crypto policy compliance checker} checks that no weak cipher algorithms
are used with the Java crypto API\@.


\sectionAndLabel{AWS KMS compliance checker}{kms-compliance-checker}

The \href{https://github.com/awslabs/aws-kms-compliance-checker}{AWS KMS
  compliance checker} extends the Constant Value Checker (see
\chapterpageref{constant-value-checker}) to enforce that calls to Amazon
Web Services' Key Management System 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:

\begin{Verbatim}
compile group: 'software.amazon.checkerframework', name: 'aws-kms-compliance-checker', version: '1.0.2'
\end{Verbatim}

\ahref{https://mvnrepository.com/artifact/software.amazon.checkerframework/aws-kms-compliance-checker/1.0.2}{Other build systems} are similar.


\sectionAndLabel{UI Thread Checker for ReactiveX}{rx-thread-checker}

The \href{https://www.bennostein.org/ase18.pdf}{Rx Thread \& Effect Checker}~\cite{SteinCSC2018} enforces
UI Thread safety properties for stream-based Android applications and is available at
\url{https://github.com/uber-research/RxThreadEffectChecker}.


\sectionAndLabel{Glacier:  Class immutability}{glacier-immutability-checker}

\href{http://mcoblenz.github.io/Glacier/}{Glacier}~\cite{CoblenzNAMS2017}
enforces transitive class immutability in Java.  According to its webpage:

\begin{itemize}
\item
  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.
\item
  Class: the immutability of an object depends only on its class's
  immutability declaration.
\item
  Immutability: state in an object is not changable through any reference to
  the object.
\end{itemize}


\sectionAndLabel{SQL checker that supports multiple dialects}{sql-schecker}

\href{http://www.jooq.org/}{jOOQ} is a database API that lets you build
typesafe SQL queries.  jOOQ version 3.0.9 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
\url{https://blog.jooq.org/2016/05/09/jsr-308-and-the-checker-framework-add-even-more-typesafety-to-jooq-3-9/}.


\sectionAndLabel{Read Checker for CERT FIO08-J}{read-checker}

CERT
rule \href{https://www.securecoding.cert.org/confluence/display/java/FIO08-J.+Distinguish+between+characters+or+bytes+read+from+a+stream+and+-1}{FIO08-J}
describes a rule for the correct handling of characters/bytes read
from a stream.

The Read Checker enforces this rule.
It is available from
\url{https://github.com/opprop/ReadChecker}.


\sectionAndLabel{Nullness Rawness Checker}{initialization-rawness-checker}

The Nullness Rawness Checker is a 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 them, install \href{https://checkerframework.org/releases/2.9.0/}{Checker Framework version 2.9.0}.


\sectionAndLabel{Immutability checkers:  IGJ, OIGJ, and Javari\label{javari-checker}}{igj-checker}

Javari~\cite{TschantzE2005}, IGJ~\cite{ZibinPAAKE2007}, and
OIGJ~\cite{ZibinPLAE2010} 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
\href{https://checkerframework.org/releases/1.9.13/}{Checker
  Framework version 1.9.13}.

They were removed from the main distribution on June 1, 2016 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,
% the type-checkers should be rewritten from scratch and
we wanted
to focus on distributing checkers that are currently being maintained.


\sectionAndLabel{SPARTA information flow type-checker for Android}{sparta-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 SPARTA toolset is available from
\url{https://checkerframework.org/sparta/}.
The paper
\href{https://homes.cs.washington.edu/~mernst/pubs/infoflow-ccs2014.pdf}{``Collaborative
    verification of information flow for a high-assurance app store''}
  appeared in CCS 2014.


\sectionAndLabel{CheckLT taint checker}{checklt-checker}

CheckLT uses taint tracking to detect illegal information flows, such as
unsanitized data that could result in a SQL injection attack.
CheckLT is available from \url{http://checklt.github.io/}.


\sectionAndLabel{EnerJ checker}{enerj-checker}

A checker for EnerJ~\cite{SampsonDFGCG2011}, 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, is available from
\url{http://sampa.cs.washington.edu/research/approximation/enerj.html}.


\sectionAndLabel{Generic Universe Types checker}{gut-checker}

A checker for Generic Universe Types~\cite{DietlEM2011}, a lightweight ownership type
system, is available from
\url{https://ece.uwaterloo.ca/~wdietl/ownership/}.


\sectionAndLabel{Safety-Critical Java checker}{safety-critical-java-checker}

A checker for Safety-Critical Java (SCJ, JSR 302)~\cite{TangPJ2010} is available at
\url{https://www.cs.purdue.edu/sss/projects/oscj/checker/checker.html}.
Developer resources are available at the project page
\url{https://code.google.com/archive/p/scj-jsr302/}.


% In a mail from Aleš Plšek <aplsek@gmail.com> on 29.03.2011:

% Name: SCJ Checker
% WWW: http://sss.cs.purdue.edu/projects/oscj/checker/checker.html
% Source-Code Repository: http://code.google.com/p/scj-jsr302/

% Description: The SCJ Checker implements verification of a set of
% annotations defined by the Safety-Critical Java standard (JSR-302).
% The checker mainly focuses on proving memory safety of Java programs
% that use a region-based memory management.

% Publications: Static checking of safety critical Java annotations:
% http://portal.acm.org/citation.cfm?doid=1850771.1850792


\sectionAndLabel{Thread locality checker}{loci-thread-locality-checker}

Loci~\cite{WrigstadPMZV2009}, a checker for thread locality, is available at
\url{http://www.it.uu.se/research/upmarc/loci/}.
%% This URL is broken as of
% Developer resources are available at the project page
% \url{http://java.net/projects/loci/}.

% A paper was publishd in ECOOP 2009, release 0.1 was made in March 2011,
% but as of October 2013 and June 2017 the manual is still listed as "forthcoming".


% In a mail from Amanj Mahmud <amanjpro@gmail.com> on 28.03.2011:

% The plugin name:
% ``Loci: A Pluggable Type Checker for Expressing Thread Locality in
% Java''

% Project homepage: http://www.it.uu.se/research/upmarc/loci

% Project's developer's page: http://java.net/projects/loci


\sectionAndLabel{Units and dimensions checker}{units-and-dimensions-checker}

A checker for units and dimensions is available at
\url{https://www.lexspoon.org/expannots/}.

Unlike the Units Checker that is distributed with the Checker Framework
(see Section~\ref{units-checker}), 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.


\input{typestate-checker}


%%% *****
%%% DO NOT EDIT HERE!
%%% New sections go at the top of the file, not the bottom.
%%% *****


% LocalWords:  SCJ EnerJ CheckLT unsanitized JavaUI CCS IGJ OIGJ FIO08
%%  LocalWords:  jOOQ typesafe