chore(KSA-Model): more Mutation Operation changes (#955)

Explicitly:
- Change InitializeMutationFlag from a union to an enum for ToString reasons
- Model `DoNotVersion` flag for Initialize Mutation
- Refactor Describe Mutation output to detail Input so resume can be done
- Refactor System Key to be optional, detailing that TrustStorage is the default
- More errors
- Smithy changes from PR feedback on #854
- Correction of spelling mistakes
- Mutation Token's UUID is required

Why change the flag to an enum?

Dafny/Smithy-Dafny's support for Union's results in structures that do not print well.
The intention of the  `InitializeMutationFlag` is to inform customers
about the result of their request.

Such information may,
possibly even should,
be logged.

Initialize Mutation and Apply Mutation MUST
ensure that the UUID of the Index and Commitment agree.
Apply MUST ensure that the UUID of the Commitment and Token agree.
The Mutation Token's UUID is REQUIRED.
It is how we track a mutation,
much like how CFN tracks a change set.

Fixed bug where UUID is a reserved word in DDB.

Refactored some of the error messages.
Utilize Java Example to demonstrate resume and restart.
Finally, addressed some of the feedback on PR #854.

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/Storage.smithy

@@ -101,7 +101,7 @@ list OverWriteEncryptedHierarchicalKeys {
 }
 
 @documentation(
-"To avoid information loss, overwrites to any itme in the Key Store
+"To avoid information loss, overwrites to any item in the Key Store
 are done conditioned on the old value.")
 structure OverWriteMutationIndex {
   @required
@@ -130,22 +130,22 @@ structure MutationCommitment {
   UUID: String
 
   @required
-  @documentation("A commitment of the Original Mutable Properities of the Branch Key.")
+  @documentation("A commitment of the Original Mutable Properties of the Branch Key.")
   Original: Blob
 
   @required
-  @documentation("A commitment of the Terminal Mutable Properities of the Branch Key.")
+  @documentation("A commitment of the Terminal Mutable Properties of the Branch Key.")
   Terminal: Blob
 
   @required
-  @documentation("Description of the input to Initizlize Mutation.")
+  @documentation("Description of the input to initialize a Mutation.")
   Input: Blob 
 
   @required
   CiphertextBlob: Blob
 }
 
-@documentation("Information on an in-flight Mutation of a Branch Key.")
+@documentation("Information of an in-flight Mutation of a Branch Key.")
 structure MutationIndex {
   @required
   @documentation("The Branch Key under Mutation.")
@@ -256,9 +256,11 @@ operation GetKeyStorageInfo {
 }
 
 @documentation(
-"Gets the ACTIVE branch key and the beacon key,
-and looks for a Mutation Commitment & Index,
-returning them if found.")
+"Retrieves the items necessary to initialize a Mutation, 
+while checking for any in-flight Mutations.  
+These items are the ACTIVE branch key and the beacon key.
+If a Mutation is already in-flight for this Branch Key,
+the in-flight Mutation's Commitment and Index are also returned.")
 operation GetItemsForInitializeMutation {
   input: GetItemsForInitializeMutationInput
   output: GetItemsForInitializeMutationOutput
@@ -286,7 +288,7 @@ operation WriteInitializeMutation {
 @documentation(
 "Creates a Mutation Index, conditioned on the Mutation Commitment.
 Used in the edge case where the Commitment exists and Index does not.
-The Index may have been deleted to restart the mutation from the very begining.
+The Index may have been deleted to restart the mutation from the very beginning.
 ")
 operation WriteMutationIndex {
   input: WriteMutationIndexInput
@@ -329,9 +331,16 @@ operation QueryForVersions {
 in the terminal state of a Mutation,
 a page of version (decrypt only) items,
 conditioned on:
-- every version already exsisting
-- every version's enc has not changed
+- every version already existing
+- every version's cipher-text had not changed
 - the Mutation Commitment has not changed
+
+If the Mutation is complete,
+the Mutation Index and Mutation Commitment are deleted.
+Otherwise,
+the Mutation Index is updated,
+conditioned on it not having been changed since
+it was last read.
 ")
 operation WriteMutatedVersions {
   input: WriteMutatedVersionsInput
@@ -509,20 +518,20 @@ structure WriteInitializeMutationInput {
   @required
   @documentation("
   The active representation of this branch key,
-  generated with the Mutation's terminal properities.  
+  generated with the Mutation's terminal properties.
   The plain-text cryptographic material of the Active must be the same as the Version.")
   Active: OverWriteEncryptedHierarchicalKey,
   @required
   @documentation("
   The decrypt representation of this branch key version,
-  generated with the Mutation's terminal properities.  
+  generated with the Mutation's terminal properties.
   The plain-text cryptographic material of the `Version` must be the same as the `Active`.")
   Version: WriteInitializeMutationVersion,
   @required
   @documentation("
   The mutated HMAC key used to support searchable encryption.
   The cryptographic material is identical to the existing beacon,
-  but is now authorized with the Mutation's terminal properities.")
+  but is now authorized with the Mutation's terminal properties.")
   Beacon: OverWriteEncryptedHierarchicalKey,
   @required // Smithy will copy documentation traits from existing shapes
   MutationCommitment: MutationCommitment
@@ -543,20 +552,20 @@ structure WriteAtomicMutationInput {
   @required
   @documentation("
   The active representation of this branch key,
-  generated with the Mutation's terminal properities.  
+  generated with the Mutation's terminal properties.
   The plain-text cryptographic material of the Active must be the same as the Version.")
   Active: OverWriteEncryptedHierarchicalKey,
   @required
   @documentation("
   The decrypt representation of this branch key version,
-  generated with the Mutation's terminal properities.  
+  generated with the Mutation's terminal properties.
   The plain-text cryptographic material of the `Version` must be the same as the `Active`.")
   Version: WriteInitializeMutationVersion,
   @required
   @documentation("
   The mutated HMAC key used to support searchable encryption.
   The cryptographic material is identical to the existing beacon,
-  but is now authorized with the Mutation's terminal properities.")
+  but is now authorized with the Mutation's terminal properties.")
   Beacon: OverWriteEncryptedHierarchicalKey
   @documentation(
   "List of version (decrypt only) items of a Branch Key to overwrite conditionally.")
@@ -569,9 +578,9 @@ structure QueryForVersionsInput {
   @documentation(
   "Optional.
   If set, Query will start at this index and read forward.  
-  Otherwise, Query will start at the indexes begining.
+  Otherwise, Query will start at the indexes beginning.
   The Default Storage is DDB;
-  see Amazon DynamoDB's defination of exclusiveStartKey for details.
+  see Amazon DynamoDB's definition of exclusiveStartKey for details.
   Note: While the Default Storage is DDB,
   the Key Store transforms the exclusiveStartKey into an opaque representation.")
   ExclusiveStartKey: Blob
@@ -588,7 +597,7 @@ structure QueryForVersionsOutput {
   "If none-empty, Query did not finish searching storage.  
   Next Query should resume from here.
   The Default Storage is DDB;
-  see Amazon DynamoDB's defination of exclusiveStartKey for details.
+  see Amazon DynamoDB's definition of exclusiveStartKey for details.
   Note: While the Default Storage is DDB,
   the Key Store transforms the exclusiveStartKey into an opaque representation.")
   @required

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy

@@ -542,7 +542,8 @@ module {:options "/functionSyntax:4" } CreateKeys {
     );
     var overWrite := Types.OverWriteEncryptedHierarchicalKey(
       Item := active,
-      Old := oldActiveItem);
+      Old := oldActiveItem
+    );
 
     var _ :- storage.WriteNewEncryptedBranchKeyVersion(
       Types.WriteNewEncryptedBranchKeyVersionInput(

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DefaultKeyStorageInterface.dfy

@@ -39,6 +39,9 @@ module DefaultKeyStorageInterface {
     map[
       "#pk" := Structure.BRANCH_KEY_IDENTIFIER_FIELD,
       "#sk" := Structure.TYPE_FIELD]
+  // Ideally, MAX_PAGE would be Types.UInt.uint8, but the size of sequence is always an int
+  const DDB_MAX_MUTATION_WRITE_PAGE_SIZE: int := 98
+  const DDB_MAX_MUTATION_WRITE_PAGE_SIZE_str: string := "98"
 
   datatype ConditionExpression =
     | BRANCH_KEY_NOT_EXIST
@@ -49,17 +52,11 @@ module DefaultKeyStorageInterface {
   // in the case statement to evaluate a literal.
   const MUTATION_COMMITMENT_TYPE := "branch:MUTATION_COMMITMENT" // Structure.MUTATION_COMMITMENT_TYPE
   const MUTATION_INDEX_TYPE := "branch:MUTATION_INDEX" // Structure.MUTATION_INDEX_TYPE
-  // const BRANCH_KEY_ACTIVE_TYPE := "branch:ACTIVE" // Structure.BRANCH_KEY_ACTIVE_TYPE
-  // const BEACON_KEY_TYPE_VALUE :=  "beacon:ACTIVE" // Structure.BEACON_KEY_TYPE_VALUE
-  // const VERSION_TYPE_PREFIX := "branch:version:" // Structure.BRANCH_KEY_TYPE_PREFIX
 
   lemma TypesAreCorrect()
     ensures
       && MUTATION_COMMITMENT_TYPE == Structure.MUTATION_COMMITMENT_TYPE
       && MUTATION_INDEX_TYPE == Structure.MUTATION_INDEX_TYPE
-    // && BRANCH_KEY_ACTIVE_TYPE == Structure.BRANCH_KEY_ACTIVE_TYPE
-    // && BEACON_KEY_TYPE_VALUE == Structure.BEACON_KEY_TYPE_VALUE
-    // && VERSION_TYPE_PREFIX == Structure.BRANCH_KEY_TYPE_PREFIX
   {}
 
   class {:termination false} DynamoDBKeyStorageInterface
@@ -560,12 +557,12 @@ module DefaultKeyStorageInterface {
         return Failure(
             Types.KeyStorageException(
               message :=
-                "DDB request to Write Mutated Versions was failed by DDB with TransactionCanceledException. "
+                "DDB request to Write Mutated Versions failed with DynamoDB's TransactionCanceledException. "
                 + "This MAY be caused by a race between hosts mutating the same Branch Key ID. "
                 + "The Mutation has NOT completed. "
                 + "Table Name: "+ ddbTableName
                 + "\tBranch Key ID: " + input.MutationCommitment.Identifier
-                + "\tDDB Exception Message: \n" + ddbResponse?.error.Message.UnwrapOr("")));
+                + "\tDynamoDB Exception Message: \n" + ddbResponse?.error.Message.UnwrapOr("")));
       }
       var ddbResponse :- ddbResponse?
       .MapFailure(
@@ -580,7 +577,7 @@ module DefaultKeyStorageInterface {
     }
 
 
-    method GetMutation' ( input: Types.GetMutationInput )
+    method {:vcs_split_on_every_assert} GetMutation' ( input: Types.GetMutationInput )
       returns (output: Result<Types.GetMutationOutput, Types.Error>)
       requires ValidState()
       modifies Modifies - {History}
@@ -1260,23 +1257,23 @@ module DefaultKeyStorageInterface {
           ));
     }
 
-    /** Transaction OverWrite up to 99 Decryt Only Items, with a Global Condition on the M-Lock.*/
+    /** Transaction OverWrite up to 98 Decryt Only Items,
+       with a Global Condition on the M-Commitment.
+       The Mutation Index is also updated via an Optimistic Lock.
+       If the mutation is complete, the M-Commitment & M-Index are deleted.
+     */
     method WriteMutatedVersions' ( input: Types.WriteMutatedVersionsInput )
       returns (output: Result<Types.WriteMutatedVersionsOutput, Types.Error>)
-      requires
-        && ValidState()
+      requires && ValidState()
       modifies Modifies - {History}
-      // Dafny will skip type parameters when generating a default decreases clause.
       decreases Modifies - {History}
-      ensures
-        && ValidState()
+      ensures unchanged(History) && ValidState()
       ensures WriteMutatedVersionsEnsuresPublicly(input, output)
-      ensures unchanged(History)
     {
       /** Validate Input */
       :- Need(
-        |input.Items| < 98,
-        Types.KeyStorageException(message:="DynamoDB Encrypted Key Storage can only write page sizes less than 99."
+        |input.Items| < DDB_MAX_MUTATION_WRITE_PAGE_SIZE,
+        Types.KeyStorageException(message:="DynamoDB Encrypted Key Storage can only write page sizes less than " + DDB_MAX_MUTATION_WRITE_PAGE_SIZE_str + "."
         ));
       :- Need(
         0 < |input.MutationCommitment.Original|,
@@ -1607,13 +1604,18 @@ module DefaultKeyStorageInterface {
         "attribute_exists(#pk)"
         + " AND original = :original"
         + " AND terminal = :terminal"
-        + " AND " + Structure.ENC_FIELD + " = :encOld",
-      ExpressionAttributeNames := map["#pk" := Structure.BRANCH_KEY_IDENTIFIER_FIELD], // "#pk":="branch-key-id"
+        + " AND " + Structure.ENC_FIELD + " = :encOld"
+        + " AND #uuid = :" + Structure.M_UUID,
+      ExpressionAttributeNames := map[
+        "#pk" := Structure.BRANCH_KEY_IDENTIFIER_FIELD, // "#pk":="branch-key-id"
+        "#uuid" := Structure.M_UUID // "#uuid" := "uuid"
+      ],
       ExpressionAttributeValues :=
         map[
           ":original" := DDB.AttributeValue.B(mLock.Original),
           ":terminal" := DDB.AttributeValue.B(mLock.Terminal),
-          ":encOld" := DDB.AttributeValue.B(mLock.CiphertextBlob)
+          ":encOld" := DDB.AttributeValue.B(mLock.CiphertextBlob),
+          ":" + Structure.M_UUID := DDB.AttributeValue.S(mLock.UUID)
         ]
     )
   }
@@ -1649,12 +1651,17 @@ module DefaultKeyStorageInterface {
       ConditionExpression :=
         "attribute_exists(#pk)"
         + " AND " + Structure.M_PAGE_INDEX + " = :" + Structure.M_PAGE_INDEX + "Old"
-        + " AND " + Structure.ENC_FIELD + " = :" + Structure.ENC_FIELD + "Old",
-      ExpressionAttributeNames := map["#pk" := Structure.BRANCH_KEY_IDENTIFIER_FIELD], // "#pk":="branch-key-id"
+        + " AND " + Structure.ENC_FIELD + " = :" + Structure.ENC_FIELD + "Old"
+        + " AND #uuid = :" + Structure.M_UUID,
+      ExpressionAttributeNames := map[
+        "#pk" := Structure.BRANCH_KEY_IDENTIFIER_FIELD, // "#pk":="branch-key-id"
+        "#uuid" := Structure.M_UUID // "#uuid" := "uuid"
+      ],
       ExpressionAttributeValues :=
         map[
           ":" + Structure.M_PAGE_INDEX + "Old" := DDB.AttributeValue.B(oldIndex.PageIndex),
-          ":" + Structure.ENC_FIELD + "Old" := DDB.AttributeValue.B(oldIndex.CiphertextBlob)
+          ":" + Structure.ENC_FIELD + "Old" := DDB.AttributeValue.B(oldIndex.CiphertextBlob),
+          ":" + Structure.M_UUID := DDB.AttributeValue.S(oldIndex.UUID)
         ]
     )
   }