1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
|
\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{Object Construction Checker}{object-construction-checker}
The \href{https://github.com/kelloggm/object-construction-checker}{Object
Construction Checker} verifies that your code correctly uses the builder
pattern, never omitting a required argument. The checker has built-in
support for \href{https://projectlombok.org/}{Lombok} and
\href{https://github.com/google/auto/blob/master/value/userguide/index.md}{AutoValue}. Programmers
can extend it to other builders by writing method specifications.
\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://plv.colorado.edu/benno/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
|
