docs/manual/external-checkers.tex - typetools/checker-framework - Git at Google

 \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
	\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