| <!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 — 2 errors</a></li> |
| |
| <li><a href="#error1">Suppress the first error</a></li> |
| |
| <li><a href="#run2">Re-run the Encryption Checker — 1 error</a></li> |
| |
| <li><a href="#error2">Correct the second error</a></li> |
| |
| <li><a href="#run3">Re-run the Encryption Checker — 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> |