JML Specifications for KeyBlob

[slyubomirsky]

Issue #, if available:
N/A

Description of changes:
These changes add JML (Java Modeling Language) formal specifications to several files that have been verified using OpenJML (https://github.com/OpenJML/OpenJML). Included also is a README-JML file that gives a summary of the semantics of JML (with a short summary at the top). From the perspective of the Java compiler, JML annotations are all comments, so annotations should not force changes to ordinary code.

The files annotated in this request were meant to be those needed to ensure a specification for KeyBlob could verify. The following is a listing:

• the exceptions in encryptionsdk.exception
• encryptionsdk.internal.PrimitivesParser
• encryptionsdk.EncryptionDataKey
• encryptionsdk.model.KeyBlob

All the annotations verify (i.e., the implementation is guaranteed to match the behavior described in the JML specification) using the development version of OpenJML.

Note that this version of KeyBlob.java includes code that addresses the issues identified in #71, so this code will have to be synced to the changes in that PR once it is approved. (Done)

Most of the annotations in this PR were supplied by @RustanLeino and @davidcok. We are in the process of annotating and verifying more files that we can submit as PRs later; we would be very interested to know what you think would be the best ways to supply these annotations and the best ways to have them correspond to the intent of the code (and the message format specifications).

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

[mattsb42-aws]

Some thoughts before digging into this in detail.

• Does the JML readme contain anything specific to this project? From a brief skim it looks like it's just a general overview of JML. It seems to me that it would be better to simply give a brief intro to "what is JML" and link to the relevant components of the OpenJML docs (that I assume exist).
• How would we run OpenJML to verify these specifications? We will need to have tests that we can run (probably manually at first, but eventually as part of our CI) that will actually perform the verification.

[slyubomirsky]

The JML readme is not specific to this project. I had included it in a previous JML annotation project as a simpler guide than the official docs (http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_toc.html), so I included it here as well, but we could stick to the official docs if that's preferable.

As for running OpenJML, the Github project includes installation instructions here: https://github.com/OpenJML/OpenJML/wiki/OpenJML-Development-Environment-Setup
The files included here verify using the development build of OpenJML in Eclipse with the following arguments (I believe the Eclipse setup will have most of these bundled in a predefined $ARGS macro):
-esc -no-staticInitWarning -progress -timeout 60 -spec-math=bigint -code-math=safe -minQuant -classpath src/main/java -specspath src/main/java -dir src/main/java/com/amazonaws/encryptionsdk/model