forked from typetools/checker-framework
-
Notifications
You must be signed in to change notification settings - Fork 11
/
new-contributor-projects.html
1712 lines (1487 loc) · 69.1 KB
/
new-contributor-projects.html
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
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html>
<html>
<head>
<title>Projects for new contributors</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<!-- This link works on the web, but not from the file system. -->
<link rel="icon" type="image/png" href="favicon-checkerframework.png">
</head>
<body>
<img src="CFLogo.png" alt="Checker Framework logo" />
<h1>Projects for new contributors</h1> <!-- omit from toc -->
<p>Contents:</p>
<!-- start toc. do not edit; run html-update-toc instead -->
<ul>
<li><a href="#introduction">Introduction</a>
<ul>
<li><a href="#get-started">How to get started: do a case study</a></li>
<li><a href="#ask-questions">How to get help and ask questions</a></li>
<li><a href="#types-of-projects">Types of projects</a></li>
</ul></li>
<li><a href="#evaluate-type-system">Evaluate a type system or a Checker Framework feature</a>
<ul>
<li><a href="#case-study-signature">Signature strings</a></li>
<li><a href="#case-study-signedness">Preventing mixed signed/unsigned computations</a></li>
<li><a href="#Whole-program_type_inference">Whole-program type inference</a></li>
<li><a href="#sound-by-default">Sound checking by default</a></li>
<li><a href="#compare-other-tools">Comparison to other tools</a></li>
<li><a href="#case-study-android-support">Android support annotations</a></li>
</ul></li>
<li><a href="#annotate-library">Annotate a library</a>
<ul>
<li><a href="#choose-a-library">Choosing a library to annotate</a></li>
<li><a href="#case-study-nullness-guava">Guava library</a></li>
</ul></li>
<li><a href="#create-new-type-system">Create a new type system</a>
<ul>
<li><a href="#ownership-type-system">Ownership type system</a></li>
<li><a href="#non-empty-checker">Non-Empty Checker for precise handling of Queue.peek() and poll()</a></li>
<li><a href="#iteration-checker">Iteration Checker to prevent <code>NoSuchElementException</code></a></li>
<li><a href="#custom-tainting-checking">Preventing injection vulnerabilities via specialized taint analysis</a></li>
<li><a href="#track-unsupported-operations">Warn about unsupported operations</a></li>
<li><a href="#overflow">Overflow checking</a></li>
<li><a href="#index-checker-mutable-length">Index checking for mutable length data structures</a></li>
<li><a href="#nullness-bug-detector">Nullness bug detector</a></li>
</ul></li>
<li><a href="#cf-other">Enhance the toolset</a>
<ul>
<li><a href="#hint-about-annotated-library-methods">Indicate library methods that should be used instead</a></li>
<li><a href="#index-errors">Improving error messages</a></li>
<li><a href="#java-expression-parser">Java expression parser</a></li>
<li><a href="#dataflow">Dataflow enhancements</a></li>
<li><a href="#Purity_analysis">Side effect analysis, also known as purity analysis</a></li>
<li><a href="#javadoc">Javadoc support</a></li>
</ul></li>
<li><a href="#apply">How to apply to GSoC (relevant to GSoC students only)</a></li>
</ul>
<!-- end toc -->
<h1 id="introduction">Introduction</h1>
<p>
The <a href="https://eisop.github.io/cf/">Checker Framework</a> is an
innovative programming tool that prevents bugs at development
time, before they escape to production.
</p>
<p>
Java's type system prevents some bugs, such as <code>int count =
"hello";</code>. However, it does not prevent other bugs, such as null
pointer dereferences, concurrency errors, disclosure of private
information, incorrect internationalization, out-of-bounds indices, etc.
<em>Pluggable type-checking</em> replaces a
programming language's built-in type system with a more powerful,
expressive one.
</p>
<p>
We have created over 20
<a href="https://eisop.github.io/cf/manual/#introduction">new type
systems</a>, and other people have created
<a href="https://eisop.github.io/cf/manual/#third-party-checkers">over 30
more</a>.
A type system is not just a
bug-finding tool: it is a verification tool that gives a <em>guarantee</em> that
no errors (of certain types) exist in your program. Even though it is
powerful, it is easy to use. It follows the standard typing rules
that programmers already know, and it fits into their workflow.
</p>
<p>
The Checker Framework is popular: it is used daily at Amazon, Google, Meta,
Oracle, Uber, on Wall Street, and in other companies from big to small. It is
attractive to programmers who care about their craft and the quality of
their code. The Checker Framework is the motivation for Java's type
annotations feature. It has received multiple awards.
<!-- at conferences such as JavaOne. -->
With this widespread use, there is a need for people to help with the
project: everything from bug fixes, to new features, to case studies, to
integration with other tools. We welcome your contribution!
</p>
<p>
Why should you join this project? It's popular, so you will have an
impact. It makes code more robust and secure, which is a socially
important purpose.
You will get to scratch your own itch by creating tools that solve
problems that frustrate you.
It is accessible even to junior software engineers and undergraduates.
(Many undergraduate students have published scientific papers, such as
<a href="https://homes.cs.washington.edu/~mernst/pubs/determinism-icse2021-abstract.html">Jason Waataja</a>,
<a href="https://homes.cs.washington.edu/~mernst/pubs/array-indexing-issta2018-abstract.html">Vlastimil Dort</a>
<a href="https://homes.cs.washington.edu/~mernst/pubs/format-string-issta2014-abstract.html">Gene Kim</a>,
<a href="https://homes.cs.washington.edu/~mernst/pubs/format-string-issta2014-abstract.html">Siwakorn Srisakaokul</a>,
<a href="https://homes.cs.washington.edu/~mernst/pubs/verigames-ftfjp2012-abstract.html">Stephanie Dietzel</a>,
<a href="https://homes.cs.washington.edu/~mernst/pubs/verigames-ftfjp2012-abstract.html">Nathaniel Mote</a>,
<a href="https://homes.cs.washington.edu/~mernst/pubs/verigames-ftfjp2012-abstract.html">Brian Walker</a>,
<a href="https://homes.cs.washington.edu/~mernst/pubs/regex-types-ftfjp2012-abstract.html">Eric Spishak</a>,
<a href="https://homes.cs.washington.edu/~mernst/pubs/mutability-jase2009-abstract.html">Jaime</a>
<a href="https://homes.cs.washington.edu/~mernst/pubs/infer-refimmutability-ecoop2008-abstract.html">Quinonez</a>,
<a href="https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-issta2008-abstract.html">Matthew Papi</a>,
<a href="https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-issta2008-abstract.html">Mah</a><a
href="https://homes.cs.washington.edu/~mernst/pubs/ownership-immutability-oopsla2010-abstract.html">mood</a>
<a href="https://homes.cs.washington.edu/~mernst/pubs/immutability-generics-fse2007-abstract.html">Ali</a>,
and
<a href="https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-issta2008-abstract.html">Telmo Correa</a>;
and even more have made significant contributions to the tool.)
Finally, we have a lot of fun on this project!
</p>
<p>
<b>Prerequisites:</b> You should be very comfortable with the Java
programming language and its type system. You should know how a type
system helps you and how it can hinder you. You should be willing to
dive into a moderately-sized codebase.
You should understand fundamental object-oriented programming concepts,
such as
<a href="https://en.wikipedia.org/wiki/Liskov_substitution_principle">behavioral
subtyping</a>: subtyping theory
permits argument types to change contravariantly (even though Java forbids it
for reasons related to overloading), whereas return types may change
<a href="https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29">covariantly</a>
both in theory and in Java.
</p>
<p>
<b>Potential projects:</b>
Most of this document lists potential projects. The projects are
grouped roughly from easiest to most challenging.
</p>
<h2 id="get-started">How to get started: do a case study</h2>
<p>
To <b>get started</b>, first do a case study of using the Checker
Framework: that is, run the Checker Framework on some program.
If you have already done so, you can skip this section.
Otherwise, a case study gives you experience in using the Checker
Framework, and it may reveal bugs in either the Checker Framework or in
the program it is analyzing.
</p>
<p>
<b>Why should you start with a case study?</b>
<!-- , instead of diving right into fixing
bugs, designing a new type system, or making other changes to the Checker
Framework?
-->
Before you can contribute to any project, you must
understand the tool from a user point of view, including its strengths,
weaknesses, and how to use it.
Using the Checker Framework is the best way to
learn about it and determine whether you would enjoy
contributing to it.
</p>
<p>
<b>What is the purpose of a case study?</b>
The primary result of your case study is that you will discover bugs in the
subject program, or you will verify that it has no bugs (of some particular
type). If you find bugs in open-source code,
and let us know when they are resolved.<br/>
Another outcome of your case study is that you may discover bugs, limitations,
or usability problems in the Checker Framework. Please
<a href="https://eisop.github.io/cf/manual/#reporting-bugs">report them</a>.
We'll try to fix them, or they might give you inspiration for
improvements you would like to make to the Checker Framework.
</p>
<p>
You might want to start with a small program that you wrote,
then repeat the process with a larger open-source program or library.
</p>
<ol>
<li>
<a href="https://eisop.github.io/cf/manual/#installation">Install</a>
the Checker Framework.
<li>
<a href="https://eisop.github.io/cf/manual/#how-to-read-this-manual">Review
the Checker Framework documentation.</a>
<li>
Choose an existing library or program to type-check.
A program that is about 1000 lines long is a good size for your first
use of the Checker Framework, but you could use a smaller or larger one.
The library or program should be under active maintenance; don't choose one
that has not had a commit in the past year.
You will find the case study easier if you are already familiar with
the program, or if it is written in good style.
<li>
Choose one type system, from
among <a href="https://eisop.github.io/cf/manual/#introduction">those
distributed with the Checker Framework</a>, that is appropriate for the
program.
<li>
If the program is hosted on GitHub, fork it and create a new branch for
your work. (Leave the master branch of your fork unchanged
from upstream.)
<li>
Annotate the program, based on its documentation.
<br/>
Please do <em>not</em> make changes unrelated to annotating the
program, such as inserting/removing whitespace or sorting
the <code>import</code> statements. Doing so bloats the size of the
diffs and makes it hard to understand the essential changes.
<li>
Change the build system so that building the annotated branch runs the type-checker.
<li>
Run the type-checker. If it issues
warnings, <a href="https://eisop.github.io/cf/manual/#handling-warnings">correct them</a>.
This might require adding more annotations,
fixing bugs in the program, or suppressing warnings.
Be sure that the program's test suite continues to pass.
Repeat until
the type-checker passes on the program.
<ul>
<li>Don't add an <code>if</code> statement that always succeeds, just
to suppress a warning. Convince yourself that both branches can
execute, or else don't add the <code>if</code> statement.
<li>If you add a <code>@SuppressWarnings</code> annotation,
<a href="https://eisop.github.io/cf/manual/#suppresswarnings-best-practices-smallest-scope">write
it on the smallest possible scope</a> and
<a href="https://eisop.github.io/cf/manual/#suppresswarnings-best-practices-justification">explain
why</a> the checker warning is a false positive and you are certain
the code is safe.
</ul>
<li>
Share it with us; we would be happy to give you feedback.
<p>
The subject line should be descriptive (not just "Case study", but
"Nullness case study of Apache Commons Exec library").
You should give us access to
<ul>
<li>the original (unannotated) version of the program,
<li>the annotated version of the program, and
<li>the exact command that runs the type-checker from the command
line.
</ul>
The best way to give all this information is a pointer to your GitHub
fork of the library.
</ol>
<p>
You can also try to fix problems that you find and submit a
<a href="https://github.com/eisop/checker-framework/pulls">pull
request</a>, but that is <em>not</em> a requirement to get started,
because not all problems are good for new contributors.
</p>
<h2 id="ask-questions">How to get help and ask questions</h2>
<p>
We are very happy to answer your questions, and we are eager to interact
with you! It's OK to have questions, and your questions can lead to
improvements in the documentation and the tool.
</p>
<p>
Before you ask a question, read this file and the
<a href="https://eisop.github.io/cf/manual/#troubleshooting">"Troubleshooting"
section</a> of the Checker Framework manual
(including <a href="https://eisop.github.io/cf/manual/#reporting-bugs">"How
to report problems"</a>),
and also search in the
<a href="https://eisop.github.io/cf/manual/">Checker Framework manual</a>
for the answer.
Don't send us a message
that says nothing but “please guide me”
or “tell me how to fix this issue from the issue tracker”.
</p>
<p>
When you ask a question, please
tell us what you have tried, tell us what went wrong or
where you got stuck, and ask a concrete technical question that will
help you get past your problem. If you can do that, then definitely ask
your question, because we don't want you to be stuck or frustrated.
</p>
<p>
When you send email,
please use standard email etiquette, such as: avoid all-caps; use a
descriptive subject line; don't put multiple different topics in a single
email message; start a new thread with a new subject line
when you change the topic; don't clutter discussions with irrelevant
remarks; don't use screenshots (unless there is a problem with a GUI), but
instead cut-and-paste the output or code into your message;
if you are making a guess, clearly indicate that it is a guess and
your grounds for it. Bug
reports should be
<a href="https://eisop.github.io/cf/manual/#reporting-bugs">complete</a>
and should usually be
<a href="https://eisop.github.io/cf/manual/#reporting-bugs">reported</a>
to the issue tracker.
</p>
<h2 id="types-of-projects">Types of projects</h2>
<p>
Here are some possible focuses for a project:
</p>
<ul>
<li>
<a href="#evaluate-type-system">Evaluate</a> a recently-written type
system, or a feature used by multiple type systems.
</li>
<li>
<a href="#annotate-library">Annotate</a> a popular library, so that it
is easier to type-check clients of the library.
</li>
<li>
<a href="#create-new-type-system">Create</a> a new type system, to
prevent some Java programming error.
</li>
<li>
<a href="#cf-other">Enhance</a> a type system or the Checker Framework
itself.
</li>
</ul>
<p>
This document gives a few suggestions in each category.
</p>
<h1 id="evaluate-type-system">Evaluate a type system or a Checker Framework feature</h1>
<p>
These projects evaluate a recently-written type system or a feature used
by multiple type systems.
Using the type systems on real code is our most important source of new ideas and improvements.
Many people have started out “just” doing a case
study but have ended up making deep, fundamental contributions and even
publishing scientific papers about their discoveries.
</p>
<p>
One possible outcome is to identify
weaknesses in the type-checker so that we can improve it. Another
possible outcome is to provide evidence that the type-checker is
effective and convince more users to adopt it. You will probably
also discover defects (bugs) in the codebase being type-checked.
</p>
<h2 id="case-study-signature">Signature strings</h2>
<p>
Determine whether the <a href="https://asm.ow2.io/">ASM library</a>, or
some other library, properly handles signature strings.
</p>
<p>
Some challenging aspects of this case study are:
</p>
<ul>
<li>
Some libraries define their own new signature string formats (!), which
you need to define in the Signature String Checker.
</li>
<li>
Sometimes the library's documentation is incorrect, and in other cases the
string format is not defined.
</li>
</ul>
<h2 id="case-study-signedness">Preventing mixed signed/unsigned computations</h2>
<!-- This project is duplicated in the highlight section and in
the Checker Framework's new-contributor-projects.html . -->
<p>
An unsigned integer's bits are interpreted differently than a signed
integer's bits. It is meaningless to add a signed and an unsigned integer
— the result will be nonsense bits. The same is true of printing and
of other numeric operators such as multiplication and comparison.
</p>
<p>
We have
a <a href="https://eisop.github.io/cf/manual/#signedness-checker">prototype
compile-time verification tool</a> that detects and prevents these
errors. The goal of this project is to perform case studies to determine
how often programmers make signedness errors (our initial investigation
suggests that this is common!) and to improve the verification tool.
</p>
<p>
The research questions are:
</p>
<ul>
<li>How often do programmers make signedness errors?
</li>
<li>Is it feasible to automatically detect signedness errors? What techniques are useful?
</li>
<li>What is the false positive rate of a signedness verification tool — that is, false alarms from the tool?
</li>
<li>How much effort is required from a programmer?
</li>
</ul>
<p>
The methodology is:
</p>
<ul>
<li>find open-source projects that use unsigned arithmetic
</li>
<li>run the verification tool on them
</li>
<li>for each tool warning, determine whether it is a defect in the
project or a limitation of the verification tool. For example, the Signedness
Checker does not currently handle boxed integers and BigInteger; these
haven't yet come up in case studies but could be worthwhile enhancements.
You may also need to write more annotations for libraries such as the
JDK.
</li>
<li>submit bug reports against the project, or improve the verification tool
</li>
</ul>
<p>
A good way to find projects that use unsigned arithmetic is to find a
library that supports unsigned
arithmetic, then search on GitHub for projects that use that library.
</p>
<p>
Here are some relevant libraries.
</p>
<ul>
<li>In the JDK's <code>Integer</code>
and <code>Long</code>, these include
<code>compareUnsigned</code>,
<code>divideUnsigned</code>,
<code>parseUnsignedInt</code>,
<code>remainderUnsigned</code>, and
<code>toUnsignedLong</code>.
<br/>
Classes like <code>DataInputStream</code>, <code>ObjectInputStream</code>,
and <code>RandomAccessFile</code> have <code>readUnsignedByte</code>.
<br/>
<code>Arrays</code> has <code>compareUnsigned</code>.
The JDK is already annotated; search for <code>@Unsigned</code> within
<a href="https://github.com/eisop/jdk">https://github.com/eisop/jdk</a>.
</li>
<li>
In Guava, see
its <a href="https://github.com/google/guava/wiki/PrimitivesExplained#unsigned-support">unsigned
support</a>, such
as <a href="https://guava.dev/releases/snapshot-jre/api/docs/com/google/common/primitives/UnsignedBytes.html">UnsignedBytes</a>,
<a href="https://guava.dev/releases/snapshot-jre/api/docs/com/google/common/primitives/UnsignedLong.html">UnsignedLong</a>,
<a href="https://guava.dev/releases/snapshot-jre/api/docs/com/google/common/primitives/UnsignedLongs.html">UnsignedLongs</a>,
etc.
Guava is already annotated; search for <code>@Unsigned</code> within
<a href="https://github.com/eisop/guava">https://github.com/eisop/guava</a>.
</li>
<li>The <a href="https://github.com/jOOQ/jOOU">jOOU</a> library consists of support for unsigned
integers.</li>
</ul>
<p>
Another possibility is to find Java projects that <em>could</em> use an
unsigned arithmetic library but do not. For
example, <a href="https://github.com/bcgit/bc-java">bc-java</a> defines
its own unsigned libraries, and some other programs might do direct bit
manipulation.
</p>
<!-- Not a good choice because this is just example code, not an actively-maintained project.
<li>Project
Nayuki: <a href="https://www.nayuki.io/page/forcing-a-files-crc-to-any-value">CRC</a>, <a href="https://www.nayuki.io/page/notepadcrypt-format-decryptor-java">crypt</a>, <a href="https://www.nayuki.io/page/native-hash-functions-for-java">hash</a>.</li>
-->
<!-- Not a good choice because it is not under active development:
<li><a href="https://bytonic.de/html/jake2.html">Jake2</a></li>
-->
<h2 id="Whole-program_type_inference">Whole-program type inference</h2>
<p>
A type system is useful because it prevents certain errors. The downside
of a type system is the effort required to write the types. Type inference
is the process of writing the types for a program.
</p>
<p>
The Checker Framework includes
a <a href="https://eisop.github.io/cf/manual/#whole-program-inference">whole-program
inference</a> that inserts type qualifiers in the user's program.
It works well on some programs, but needs more enhancements to work well on
all programs.
</p>
<h2 id="sound-by-default">Sound checking by default</h2>
<p>
By default, the Checker Framework is
<a href="https://eisop.github.io/cf/manual/#unsound-by-default">unsound
in</a> <a href="https://eisop.github.io/cf/manual/#nullness-lint">several</a>
<a href="https://github.com/typetools/checker-framework/issues/986">circumstances</a>.
“Unsound” means that the Checker Framework
may report no warning even though the program can misbehave at run time.
</p>
<p>
The reason that the Checker Framework is unsound is that we believe that
enabling these checks would cause too many false positive warnings:
warnings that the Checker Framework issues because it cannot prove that the
code is safe (even though a human can see that the code is safe). Having
too many false positive warnings would irritate users and lead them not to
use the checker at all, or would force them to simply disable those checks.
</p>
<p>
We would like to do studies of these command-line options to see whether
our concern is justified. Is it prohibitive to enable sound checking? Or can we
think of enhancements that would let us turn on those checks that are
currently disabled by default?
</p>
<p>
There is no need to annotate new code for this project. Just use existing
annotated codebases, such as those that are type-checked as part of the
Checker
Framework's <a href="https://github.com/eisop/checker-framework/blob/master/azure-pipelines.yml">Azure
Pipeline</a>. In other words, you can start by enabling Azure
Pipelines for your fork and then changing the default behavior in a
branch. The Azure Pipelines job will show you what new warnings appear.
</p>
<h2 id="compare-other-tools">Comparison to other tools</h2>
<p>
Many other tools exist for prevention of programming errors, such as
Error Prone, NullAway, FindBugs, JLint, PMD, and IDEs such as Eclipse and
IntelliJ. These tools
are not as powerful as the Checker Framework (some are bug finders rather
than verification tools, and some perform a shallower analysis), but they
may be easier to use.
Programmers who use these tools wonder, "Is it worth my time to switch to
using the Checker Framework?"
</p>
<p>
The goal of this project is to perform a head-to-head comparison of as
many different tools as possible. You will quantify:
</p>
<ul>
<li>the number of annotations that need to be written</li>
<li>the number of bugs detected</li>
<li>the number of bugs missed</li>
<li>the number of false positive warnings</li>
</ul>
<p>
This project will help programmers to choose among the different tools
— it will show when a programmer should or should not use the
Checker Framework.
This project will also indicate how each tool should be improved.
</p>
<p>
One place to start would be with an old version of a program that is
known to contain bugs. Or, start with the latest version of the program
and re-introduce fixed bugs. (Either of these is more realistic than
introducing artificial bugs into the program.) A possibility would be to
use the Lookup program that has been used in previous case studies.
</p>
<h2 id="case-study-android-support">Android support annotations</h2>
<p>
Android uses its own annotations that are similar to some in the Checker
Framework. Examples include the
<a href="https://tips.seebrock3r.me/annotations-to-support-your-contracts-609ff259d5df">Android
Studio support annotations</a>,
including <code>@NonNull</code>, <code>@IntRange</code>, <code>@IntDef</code>,
and others.
</p>
<p>
The goal of this project is to implement support for these annotations.
That is probably as simple as creating aliased annotations
by calling method <code>addAliasedTypeAnnotation()</code>
in <a href="https://eisop.github.io/cf/api/org/checkerframework/framework/type/AnnotatedTypeFactory.html">AnnotatedTypeFactory</a>.
</p>
<p>
Then, do a case study to show the utility (or not) of
pluggable type-checking, by comparison with how Android Studio currently
checks the annotations.
</p>
<h1 id="annotate-library">Annotate a library</h1>
<p>
These projects annotate a library, so that it is easier to
type-check clients of the library. Another benefit is that this may find
bugs in the library. It can also give evidence for the usefulness of
pluggable type-checking, or point out ways to improve the Checker
Framework.
</p>
<p>
When type-checking a method call, the Checker Framework uses the method
declaration's annotations.
This means that in order to type-check code that uses a library, the
Checker Framework needs an annotated version of the library.
</p>
<p>
The Checker Framework comes with a
few <a href="https://search.maven.org/search?q=annotatedlib">annotated
libraries</a>. Increasing this number will make the Checker Framework even
more useful, and easier to use.
</p>
<p>
After you have <a href="#choose-a-library">chosen a library</a>,
fork the library's source code, adjust
its <a href="https://eisop.github.io/cf/manual/#external-tools">build
system</a> to run the Checker Framework, and add annotations to it until
the type-checker issues no warnings.
</p>
<p>
Before you get started, be sure to read
<a href="https://eisop.github.io/cf/manual/#get-started-with-legacy-code">How
to get started annotating legacy code</a>. More generally, read the
<a href="https://eisop.github.io/cf/manual/#how-to-read-this-manual">relevant
sections of the Checker Framework manual</a>.
</p>
<h2 id="choose-a-library">Choosing a library to annotate</h2>
<p>
There are several ways to <b>choose a library</b> to annotate:
</p>
<ul>
<li>
The best way to choose a library is to try to annotate a program and notice
that library annotations are needed in order to type-check the program.
</li>
<li>
Alternately, you can
choose a <a href="https://docs.google.com/spreadsheets/d/17x_jKkGquEFq7LBQhS9HGXiG7iIl2AlXoPGfB6N5_bw">popular
Java library</a>.
</li>
</ul>
<p>
When annotating a library, it is important to type-check both the library
and at least one client that uses it. Type-checking the client will
ensure that the library annotations are accurate.
</p>
<p>
Whatever library you choose, you will need to deeply understand its
source code. You will find it easier to work with a library that is
well-designed and well-documented.
</p>
<p>
You should choose a library that is
not <a href="https://search.maven.org/search?q=org.checkerframework.annotatedlib">already
annotated</a>. There are two exceptions to this.
</p>
<ul>
<li>
A library might be annotated for one type system, but you add
annotations for a different type system. One advantage of this is that
the library's build system is already set up to run the Checker
Framework. You can tell which type systems a library is annotated for
by examining its source code.
</li>
<li>
A library might be annotated, but the annotations have not been
verified by running the type-checker on the library source code. You
would verify that the annotations in the library are correct.
</li>
</ul>
<h2 id="case-study-nullness-guava">Guava library</h2>
<p>
Guava is already partially annotated with nullness annotations — in
part by Guava's developers, and in part by the Checker Framework team.
However, Guava does not yet type-check without errors. Doing so could
find more errors (the Checker Framework has found nullness and indexing
errors in Guava in the past) and would be a good case study to learn the
limitations of the Nullness Checker.
</p>
<h1 id="create-new-type-system">Create a new type system</h1>
<p>
The Checker Framework is shipped with <a href="https://eisop.github.io/cf/manual/#introduction">about 20 type-checkers</a>. Users can
<a href="https://eisop.github.io/cf/manual/#creating-a-checker">create a
new checker</a> of their own. However, some users don't want to go to
that trouble. They would like to have more type-checkers packaged with the
Checker Framework for easy use.
</p>
<p>
Each of these projects requires you to design a <a href="https://eisop.github.io/cf/manual/#creating-a-checker">new type system</a>,
implement it, and perform case studies to demonstrate that it is both
usable and effective in finding/preventing bugs.
</p>
<h2 id="ownership-type-system">Ownership type system</h2>
<p>
The <a href="https://eisop.github.io/cf/manual/#resource-leak-annotations">lightweight
ownership mechanism</a> of the Resource Leak Checker is not implemented as
a type system, but it should be. That would enable writing ownership
annotations on generic type arguments, like <code>List<@Owning
Socket></code>. It would also enable changing the Resource Leak Checker
so that non-<code>@Owning</code> formal parameters do not have
their <a href="https://eisop.github.io/cf/manual/#resource-leak-owning-fields"><code>@MustCall</code>
annotation erased</a>.
</p>
<!-- See https://docs.google.com/document/d/14Q0iIH_3cfKvGnoLtYDck64MEKkvvPKaW5t7nvaNuVA -->
<p>
We have some notes on possible implementation strategies.
</p>
<h2 id="non-empty-checker">Non-Empty Checker for precise handling of Queue.peek() and poll()</h2>
<p>
The Nullness Checker issues a false positive warning for this code:
</p>
<pre>
import java.util.PriorityQueue;
import org.checkerframework.checker.nullness.qual.NonNull;
public class MyClass {
public static void usePriorityQueue(PriorityQueue<@NonNull Object> active) {
while (!(active.isEmpty())) {
@NonNull Object queueMinPathNode = active.peek();
}
}
}
</pre>
<p>
The Checker Framework does not determine that <code>active.peek()</code> returns a non-null value in this context.
</p>
<p>
The contract of <code>peek()</code> is that it returns a non-null value if the queue is not empty and the queue contains no null values.
</p>
<p>
To handle this code precisely, the Nullness Checker needs to know, for each queue, whether it is empty.
This is analogous to how the Nullness Checker tracks whether a particular
value <a href="https://eisop.github.io/cf/manual/#map-key-checker">is a key in a map</a>.
</p>
<p>
It should be handled the same way: by adding a new subchecker, called the
Nonempty Checker, to the Nullness Checker. Its types are:
</p>
<ul>
<li><code>@UnknownNonEmpty</code> — the queue might or might not be empty
<li><code>@NonEmpty</code> — the queue is definitely non-empty
</ul>
<p>
There is a start at this type-checker in branch <code>nonempty-checker</code>. It:
</p>
<ul>
<li>defines the annotations
</li>
<li>creates the integration into the Nullness Checker
</li>
</ul>
<p>
However, it is not done. (In fact, it doesn't even compile.)
For information about what needs to be done, see <a href="https://github.com/typetools/checker-framework/issues/399">issue #399</a>.
</p>
<p>
When you are done, the Nullness Checker should issue only the <code>// ::</code> diagnostics from <code>checker/tests/nullness/IsEmptyPoll.java</code> — no more and no fewer.
You can test that by running the Nullness Checker on the file, and when you are done you should delete the <code>// @skip-test</code> line so that the file is run as part of the Checker Framework test suite.
</p>
<h2 id="iteration-checker">Iteration Checker to prevent <code>NoSuchElementException</code></h2>
<!--
There is a draft implementation in branch "iteration-checker" of
https://github.com/t-rasmud .
However, it needs the side-effects-only pull request.
There is a draft paper at $t/iteration-checking-paper/
-->
<p>
A Java program that uses an <code>Iterator</code> can
throw <code>NoSuchElementException</code> if the program
calls <code>next()</code> on the <code>Iterator</code> but
the <code>Iterator</code> has no more elements to iterate over. Such
exceptions even occur in production code (for example,
in <a href="https://github.com/eclipse/rdf4j/issues/3090">Eclipse's
rdf4j</a>).
</p>
<p>
We would like a compile-time guarantee that this run-time error will never
happen. Our analysis will statically determine whether
the <code>hasNext()</code> method would return true. The basic type system
has two type qualifiers: <code>@HasNext</code> is a subtype
of <code>@UnknownHasNext</code>.
</p>
<p>
A variable's type is <code>@HasNext</code> if the program
calls <code>hasNext()</code> and it returns true. Implementing this is
easy (see
the <a href="https://eisop.github.io/cf/manual/#creating-dataflow">dataflow
section</a> in
the <a href="https://eisop.github.io/cf/manual/#creating-a-checker">"How
to create a new checker" chapter</a>). The analysis can also permit some
calls to <code>next()</code> even if the programmer has <em>not</em>
called <code>hasNext()</code>. For example, a call to <code>next()</code>
is permitted on a newly-constructed iterator that is made from a non-empty
collection. (This special case could build upon
the <a href="#non-empty-checker">Non-Empty Checker</a> mentioned above.)
There are probably other special cases, which experimentation will reveal.
</p>
<p>
Parts of this are already implemented, but it needs to be enhanced. Once
case studies have demonstrated its effectiveness, then it can be released
to the world, and a scientific paper can be written.
</p>
<h2 id="custom-tainting-checking">Preventing injection vulnerabilities via specialized taint analysis</h2>
<!-- This project is duplicated in the highlight section and in the Checker
Framework's new-contributor-projects.html . -->
<p>
Many security vulnerabilities result from use of untrusted data without sanitizing it first.
Examples include SQL injection, cross-site scripting, command injection, and many more.
Other vulnerabilities result from leaking private data, such as credit card numbers.
</p>
<p>
We have built a generalized taint analysis that can address any of these problems. However, because it is so general, it is not very useful. A user must customize it for each particular problem.
</p>
<p>
The goal of this project is to make those customizations, and to evaluate their usefulness.
A specific research question is: "To what extent is a general taint analysis useful in eliminating a wide variety of security vulnerabilities? How much customization, if any, is needed?"
</p>
<p>
The generalized taint analysis is the Checker Framework's
a <a href="https://eisop.github.io/cf/manual/#tainting-checker">Tainting
Checker</a>. It requires customization to a particular domain:
</p>
<ul>
<li>
rename the <code>@Tainted</code> and <code>@Untainted</code> qualifiers
to something more specific (such as <code>@Private</code>
or <code>@PaymentDetails</code> or <code>@HtmlQuoted</code>), and
<li>
annotate libraries.
</ul>
<p>
The first part of this project is to make this customization easier to do
— preferably, a user will not have to change any code in the Checker
Framework (the
<a href="https://eisop.github.io/cf/manual/#subtyping-checker">Subtyping
Checker</a> already works this way).
As part of making customization easier, a user should be able to specify
multiple levels of taint — many information classification hierarchies
have more than two levels. For example, the US government separates
information into four categories: Unclassified, Confidential, Secret, and
Top Secret.
</p>
<p>
The second part of this project is to provide several examples, and do case
studies showing the utility of compile-time taint checking.
</p>
<p>
Possible examples include:
</p>
<ul>
<li>SQL injection
<li>OS command injection
<li>the <code>@PrivacySource</code> and <code>@PrivacySink</code>
annotations used by the Meta <a href="https://fbinfer.com/">Infer
static analyzer</a>.
<li>information flow
<li>many of the <a href="http://cwe.mitre.org/top25/">CWE/SANS most
dangerous software programming errors</a> (and the "on the cusp" ones too)
<!-- More details appear in these files:
~/research/games/notes/notes
~/prof/grants/2012-02-darpa-verigames/proposal/top25-as-types.pdf
-->
</ul>
<p>
For some microbenchmarks, see the Juliette test suite for Java from CWE.
</p>
<h2 id="track-unsupported-operations">Warn about unsupported operations</h2>
<!-- This project is duplicated in the highlight section and in the Checker
Framework's new-contributor-projects.html. -->
<p>
In Java, some objects do not fully implement their interface; they
throw <code>UnsupportedOperationException</code> for some operations. One
example is <a href="https://docs.oracle.com/en/java/javase/11/core/creating-immutable-lists-sets-and-maps.html">unmodifiable collections</a>. They throw the exception when a
mutating operation is called, such
as <code>add</code>, <code>addAll</code>, <code>put</code>, <code>remove</code>,
etc.
</p>
<p>
The goal of this project is to
design a compile-time verification tool to track which operations might not be supported.
This tool will issue a warning whenever
an <code>UnsupportedOperationException</code> might occur at run time.
This helps programmers to avoid run-time exceptions (crashes) in their Java programs.
</p>
<p>
The research questions include:
</p>
<ul>
<li>Is it is possible to build a verification tool to prevent <code>UnsupportedOperationException</code>? What design is effective?
</li>
<li>How difficult is such a tool to use, in terms of programmer effort and number of false alarms?
</li>
<li>Are potential <code>UnsupportedOperationException</code> exceptions
pervasive in Java programs? Is it possible to eliminate them?
</li>
</ul>
<p>
The methodology is:
</p>
<ol>
<li>design a static (compile-time) analysis
</li>
<li>implement it
</li>