diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy index 3173b024c..88d622d12 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy @@ -102,7 +102,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations { grantTokens: KMS.GrantTokenList, kmsClient: KMS.IKMSClient ) - returns (res: Result) + returns (res: Result) 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/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/InitializeMutation.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/InitializeMutation.dfy index 7732aec74..ae2792028 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/InitializeMutation.dfy +++ b/AwsCryptographicMaterialProviders/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/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationErrorRefinement.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationErrorRefinement.dfy index 25aecf34d..4dd1e04ae 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutationErrorRefinement.dfy +++ b/AwsCryptographicMaterialProviders/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,