fix(Mutations): KMS Error while generating at init is MutationFrom

aws · Jan 31, 2025 · f180e85 · f180e85
1 parent 0b94627
commit f180e85
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 6 deletions.
diff --git a/...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy b/...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy
@@ -102,7 +102,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
     grantTokens: KMS.GrantTokenList,
     kmsClient: KMS.IKMSClient
   )
-    returns (res: Result<KMS.GenerateDataKeyWithoutPlaintextResponse, Types.Error>)
+    returns (res: Result<KMS.GenerateDataKeyWithoutPlaintextResponse, KmsError>)
     requires kmsClient.ValidState()
     requires HasKeyId(kmsConfiguration) && KmsArn.ValidKmsArn?(GetKeyId(kmsConfiguration))
     requires AttemptKmsOperation?(kmsConfiguration, encryptionContext)
@@ -145,14 +145,14 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
 
     :- Need(
       && generateResponse.KeyId.Some?,
-      Types.KeyStoreException(
+      Types.KeyManagementException(
         message := "Invalid response from KMS GenerateDataKey:: Invalid Key Id")
     );
 
     :- Need(
       && generateResponse.CiphertextBlob.Some?
       && KMS.IsValid_CiphertextType(generateResponse.CiphertextBlob.value),
-      Types.KeyStoreException(
+      Types.KeyManagementException(
         message := "Invalid response from AWS KMS GenerateDataKey: Invalid ciphertext")
     );
 

diff --git a/...ptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/InitializeMutation.dfy b/...ptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/InitializeMutation.dfy
@@ -7,6 +7,7 @@ include "KmsUtils.dfy"
 include "MutationIndexUtils.dfy"
 include "SystemKey/Handler.dfy"
 include "Mutations.dfy"
+include "MutationErrorRefinement.dfy"
 
 module {:options "/functionSyntax:4" } InternalInitializeMutation {
   // StandardLibrary Imports
@@ -33,6 +34,7 @@ module {:options "/functionSyntax:4" } InternalInitializeMutation {
   import MutationIndexUtils
   import SystemKeyHandler = SystemKey.Handler
   import Mutations
+  import MutationErrorRefinement
 
   datatype InternalInitializeMutationInput = | InternalInitializeMutationInput (
     nameonly Identifier: string ,
@@ -417,12 +419,18 @@ module {:options "/functionSyntax:4" } InternalInitializeMutation {
       grantTokens := grantTokens,
       kmsClient := kmsClient
     );
-    var wrappedDecryptOnlyBranchKey :- wrappedDecryptOnlyBranchKey?
-    .MapFailure(e => Types.Error.AwsCryptographyKeyStore(e));
+
+    if (wrappedDecryptOnlyBranchKey?.Failure?) {
+      var error := MutationErrorRefinement.GenerateNewActiveException(
+        identifier := decryptOnlyEncryptionContext[Structure.BRANCH_KEY_IDENTIFIER_FIELD],
+        kmsArn := mutationToApply.Terminal.kmsArn,
+        error := wrappedDecryptOnlyBranchKey?.error);
+      return Failure(error);
+    }
 
     var newDecryptOnly := Structure.ConstructEncryptedHierarchicalKey(
       decryptOnlyEncryptionContext,
-      wrappedDecryptOnlyBranchKey.CiphertextBlob.value
+      wrappedDecryptOnlyBranchKey?.value.CiphertextBlob.value
     );
 
     :- Need(

diff --git a/...aphicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationErrorRefinement.dfy b/...aphicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationErrorRefinement.dfy
@@ -28,6 +28,29 @@ module {:options "/functionSyntax:4" } MutationErrorRefinement {
     + "\nKMS Message: " + errorMessage?.UnwrapOr("")
   }
 
+  function GenerateNewActiveException(
+    nameonly identifier: string,
+    nameonly kmsArn: string,
+    nameonly error: KMSKeystoreOperations.KmsError,
+    nameonly localOperation: string := "InitializeMutation",
+    nameonly kmsOperation: string := "GenerateDataKeyWithoutPlaintext"
+  ): (output: Types.Error)
+  {
+    var opaqueKmsError? := KmsUtils.ExtractKmsOpaque(error);
+    var kmsErrorMessage? := KmsUtils.ExtractMessageFromKmsError(error);
+    var errorContext := ParsedErrorContext(
+                          localOperation := localOperation,
+                          kmsOperation := kmsOperation,
+                          identifier := identifier,
+                          itemType := Structure.BRANCH_KEY_ACTIVE_TYPE,
+                          errorMessage? := kmsErrorMessage?);
+    var message :=
+      "Key Management denied access while creating the new Active item."
+      + " Mutation is halted. Check access to KMS ARN: " + kmsArn  + " ."
+      + "\n" + errorContext;
+    Types.MutationToException(message := message)
+  }
+
   function CreateActiveException(
     nameonly branchKeyItem: KeyStoreTypes.EncryptedHierarchicalKey,
     nameonly error: KMSKeystoreOperations.KmsError,