Checker Framework Tutorial

1. Import encryption-checker project

This project has three source files: Encrypted.java and PossibleUnencrypted.java are the type qualifier definitions and EncryptedDemo.java is the the example program that use the Encrypted checker. You will need to setup your JRE to use the Checker Framework jars, see Issue 1 below. This will fix the "TYPE_USE cannot be resolved or is not a field" error. The import myqual.Encrypted is never used warning should be ignored. When building the encryption-checker project, it is important that your -source and -target levels are set to at least 1.7 (1.8 is recommended). See Issue 2.

2. Set Up the Subtyping Checker

The Encryption Checker is built on top of the Subtyping Checker. The Subtyping Checker allows you to enforce a basic type systems by listing its qualifiers when type checking. To set up the Subtyping Checker to use the Encryption Checker's qualifiers, do the following:

3. Run the Encrypted Checker

Right Click on the src package, select Checker Framework->Run Built-in Checker->Subtyping Checker. You should see the following errors:

incompatible types in assignment.
		/*@Encrypted*/ int encryptInt = (character + OFFSET) % Character.MAX_VALUE ;
  found   : int
  required: @Encrypted int	EncryptionDemo.java	/encryption-checker/src/encrypted	
incompatible types in argument.
		sendOverInternet(password);
  found   : String
  required: @Encrypted String	EncryptionDemo.java	/encryption-checker/src/encrypted	

4. Suppress the First Error

The first error needs to be suppressed, because the string on the left is considered "encrypted" in this encryption scheme. All @SuppressWarnings should have a comment explaining why suppressing the warning is the correct action. The comment should also be initialed and dated. See the correction below.

// The SuppressWarnings is necessary because, the type system is not capable of
//validating that the return value is encrypted. -SOM 01/25/2013
@SuppressWarnings("encrypted")
private /*@Encrypted*/ char encryptCharacter(char character) {

      

5. Run the Encryption Checker

You will see the following error:

incompatible types in argument.
		sendOverInternet(password);
  found   : String
  required: @Encrypted String	EncryptionDemo.java	/encryption-checker/src/encrypted

This is a real error, because the programmer is trying to send a password over the internet without encrypting it first.

6. Correct the Second Error

The password should be encrypted before it is sent over the internet. The correction is below.

void sendPassword() {
    String password = getUserPassword();
    sendOverInternet(encrypt(password));
}