Merge branch 'build-fix-2024-04-19' of github.com:aws/aws-cryptograph…

…ic-material-providers-library-dafny into build-fix-2024-04-19

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/ErrorMessages.dfy

@@ -0,0 +1,61 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+include "../Model/AwsCryptographyMaterialProvidersTypes.dfy"
+include "KeyWrapping/EdkWrapping.dfy"
+
+module ErrorMessages {
+  import Types = AwsCryptographyMaterialProvidersTypes
+  import UTF8
+  import UUID
+  import opened Wrappers
+  import EdkWrapping
+
+  const SALT_LENGTH := 16
+  const IV_LENGTH := 12
+  const VERSION_LENGTH := 16
+
+  function method IncorrectRawDataKeys(datakey: string, keyringName: string, keyProviderId: string)
+    : string
+  {
+    "EncryptedDataKey "
+    + datakey
+    + " did not match " + keyringName + ". "
+    + "Expected: keyProviderId: "
+    + keyProviderId + ".\n"
+  }
+
+  function method {:opaque} IncorrectDataKeys(encryptedDataKeys: Types.EncryptedDataKeyList, material : Types.AlgorithmSuiteInfo,errMsg: string := "")
+    : Result<string, Types.Error>
+  {
+    var expectedValue :- IncorrectDataKeysExpectedValues(encryptedDataKeys, material, errMsg);
+    Success("Unable to decrypt data key: No Encrypted Data Keys found to match. \n Expected: \n" + expectedValue)
+  }
+
+  function method {:tailrecursion} {:opaque} IncorrectDataKeysExpectedValues(encryptedDataKeys: Types.EncryptedDataKeyList, material : Types.AlgorithmSuiteInfo, errMsg: string := "")
+    : Result<string, Types.Error>
+    decreases |encryptedDataKeys|
+  {
+    if (|encryptedDataKeys| == 0) then
+      Success(errMsg)
+    else
+      var encryptedDataKey := encryptedDataKeys[0];
+      var extractedKeyProviderId :- UTF8.Decode(encryptedDataKey.keyProviderId).MapFailure(e => Types.AwsCryptographicMaterialProvidersException( message := e ));
+      var extractedKeyProviderInfo :- UTF8.Decode(encryptedDataKey.keyProviderInfo).MapFailure(e => Types.AwsCryptographicMaterialProvidersException( message := e ));
+      if (extractedKeyProviderId != "aws-kms-hierarchy") then
+        IncorrectDataKeysExpectedValues(encryptedDataKeys[1..], material, errMsg +
+                                        "KeyProviderId: " + extractedKeyProviderId +
+                                        ", KeyProviderInfo: " + extractedKeyProviderInfo + "\n")
+      else
+        var providerWrappedMaterial :- EdkWrapping.GetProviderWrappedMaterial(encryptedDataKey.ciphertext, material);
+        var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH;
+        var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH;
+        :- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, Types.AwsCryptographicMaterialProvidersException(message := "Wrong branch key version index."));
+        :- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, Types.AwsCryptographicMaterialProvidersException(message := "Incorrect ciphertext structure."));
+        var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX];
+        var branchVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => Types.AwsCryptographicMaterialProvidersException( message := e ));
+        IncorrectDataKeysExpectedValues(encryptedDataKeys[1..], material, errMsg +
+                                        "KeyProviderId: " + extractedKeyProviderId +
+                                        ", KeyProviderInfo: " + extractedKeyProviderInfo +
+                                        ", BranchKeyVersion: " + branchVersion + "\n")
+  }
+}

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy

@@ -10,6 +10,7 @@ include "AwsKmsUtils.dfy"
 include "AwsKmsKeyring.dfy"
 include "../../AwsArnParsing.dfy"
 include "../../../Model/AwsCryptographyMaterialProvidersTypes.dfy"
+include "../../ErrorMessages.dfy"
 
 module AwsKmsDiscoveryKeyring {
   import opened StandardLibrary
@@ -28,6 +29,7 @@ module AwsKmsDiscoveryKeyring {
   import opened AwsKmsKeyring
   import EdkWrapping
   import MaterialWrapping
+  import ErrorMessages
 
   class AwsKmsDiscoveryKeyring
     //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#interface
@@ -221,9 +223,13 @@ module AwsKmsDiscoveryKeyring {
       var edkTransform : AwsKmsEncryptedDataKeyTransformer := new AwsKmsEncryptedDataKeyTransformer();
       var edksToAttempt, parts :- Actions.DeterministicFlatMapWithResult(edkTransform, matchingEdks);
 
-      :- Need(0 < |edksToAttempt|,
-              Types.AwsCryptographicMaterialProvidersException(
-                message := "Unable to decrypt data key: No Encrypted Data Keys found to match."));
+      if (0 == |edksToAttempt|) {
+        var errorMessage :- ErrorMessages.IncorrectDataKeys(input.encryptedDataKeys, input.materials.algorithmSuite);
+        return Failure(
+            Types.AwsCryptographicMaterialProvidersException(
+              message := errorMessage
+            ));
+      }
 
       // We want to make sure that the set of EDKs we're about to attempt
       // to decrypt all actually came from the original set of EDKs. This is useful

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy

@@ -15,6 +15,7 @@ include "../../CMCs/StormTrackingCMC.dfy"
 include "../../CMCs/LocalCMC.dfy"
 include "../../CMCs/SynchronizedLocalCMC.dfy"
 include "../../../Model/AwsCryptographyMaterialProvidersTypes.dfy"
+include "../../ErrorMessages.dfy"
 
 module AwsKmsHierarchicalKeyring {
   import opened StandardLibrary
@@ -50,6 +51,7 @@ module AwsKmsHierarchicalKeyring {
   import HMAC
   import opened AESEncryption
   import Aws.Cryptography.Primitives
+  import ErrorMessages
 
   const BRANCH_KEY_STORE_GSI := "Active-Keys"
   const BRANCH_KEY_FIELD := "enc"
@@ -340,10 +342,13 @@ module AwsKmsHierarchicalKeyring {
       var filter := new OnDecryptHierarchyEncryptedDataKeyFilter(branchKeyIdForDecrypt);
       var edksToAttempt :- FilterWithResult(filter, input.encryptedDataKeys);
 
-      :- Need(
-        0 < |edksToAttempt|,
-        E("Unable to decrypt data key: No Encrypted Data Keys found to match.")
-      );
+      if (0 == |edksToAttempt|) {
+        var errorMessage :- ErrorMessages.IncorrectDataKeys(input.encryptedDataKeys, input.materials.algorithmSuite);
+        return Failure(
+            Types.AwsCryptographicMaterialProvidersException(
+              message := errorMessage
+            ));
+      }
 
       var decryptClosure := new DecryptSingleEncryptedDataKey(
         materials,

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy

@@ -9,6 +9,7 @@ include "Constants.dfy"
 include "AwsKmsMrkMatchForDecrypt.dfy"
 include "../../AwsArnParsing.dfy"
 include "AwsKmsUtils.dfy"
+include "../../ErrorMessages.dfy"
 
 include "../../../Model/AwsCryptographyMaterialProvidersTypes.dfy"
 
@@ -28,8 +29,10 @@ module AwsKmsKeyring {
   import Types = AwsCryptographyMaterialProvidersTypes
   import KMS = ComAmazonawsKmsTypes
   import UTF8
+  import UUID
   import EdkWrapping
   import MaterialWrapping
+  import ErrorMessages
 
   //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#interface
   //= type=implication
@@ -504,9 +507,13 @@ module AwsKmsKeyring {
       var filter := new OnDecryptEncryptedDataKeyFilter(awsKmsKey);
       var edksToAttempt :- FilterWithResult(filter, input.encryptedDataKeys);
 
-      :- Need(0 < |edksToAttempt|,
-              Types.AwsCryptographicMaterialProvidersException(
-                message := "Unable to decrypt data key: No Encrypted Data Keys found to match."));
+      if (0 == |edksToAttempt|) {
+        var errorMessage :- ErrorMessages.IncorrectDataKeys(input.encryptedDataKeys, input.materials.algorithmSuite);
+        return Failure(
+            Types.AwsCryptographicMaterialProvidersException(
+              message := errorMessage
+            ));
+      }
 
       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
       //# For each encrypted data key in the filtered set, one at a time, the

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy

@@ -10,6 +10,7 @@ include "AwsKmsUtils.dfy"
 include "../../AwsArnParsing.dfy"
 include "../../KeyWrapping/EdkWrapping.dfy"
 include "AwsKmsKeyring.dfy"
+include "../../ErrorMessages.dfy"
 
 module AwsKmsMrkDiscoveryKeyring {
   import opened StandardLibrary
@@ -21,13 +22,15 @@ module AwsKmsMrkDiscoveryKeyring {
   import AlgorithmSuites
   import Keyring
   import Materials
+  import UUID
   import UTF8
   import Types = AwsCryptographyMaterialProvidersTypes
   import KMS = Types.ComAmazonawsKmsTypes
   import opened AwsKmsUtils
   import AwsKmsKeyring
   import EdkWrapping
   import MaterialWrapping
+  import ErrorMessages
 
   class AwsKmsMrkDiscoveryKeyring
     //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-discovery-keyring.md#interface
@@ -256,9 +259,13 @@ module AwsKmsMrkDiscoveryKeyring {
         assert helper in Seq.Flatten(parts);
       }
 
-      :- Need(0 < |edksToAttempt|,
-              Types.AwsCryptographicMaterialProvidersException(
-                message := "Unable to decrypt data key: No Encrypted Data Keys found to match."));
+      if (0 == |edksToAttempt|) {
+        var errorMessage :- ErrorMessages.IncorrectDataKeys(input.encryptedDataKeys, input.materials.algorithmSuite);
+        return Failure(
+            Types.AwsCryptographicMaterialProvidersException(
+              message := errorMessage
+            ));
+      }
 
       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-discovery-keyring.md#ondecrypt
       //# For each encrypted data key in the filtered set, one at a time, the

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy

@@ -11,6 +11,7 @@ include "../../KeyWrapping/EdkWrapping.dfy"
 include "../../Keyring.dfy"
 include "../../Materials.dfy"
 include "../../AlgorithmSuites.dfy"
+include "../../ErrorMessages.dfy"
 
 module AwsKmsMrkKeyring {
   import opened StandardLibrary
@@ -30,6 +31,7 @@ module AwsKmsMrkKeyring {
   import UTF8
   import EdkWrapping
   import MaterialWrapping
+  import ErrorMessages
 
   //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#interface
   //= type=implication
@@ -482,9 +484,13 @@ module AwsKmsMrkKeyring {
       var filter := new AwsKmsUtils.OnDecryptMrkAwareEncryptedDataKeyFilter(awsKmsArn, PROVIDER_ID);
       var edksToAttempt :- FilterWithResult(filter, input.encryptedDataKeys);
 
-      :- Need(0 < |edksToAttempt|,
-              Types.AwsCryptographicMaterialProvidersException(
-                message := "Unable to decrypt data key: No Encrypted Data Keys found to match."));
+      if (0 == |edksToAttempt|) {
+        var errorMessage :- ErrorMessages.IncorrectDataKeys(input.encryptedDataKeys, input.materials.algorithmSuite);
+        return Failure(
+            Types.AwsCryptographicMaterialProvidersException(
+              message := errorMessage
+            ));
+      }
 
       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#ondecrypt
       //# For each encrypted data key in the filtered set, one at a time, the

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy

@@ -10,6 +10,7 @@ include "Constants.dfy"
 include "AwsKmsUtils.dfy"
 include "../../KeyWrapping/MaterialWrapping.dfy"
 include "../../KeyWrapping/EdkWrapping.dfy"
+include "../../ErrorMessages.dfy"
 
 include "../../../Model/AwsCryptographyMaterialProvidersTypes.dfy"
 
@@ -19,6 +20,7 @@ module AwsKmsRsaKeyring {
   import opened UInt = StandardLibrary.UInt
   import opened Actions
   import UTF8
+  import UUID
   import Aws.Cryptography.Primitives
   import Crypto = AwsCryptographyPrimitivesTypes
   import Keyring
@@ -33,6 +35,7 @@ module AwsKmsRsaKeyring {
   import MaterialWrapping
   import EdkWrapping
   import AwsKmsUtils
+  import ErrorMessages
 
   const MIN_KMS_RSA_KEY_LEN: Crypto.RSAModulusLengthBits := 2048
 
@@ -229,9 +232,13 @@ module AwsKmsRsaKeyring {
       var filter := new AwsKmsUtils.OnDecryptMrkAwareEncryptedDataKeyFilter(awsKmsArn, RSA_PROVIDER_ID);
       var edksToAttempt :- FilterWithResult(filter, input.encryptedDataKeys);
 
-      :- Need(0 < |edksToAttempt|,
-              Types.AwsCryptographicMaterialProvidersException(
-                message := "Unable to decrypt data key: No Encrypted Data Keys found to match."));
+      if (0 == |edksToAttempt|) {
+        var errorMessage :- ErrorMessages.IncorrectDataKeys(input.encryptedDataKeys, input.materials.algorithmSuite);
+        return Failure(
+            Types.AwsCryptographicMaterialProvidersException(
+              message := errorMessage
+            ));
+      }
 
       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-rsa-keyring.md#onencrypt
       //# OnEncrypt MUST calculate a Encryption Context Digest by:

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy

@@ -9,6 +9,7 @@ include "../KeyWrapping/MaterialWrapping.dfy"
 include "../KeyWrapping/EdkWrapping.dfy"
 include "../CanonicalEncryptionContext.dfy"
 include "../../Model/AwsCryptographyMaterialProvidersTypes.dfy"
+include "../ErrorMessages.dfy"
 
 module RawAESKeyring {
   import opened StandardLibrary
@@ -26,6 +27,7 @@ module RawAESKeyring {
   import Seq
   import MaterialWrapping
   import EdkWrapping
+  import ErrorMessages
 
   import Aws.Cryptography.Primitives
 
@@ -338,11 +340,13 @@ module RawAESKeyring {
             errors := errors + [unwrapOutput.error];
           }
         } else {
+          var extractedKeyProviderId :- UTF8.Decode(input.encryptedDataKeys[i].keyProviderId).MapFailure(e => Types.AwsCryptographicMaterialProvidersException( message := e ));
           errors := errors + [
             Types.AwsCryptographicMaterialProvidersException(
-              message :="EncrypedDataKey "
-              + Base10Int2String(i)
-              + " did not match AESKeyring. " )
+              message := ErrorMessages.IncorrectRawDataKeys(Base10Int2String(i),
+                                                            "AESKeyring",
+                                                            extractedKeyProviderId
+              ))
           ];
         }
       }

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawRSAKeyring.dfy

@@ -8,6 +8,7 @@ include "../Materials.dfy"
 include "../KeyWrapping/MaterialWrapping.dfy"
 include "../KeyWrapping/EdkWrapping.dfy"
 include "../../Model/AwsCryptographyMaterialProvidersTypes.dfy"
+include "../ErrorMessages.dfy"
 
 module RawRSAKeyring {
   import opened StandardLibrary
@@ -27,6 +28,7 @@ module RawRSAKeyring {
   import opened Seq
   import MaterialWrapping
   import EdkWrapping
+  import ErrorMessages
 
 
   //= aws-encryption-sdk-specification/framework/raw-rsa-keyring.md#public-key
@@ -353,10 +355,13 @@ module RawRSAKeyring {
             errors := errors + [unwrapOutput.error];
           }
         } else {
-          errors := errors + [Types.AwsCryptographicMaterialProvidersException( message :=
-                                                                                  "EncryptedDataKey "
-                                                                                  + Base10Int2String(i)
-                                                                                  + " did not match RSAKeyring. ")
+          var extractedKeyProviderId :- UTF8.Decode(input.encryptedDataKeys[i].keyProviderId).MapFailure(e => Types.AwsCryptographicMaterialProvidersException( message := e ));
+          errors := errors + [
+            Types.AwsCryptographicMaterialProvidersException(
+              message := ErrorMessages.IncorrectRawDataKeys(Base10Int2String(i),
+                                                            "RSAKeyring",
+                                                            extractedKeyProviderId
+              ))
           ];
         }
       }