blob: 0dd66a231f85ad9cf976692ed99508e6784a3942 [file] [log] [blame]
<!DOCTYPE html>
<html>
<head>
<meta name="generator" content=
"HTML Tidy for Linux (vers 25 March 2009), see www.w3.org">
<title>Checker Framework Tutorial - Writing an Encryption Checker -
Command Line</title>
<link href="bootstrap/css/bootstrap.css" rel="stylesheet" type=
"text/css">
<script type="text/javascript" src="bootstrap/js/bootstrap.min.js">
</script>
<link href="css/main.css" rel="stylesheet" type="text/css">
<link rel="icon" type="image/png" href=
"https://checkerframework.org/favicon-checkerframework.png">
</head>
<body>
<div class="top_liner"></div>
<div class="navbar navbar-inverse navbar-fixed-top" style=
"border-bottom: 1px solid #66d;">
<div class="navbar-inner">
<div class="contained">
<ul class="nav">
<li class="heading">Checker Framework:</li>
<li><a href="https://checkerframework.org/">Main Site</a></li>
<li><a href=
"https://checkerframework.org/manual/">
Manual</a></li>
<li><a href=
"https://groups.google.com/forum/#!forum/checker-framework-discuss">
Discussion List</a></li>
<li><a href=
"https://github.com/typetools/checker-framework/issues">Issue
Tracker</a></li>
<li><a href=
"https://github.com/typetools/checker-framework">Source
Code</a></li>
<li class="active"><a href=
"https://checkerframework.org/tutorial/">Tutorial</a></li>
</ul>
</div>
</div>
</div><img src="https://checkerframework.org/CFLogo.png" alt="Checker Framework logo">
<div class="page-header short" style=
"border-bottom: 1px solid #EEE; border-top: none;">
<h1>Checker Framework Tutorial</h1>
<h2><small>Previous <a href="security-error-cmd.html">Finding a
Security Error</a>, Download <a href="../sourcefiles.zip">Example
Sources</a></small></h2>
</div>
<div id="top">
<div class="page-header short" style="border-top: none;">
<h2>Writing an Encryption Checker
<small><em>Optional</em></small></h2>
</div>
</div>
<div id="introduction">
<p>This section of the tutorial is only for those who are interested
in writing their own type-checkers. Others may skip this
section.</p><!--Copied from the manual-->
<p>Although the Checker Framework ships with <a href=
"https://checkerframework.org/manual/#introduction">
many checkers</a>, you may wish to write your own checker because
there are other run-time problems you wish to prevent. If you do
not wish to write a new type-checker, feel free to skip this section
of the tutorial.</p>
</div>
<div id="outline">
<div class="well">
<h5>Outline</h5>
<ol>
<li><a href="#setup">An Encryption Checker</a>
</li>
<li><a href="#annotation">Write type annotation
definitions</a></li>
<li><a href="#run1">Run the Encryption Checker &mdash; 2 errors</a></li>
<li><a href="#error1">Suppress the first error</a></li>
<li><a href="#run2">Re-run the Encryption Checker &mdash; 1 error</a></li>
<li><a href="#error2">Correct the second error</a></li>
<li><a href="#run3">Re-run the Encryption Checker &mdash; no errors</a></li>
<li><a href="#learnmore">Learn more about writing your own checker</a></li>
</ol>
</div>
</div>
<div id="setup">
<h4>1. An Encryption Checker</h4>
<p>As an example, suppose that you wish to only allow encrypted
information to be sent over the internet. To do so, you can write an
Encryption Checker.</p>
</div>
<div id="annotation">
<h4>2. Write the type annotation definitions</h4>
<p>For this example, the annotation definitions have already been
written for you and appear in files <code>Encrypted.java</code>,
<code>PossiblyUnencrypted.java</code>, and
<code>PolyEncrypted.java</code>.</p>
<p><b>Compile the annotation definitions.</b></p>
<pre>
$ <strong>javacheck myqual/Encrypted.java myqual/PossiblyUnencrypted.java myqual/PolyEncrypted.java</strong>
</pre>
</div>
<div id="run1">
<h4>3. Run the Encryption Checker</h4>
<p>The <code>@Encrypted</code> annotations have already been written
in file EncryptionDemo.java. The default for types without annotations is
<code>@PossiblyUnencrypted</code>.</p>
<p><b>Invoke the compiler</b> with the Subtyping Checker.
Specify the @Encrypted, @PossiblyUnencrypted, and @PolyEncrypted annotations using the -Aquals
command-line option, and add the Encrypted, PossiblyUnencrypted, and PolyEncrypted
classfiles to the processor classpath:</p>
<pre>
$ <strong>javacheck -processor org.checkerframework.common.subtyping.SubtypingChecker -Aquals=myqual.Encrypted,myqual.PossiblyUnencrypted,myqual.PolyEncrypted encrypted/EncryptionDemo.java</strong>
encrypted/EncryptionDemo.java:21: error: [assignment] incompatible types in assignment.
@Encrypted int encryptInt = (character + OFFSET) % Character.MAX_VALUE ;
^
found : @PossiblyUnencrypted int
required: @Encrypted int
encrypted/EncryptionDemo.java:32: error: [argument] incompatible types in argument.
sendOverInternet(password);
^
found : @PossiblyUnencrypted String
required: @Encrypted String
2 errors
</pre>
</div>
<div id="error1">
<h4>4. Suppress the First Error</h4>
<p>The first error needs to be suppressed, because the string on the
left is considered "encrypted" in this encryption scheme. All
<code>@SuppressWarnings</code> should have a comment explaining why
suppressing the warning is the correct action. See the correction
below.</p>
<pre>
<b>@SuppressWarnings("encrypted") // this is the encryption algorithm</b>
private @Encrypted char encryptCharacter(char character) {
</pre>
</div>
<div id="run2">
<h4>5. Re-run the Encryption Checker</h4>
<p>You will see the following error:</p>
<pre>
$ <strong>javacheck -processor org.checkerframework.common.subtyping.SubtypingChecker -Aquals=myqual.Encrypted,myqual.PossiblyUnencrypted,myqual.PolyEncrypted encrypted/EncryptionDemo.java</strong>
encrypted/EncryptionDemo.java:34: error: [argument] incompatible types in argument.
sendOverInternet(password);
^
found : @PossiblyUnencrypted String
required: @Encrypted String
1 error
</pre>
<p>This is a real error, because the programmer is trying to send a
password over the Internet without encrypting it first.</p>
</div>
<div id="error2">
<h4>6. Correct the Second Error</h4>
<p>The password should be encrypted before it is sent over the
Internet. The correction is below.</p>
<pre>
void sendPassword() {
String password = getUserPassword();
sendOverInternet(<b>encrypt(</b>password<b>)</b>);
}
</pre>
</div>
<div id="run3">
<h4>7. Re-run the Encryption Checker</h4>
<pre>
$ <strong>javacheck -processor org.checkerframework.common.subtyping.SubtypingChecker -Aquals=myqual.Encrypted,myqual.PossiblyUnencrypted,myqual.PolyEncrypted encrypted/EncryptionDemo.java</strong>
</pre>
<p>There should be no errors.</p>
</div>
<div id="learnmore">
<h4>8. Learn more about writing your own checker</h4>
<p>For further explanations, see the Checker Framework manual, chapter
<a href=
"https://checkerframework.org/manual/#creating-a-checker">How
to create a new checker</a>.</p>
</div>
<div id="end">
<div class="page-header short">
<h2>The end of the Checker Framework Tutorial <small><br/>
<strong>Return
to the <a href="../index.html">main page</a> of the
Tutorial.</strong></small></h2>
</div>
</div>
<!--
<div class="bottom_liner well">
<a href="#">Top</a>
</div>
-->
<!-- LocalWords: Plugin plugin VM SDK plugins quals classpath
-->
<!-- LocalWords: NullnessChecker plugin's hg
-->
</body>
</html>