JML Specifications for KeyBlob

src/main/java/com/amazonaws/encryptionsdk/EncryptedDataKey.java

@@ -13,10 +13,112 @@
 
 package com.amazonaws.encryptionsdk;
 
+//@ model import java.util.Arrays;
+//@ model import java.nio.charset.StandardCharsets;
+
+
+//@ nullable_by_default
 public interface EncryptedDataKey {
+
+    //@// An EncryptedDataKey object abstractly contains 3 pieces of data.
+    //@// These are represented by 3 byte arrays:
+
+    //@ model public instance byte[] providerId;
+    //@ model public instance byte[] providerInformation;
+    //@ model public instance byte[] encryptedDataKey;
+
+    //@// The fields of an EncryptedDataKey may be populated via deserialization. The
+    //@// Encryption SDK design allows the deserialization routine to be called repeatedly,
+    //@// each call trying to fill in information that for some reason was not possible
+    //@// with the previous call. In some such "intermediate" states, the deserialization
+    //@// is incomplete in a way that other methods don't expect. Therefore, those methods
+    //@// should not be called in these incomplete intermediate states. The model field
+    //@// isDeserializing is true in those incomplete intermediate states, and it is used
+    //@// in method specifications.
+    //@ public model instance boolean isDeserializing;
+
+    //@// There are some complications surrounding the representations of strings versus
+    //@// byte arrays. The serialized form in message headers is always a sequence of
+    //@// bytes, but the EncryptedDataKey interface (and some other methods)
+    //@// expose the provider ID as if it were a string. Conversions (using UTF-8)
+    //@// between byte arrays and strings (which in Java use UTF-16) are not bijections.
+    //@// For example, both "\u003f".getBytes() and "\ud800".getBytes() yield a 1-byte
+    //@// array containing [0x3f], and calling `new String(..., StandardCharsets.UTF_8)`
+    //@// with either the 1-byte array [0x80] or the 3-byte array [0xef,0xbf,0xbd] yields
+    //@// the string "\ufffd". Therefore, all we can say about these conversions
+    //@// is that a given byte[]-String pair satisfies a conversion relation.
+    //@//
+    //@// The model functions "ba2s" and "s2ba" are used to specify the conversions
+    //@// between byte arrays and strings:
+    /*@ public normal_behavior
+      @   requires s != null;
+      @   ensures \result != null;
+      @ function
+      @ public model static byte[] s2ba(String s) {
+      @   return s.getBytes(StandardCharsets.UTF_8);
+      @ }
+      @*/
+    /*@ public normal_behavior
+      @   requires ba != null;
+      @   ensures \result != null;
+      @ function
+      @ public model static String ba2s(byte[] ba) {
+      @   return new String(ba, StandardCharsets.UTF_8);
+      @ }
+      @*/
+    //@// The "ba2s" and "s2ba" are given function bodies above, but the verification
+    //@// does not rely on these function bodies directly. Instead, the code (in KeyBlob)
+    //@// uses "assume" statements when it necessary to connect these functions with
+    //@// copies of their bodies that appear in the code. This is a limitation of JML.
+    //@//
+    //@// One of the properties that holds of "s2ba(s)" is that its result depends not
+    //@// on the particular String reference "s" being passed in, but only the contents
+    //@// of the string referenced by "s". This property is captured in the following
+    //@// lemma:
+    /*@ public normal_behavior
+      @   requires s != null && t != null && String.equals(s, t);
+      @   ensures Arrays.equalArrays(s2ba(s), s2ba(t));
+      @ pure
+      @ public model static void lemma_s2ba_depends_only_string_contents_only(String s, String t);
+      @*/
+    //@//
+    //@// As a specification convenience, the model function "ba2s2ba" uses the two
+    //@// model functions above to convert from a byte array to a String and then back
+    //@// to a byte array. As mentioned above, this does not always result in a byte
+    //@// array with the original contents. The "assume" statements about the conversion
+    //@// functions need to be careful not to assume too much.
+    /*@ public normal_behavior
+      @   requires ba != null;
+      @   ensures \result == s2ba(ba2s(ba));
+      @ function
+      @ public model static byte[] ba2s2ba(byte[] ba) {
+      @   return s2ba(ba2s(ba));
+      @ }
+      @*/    
+
+    //@// Here follows 3 methods that access the abstract values of interface properties.
+    //@// Something to note about these methods is that each one requires the property
+    //@// requested to be known to be non-null. For example, "getProviderId" is only allowed
+    //@// to be called when "providerId" is known to be non-null.
+
+    //@ public normal_behavior
+    //@   requires providerId != null;
+    //@   ensures \result != null;
+    //@   ensures String.equals(\result, ba2s(providerId));
+    //@ pure
     public String getProviderId();
 
+    //@ public normal_behavior
+    //@   requires providerInformation != null;
+    //@   ensures \fresh(\result);
+    //@   ensures Arrays.equalArrays(providerInformation, \result);
+    //@ pure
     public byte[] getProviderInformation();
 
+    //@ public normal_behavior
+    //@   requires encryptedDataKey != null;
+    //@   ensures \fresh(\result);
+    //@   ensures Arrays.equalArrays(encryptedDataKey, \result);
+    //@ pure
     public byte[] getEncryptedDataKey();
 }

src/main/java/com/amazonaws/encryptionsdk/exception/AwsCryptoException.java

@@ -16,25 +16,41 @@
 /**
  * This is the parent class of the runtime exceptions thrown by the AWS Encryption SDK.
  */
+//@ non_null_by_default
 public class AwsCryptoException extends RuntimeException {
     private static final long serialVersionUID = -1L;
 
+    //@ public normal_behavior
+    //@   ensures standardThrowable();
+    //@ pure
     public AwsCryptoException() {
         super();
     }
 
+    //@ public normal_behavior
+    //@   ensures standardThrowable(message);
+    //@ pure
     public AwsCryptoException(final String message) {
         super(message);
     }
 
+    //@ public normal_behavior
+    //@   ensures standardThrowable(cause);
+    //@ pure
     public AwsCryptoException(final Throwable cause) {
         super(cause);
     }
 
+    //@ public normal_behavior
+    //@   ensures standardThrowable(message,cause);
+    //@ pure
     public AwsCryptoException(final String message, final Throwable cause) {
         super(message, cause);
     }
 
+    //@ public normal_behavior
+    //@   ensures standardThrowable(message,cause);
+    //@ pure  // TODO
     public AwsCryptoException(final String message, final Throwable cause, final boolean enableSuppression,
             final boolean writableStackTrace) {
         super(message, cause, enableSuppression, writableStackTrace);

src/main/java/com/amazonaws/encryptionsdk/exception/BadCiphertextException.java

@@ -17,22 +17,39 @@
  * This exception is thrown when the values found in a ciphertext message are
  * invalid or corrupt.
  */
+//@ non_null_by_default
 public class BadCiphertextException extends AwsCryptoException {
     private static final long serialVersionUID = -1L;
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable();
+      @*/
+    //@ pure
     public BadCiphertextException() {
         super();
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message);
+      @*/
+    //@ pure
     public BadCiphertextException(final String message) {
         super(message);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(cause);
+      @*/
+    //@ pure
     public BadCiphertextException(final Throwable cause) {
         super(cause);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message,cause);
+      @*/
+    //@ pure
     public BadCiphertextException(final String message, final Throwable cause) {
         super(message, cause);
     }
-}
+}

src/main/java/com/amazonaws/encryptionsdk/exception/CannotUnwrapDataKeyException.java

@@ -18,21 +18,38 @@
 /**
  * This exception is thrown when there are no {@link DataKey}s which can be decrypted.
  */
+//@ non_null_by_default
 public class CannotUnwrapDataKeyException extends AwsCryptoException {
     private static final long serialVersionUID = -1L;
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable();
+      @*/
+    //@ pure
     public CannotUnwrapDataKeyException() {
         super();
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message);
+      @*/
+    //@ pure
     public CannotUnwrapDataKeyException(final String message) {
         super(message);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(cause);
+      @*/
+    //@ pure
     public CannotUnwrapDataKeyException(final Throwable cause) {
         super(cause);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message,cause);
+      @*/
+    //@ pure
     public CannotUnwrapDataKeyException(final String message, final Throwable cause) {
         super(message, cause);
     }

src/main/java/com/amazonaws/encryptionsdk/exception/NoSuchMasterKeyException.java

@@ -19,24 +19,45 @@
  * This exception is thrown when the SDK attempts to use a {@link MasterKey} which either doesn't
  * exist or to which it doesn't have access.
  */
+//@ non_null_by_default
 public class NoSuchMasterKeyException extends AwsCryptoException {
     private static final long serialVersionUID = -1L;
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable();
+      @*/
+    //@ pure
     public NoSuchMasterKeyException() {
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message);
+      @*/
+    //@ pure
     public NoSuchMasterKeyException(final String message) {
         super(message);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(cause);
+      @*/
+    //@ pure
     public NoSuchMasterKeyException(final Throwable cause) {
         super(cause);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message,cause);
+      @*/
+    //@ pure
     public NoSuchMasterKeyException(final String message, final Throwable cause) {
         super(message, cause);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message,cause);
+      @*/
+    //@ pure // TODO
     public NoSuchMasterKeyException(final String message, final Throwable cause,
             final boolean enableSuppression, final boolean writableStackTrace) {
         super(message, cause, enableSuppression, writableStackTrace);

src/main/java/com/amazonaws/encryptionsdk/exception/ParseException.java

@@ -17,12 +17,17 @@
  * This exception is thrown when there are not enough bytes to parse a primitive, a specified number
  * of bytes, or the bytes does not properly represent the desired object.
  */
+//@ non_null_by_default
 public class ParseException extends AwsCryptoException {
     private static final long serialVersionUID = -1L;
 
     /**
      * Constructs a new exception with no detail message.
      */
+    /*@ public normal_behavior
+      @   ensures standardThrowable();
+      @*/
+    //@ pure
     public ParseException() {
         super();
     }
@@ -33,6 +38,10 @@ public ParseException() {
      * @param message
      *            the detail message.
      */
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message);
+      @*/
+    //@ pure
     public ParseException(final String message) {
         super(message);
     }
@@ -47,6 +56,10 @@ public ParseException(final String message) {
      *            method). (A <tt>null</tt> value is permitted, and indicates that the cause is
      *            nonexistent or unknown.)
      */
+    /*@ public normal_behavior
+      @   ensures standardThrowable(cause);
+      @*/
+    //@ pure
     public ParseException(final Throwable cause) {
         super(cause);
     }
@@ -67,6 +80,10 @@ public ParseException(final Throwable cause) {
      *            method). (A <tt>null</tt> value is permitted, and indicates that the cause is
      *            nonexistent or unknown.)
      */
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message,cause);
+      @*/
+    //@ pure
     public ParseException(final String message, final Throwable cause) {
         super(message, cause);
     }

src/main/java/com/amazonaws/encryptionsdk/exception/UnsupportedProviderException.java

@@ -19,24 +19,45 @@
  * This exception is thrown when there are no {@link MasterKeyProvider}s which which support the
  * requested {@code provider} value.
  */
+//@ non_null_by_default
 public class UnsupportedProviderException extends AwsCryptoException {
     private static final long serialVersionUID = -1L;
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable();
+      @*/
+    //@ pure
     public UnsupportedProviderException() {
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message);
+      @*/
+    //@ pure
     public UnsupportedProviderException(final String message) {
         super(message);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(cause);
+      @*/
+    //@ pure
     public UnsupportedProviderException(final Throwable cause) {
         super(cause);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message,cause);
+      @*/
+    //@ pure
     public UnsupportedProviderException(final String message, final Throwable cause) {
         super(message, cause);
     }
 
+    /*@ public normal_behavior
+      @   ensures standardThrowable(message,cause);
+      @*/
+    //@ pure // TODO
     public UnsupportedProviderException(final String message, final Throwable cause,
             final boolean enableSuppression, final boolean writableStackTrace) {
         super(message, cause, enableSuppression, writableStackTrace);