feat(KeyStoreAdmin)(WIP): Atomic Mutation

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy

@@ -33,6 +33,16 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
   datatype ApplyMutationResult =
     | ContinueMutation(ContinueMutation: MutationToken)
     | CompleteMutation(CompleteMutation: MutationComplete)
+  datatype AtomicMutationInput = | AtomicMutationInput (
+    nameonly Identifier: string ,
+    nameonly Mutations: Mutations ,
+    nameonly Strategy: Option<KeyManagementStrategy> := Option.None ,
+    nameonly SystemKey: SystemKey ,
+    nameonly DoNotVersion: Option<bool> := Option.None
+  )
+  datatype AtomicMutationOutput = | AtomicMutationOutput (
+    nameonly MutatedBranchKeyItems: MutatedBranchKeyItems
+  )
   datatype AwsKmsDecryptEncrypt = | AwsKmsDecryptEncrypt (
     nameonly decrypt: Option<AwsCryptographyKeyStoreTypes.AwsKms> := Option.None ,
     nameonly encrypt: Option<AwsCryptographyKeyStoreTypes.AwsKms> := Option.None
@@ -78,12 +88,14 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
       InitializeMutation := [];
       ApplyMutation := [];
       DescribeMutation := [];
+      AtomicMutation := [];
     }
     ghost var CreateKey: seq<DafnyCallEvent<CreateKeyInput, Result<CreateKeyOutput, Error>>>
     ghost var VersionKey: seq<DafnyCallEvent<VersionKeyInput, Result<VersionKeyOutput, Error>>>
     ghost var InitializeMutation: seq<DafnyCallEvent<InitializeMutationInput, Result<InitializeMutationOutput, Error>>>
     ghost var ApplyMutation: seq<DafnyCallEvent<ApplyMutationInput, Result<ApplyMutationOutput, Error>>>
     ghost var DescribeMutation: seq<DafnyCallEvent<DescribeMutationInput, Result<DescribeMutationOutput, Error>>>
+    ghost var AtomicMutation: seq<DafnyCallEvent<AtomicMutationInput, Result<AtomicMutationOutput, Error>>>
   }
   trait {:termination false} IKeyStoreAdminClient
   {
@@ -187,6 +199,21 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
       ensures DescribeMutationEnsuresPublicly(input, output)
       ensures History.DescribeMutation == old(History.DescribeMutation) + [DafnyCallEvent(input, output)]
 
+    predicate AtomicMutationEnsuresPublicly(input: AtomicMutationInput , output: Result<AtomicMutationOutput, Error>)
+    // The public method to be called by library consumers
+    method AtomicMutation ( input: AtomicMutationInput )
+      returns (output: Result<AtomicMutationOutput, Error>)
+      requires
+        && ValidState()
+      modifies Modifies - {History} ,
+               History`AtomicMutation
+      // Dafny will skip type parameters when generating a default decreases clause.
+      decreases Modifies - {History}
+      ensures
+        && ValidState()
+      ensures AtomicMutationEnsuresPublicly(input, output)
+      ensures History.AtomicMutation == old(History.AtomicMutation) + [DafnyCallEvent(input, output)]
+
   }
   datatype KeyStoreAdminConfig = | KeyStoreAdminConfig (
     nameonly logicalKeyStoreName: string ,
@@ -481,6 +508,26 @@ abstract module AbstractAwsCryptographyKeyStoreAdminService
       History.DescribeMutation := History.DescribeMutation + [DafnyCallEvent(input, output)];
     }
 
+    predicate AtomicMutationEnsuresPublicly(input: AtomicMutationInput , output: Result<AtomicMutationOutput, Error>)
+    {Operations.AtomicMutationEnsuresPublicly(input, output)}
+    // The public method to be called by library consumers
+    method AtomicMutation ( input: AtomicMutationInput )
+      returns (output: Result<AtomicMutationOutput, Error>)
+      requires
+        && ValidState()
+      modifies Modifies - {History} ,
+               History`AtomicMutation
+      // Dafny will skip type parameters when generating a default decreases clause.
+      decreases Modifies - {History}
+      ensures
+        && ValidState()
+      ensures AtomicMutationEnsuresPublicly(input, output)
+      ensures History.AtomicMutation == old(History.AtomicMutation) + [DafnyCallEvent(input, output)]
+    {
+      output := Operations.AtomicMutation(config, input);
+      History.AtomicMutation := History.AtomicMutation + [DafnyCallEvent(input, output)];
+    }
+
   }
 }
 abstract module AbstractAwsCryptographyKeyStoreAdminOperations {
@@ -569,4 +616,20 @@ abstract module AbstractAwsCryptographyKeyStoreAdminOperations {
     ensures
       && ValidInternalConfig?(config)
     ensures DescribeMutationEnsuresPublicly(input, output)
+
+
+  predicate AtomicMutationEnsuresPublicly(input: AtomicMutationInput , output: Result<AtomicMutationOutput, Error>)
+  // The private method to be refined by the library developer
+
+
+  method AtomicMutation ( config: InternalConfig , input: AtomicMutationInput )
+    returns (output: Result<AtomicMutationOutput, Error>)
+    requires
+      && ValidInternalConfig?(config)
+    modifies ModifiesInternalConfig(config)
+    // Dafny will skip type parameters when generating a default decreases clause.
+    decreases ModifiesInternalConfig(config)
+    ensures
+      && ValidInternalConfig?(config)
+    ensures AtomicMutationEnsuresPublicly(input, output)
 }

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/KeyStoreAdmin.smithy

@@ -47,7 +47,8 @@ service KeyStoreAdmin {
     VersionKey,
     InitializeMutation,
     ApplyMutation,
-    DescribeMutation
+    DescribeMutation,
+    AtomicMutation
   ],
   errors: [
     KeyStoreAdminException,
@@ -562,6 +563,63 @@ structure DescribeMutationOutput {
   MutationInFlight: MutationInFlight
 }
 
+// Atomic Mutation
+operation AtomicMutation {
+  input: AtomicMutationInput
+  output: AtomicMutationOutput
+  errors: [
+    KeyStoreAdminException
+    MutationConflictException
+    MutationInvalidException
+    UnexpectedStateException
+    aws.cryptography.keyStore#VersionRaceException
+    aws.cryptography.keyStore#KeyStorageException
+    aws.cryptography.keyStore#BranchKeyCiphertextException
+    MutationVerificationException
+    MutationToException
+    MutationFromException
+  ]
+}
+
+structure AtomicMutationInput {
+  @documentation("The identifier for the Branch Key to be mutated.")
+  @required
+  Identifier: String
+
+  @documentation("Describes the Mutation that will be applied to all Items of the Branch Key.")
+  @required
+  Mutations: Mutations
+
+  @documentation("Optional. Defaults to reEncrypt with a default KMS Client.")
+  Strategy: KeyManagementStrategy
+
+  // Smithy's Effective Docuemtnation will utilize System Key's documentation trait
+  @required
+  SystemKey: SystemKey
+
+  @documentation(
+  "Optional. Defaults to False, which Versions (or Rotates) the Branch Key,
+  creating a new Version that has only ever been in the terminal state.
+  Setting this value to True disables the rotation.
+  This is a Security vs Performance trade off.
+  Mutating a Branch Key can change the security domain of the Branch Key.
+  Some application's Threat Models benefit from ensuring a new Version
+  is created whenever a Mutation occurs,
+  allowing the application to track under which security domain data
+  was protected.
+  However, not all Threat Models call for this.
+  Particularly if Mutations are triggered in response to external actors,
+  creating a new Version for every Mutation request can needlessly grow
+  the item count of a Branch Key.")
+  DoNotVersion: Boolean
+}
+
+// TODO-Mutation-FF-Atomic: AtomicMutationOutput
+structure AtomicMutationOutput {
+  @required
+  MutatedBranchKeyItems: MutatedBranchKeyItems
+}
+
 // Errors
 
 @error("client")

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/ApplyMutation.dfy

@@ -298,6 +298,7 @@ module {:options "/functionSyntax:4" } InternalApplyMutation {
     return Success(());
   }
 
+  // TODO-Atomic: Refactor with Atomic Mutation
   method QueryForVersionsAndValidate(
     input: InternalApplyMutationInput,
     mutationToApply: StateStrucs.MutationToApply