test(Keystore): assert that lying branch keys are rejected

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy

@@ -95,4 +95,9 @@ module Fixtures {
   const kmsKeyAlias := "arn:aws:kms:us-west-2:370957321024:alias/postalHorn"
   const postalHornBranchKeyId := "682dfba7-4c35-491d-8d6a-5a9c56194061"
   const postalHornBranchKeyActiveVersion := "6b7a8ef4-8c1c-4f63-b196-a6ef7e496e50"
+
+  // Creation of this particular illegal Branch Key is detailed here:
+  // `git rev-parse --show-toplevel`/cfn/lyingBranchKeyCreation.md
+  const lyingBranchKeyId := "kms-arn-attribute-is-lying"
+  const lyingBranchKeyDecryptOnlyVersion := "129c5c87-308a-41c9-8b9d-a27f66e915f4"
 }

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestLyingBranchKey.dfy

@@ -0,0 +1,134 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../src/Index.dfy"
+include "Fixtures.dfy"
+  //include "../src/ErrorMessages.dfy"
+
+// These tests assert that a particular form of
+// illegal Branch Key is always correctly handled.
+// Creation of this particular illegal Branch Key is detailed here:
+// `git rev-parse --show-toplevel`/cfn/lyingBranchKeyCreation.md
+// The Branch Key's Item says it is protected by KMS-ARN Fixtures.dfy#postalHornKeyArn,
+// but the KMS requests were actually executed against KMS-ARN Fixtures.dfy#keyArn.
+// Thus, all Keystore Operations related to the Branch Key MUST fail with exceptions from KMS.
+module TestLyingBranchKey {
+  import Types = AwsCryptographyKeyStoreTypes
+  import KMS = Com.Amazonaws.Kms
+  import DDB = Com.Amazonaws.Dynamodb
+  import ComAmazonawsKmsTypes
+  import KeyStore
+  import opened Wrappers
+  import opened Fixtures
+  import UTF8
+  import ErrorMessages = KeyStoreErrorMessages
+
+  method {:test} TestGetActiveKeyForLyingBranchKey() {
+    var kmsClient :- expect KMS.KMSClient();
+    var ddbClient :- expect DDB.DynamoDBClient();
+    var kmsConfig := Types.KMSConfiguration.kmsKeyArn(postalHornKeyArn);
+    var keyStoreConfig := Types.KeyStoreConfig(
+      id := None,
+      kmsConfiguration := kmsConfig,
+      logicalKeyStoreName := logicalKeyStoreName,
+      grantTokens := None,
+      ddbTableName := branchKeyStoreName,
+      ddbClient := Some(ddbClient),
+      kmsClient := Some(kmsClient)
+    );
+    var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
+
+    var result := keyStore.GetActiveBranchKey(
+      Types.GetActiveBranchKeyInput(
+        branchKeyIdentifier := lyingBranchKeyId
+      ));
+    expect result.Failure?;
+    match result.error {
+      case ComAmazonawsKms(nestedError) =>
+        expect nestedError.IncorrectKeyException?;
+      case _ => expect false, "Lying Branch Key SHOULD Fail with KMS IncorrectKeyException.";
+    }
+  }
+
+  method {:test} TestGetBranchKeyVersionForLyingBranchKey() {
+    var kmsClient :- expect KMS.KMSClient();
+    var ddbClient :- expect DDB.DynamoDBClient();
+    var kmsConfig := Types.KMSConfiguration.kmsKeyArn(postalHornKeyArn);
+    var keyStoreConfig := Types.KeyStoreConfig(
+      id := None,
+      kmsConfiguration := kmsConfig,
+      logicalKeyStoreName := logicalKeyStoreName,
+      grantTokens := None,
+      ddbTableName := branchKeyStoreName,
+      ddbClient := Some(ddbClient),
+      kmsClient := Some(kmsClient)
+    );
+    var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
+
+    var result := keyStore.GetBranchKeyVersion(
+      Types.GetBranchKeyVersionInput(
+        branchKeyIdentifier := lyingBranchKeyId,
+        branchKeyVersion := lyingBranchKeyDecryptOnlyVersion
+      ));
+    expect result.Failure?;
+    match result.error {
+      case ComAmazonawsKms(nestedError) =>
+        expect nestedError.IncorrectKeyException?;
+      case _ => expect false, "Lying Branch Key SHOULD Fail with KMS IncorrectKeyException.";
+    }
+  }
+
+  method {:test} TestGetBeaconKeyForLyingBranchKey() {
+    var kmsClient :- expect KMS.KMSClient();
+    var ddbClient :- expect DDB.DynamoDBClient();
+    var kmsConfig := Types.KMSConfiguration.kmsKeyArn(postalHornKeyArn);
+    var keyStoreConfig := Types.KeyStoreConfig(
+      id := None,
+      kmsConfiguration := kmsConfig,
+      logicalKeyStoreName := logicalKeyStoreName,
+      grantTokens := None,
+      ddbTableName := branchKeyStoreName,
+      ddbClient := Some(ddbClient),
+      kmsClient := Some(kmsClient)
+    );
+    var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
+
+    var result := keyStore.GetBeaconKey(
+      Types.GetBeaconKeyInput(
+        branchKeyIdentifier := lyingBranchKeyId
+      ));
+    expect result.Failure?;
+    match result.error {
+      case ComAmazonawsKms(nestedError) =>
+        expect nestedError.IncorrectKeyException?;
+      case _ => expect false, "Lying Branch Key SHOULD Fail with KMS IncorrectKeyException.";
+    }
+  }
+
+  method {:test} TestVersionKeyForLyingBranchKey() {
+    var kmsClient :- expect KMS.KMSClient();
+    var ddbClient :- expect DDB.DynamoDBClient();
+    var kmsConfig := Types.KMSConfiguration.kmsKeyArn(postalHornKeyArn);
+    var keyStoreConfig := Types.KeyStoreConfig(
+      id := None,
+      kmsConfiguration := kmsConfig,
+      logicalKeyStoreName := logicalKeyStoreName,
+      grantTokens := None,
+      ddbTableName := branchKeyStoreName,
+      ddbClient := Some(ddbClient),
+      kmsClient := Some(kmsClient)
+    );
+    var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
+
+    var result := keyStore.VersionKey(
+      Types.VersionKeyInput(
+        branchKeyIdentifier := lyingBranchKeyId
+      ));
+    expect result.Failure?;
+    match result.error {
+      case ComAmazonawsKms(nestedError) =>
+        expect nestedError.IncorrectKeyException?;
+      case _ => expect false,   "Lying Branch Key SHOULD Fail with KMS IncorrectKeyException.";
+    }
+  }
+}

cfn/lyingBranchKeyCreation.md

@@ -0,0 +1,113 @@
+To validate that the MPL protects from Branch Keys lying about the KMS ARN used to encrypt it,
+we need to create a "lying Branch Key".
+
+The following commands were used to do so,
+with the AWS CLI @ `aws-cli/2.15.60 Python/3.11.9 Darwin/22.6.0 source/x86_64`.
+
+#### Set Common Variables:
+
+```sh
+createTime=`printf '%.26sZ\n' $(gdate -u +%FT%H:%M:%S:%N)`
+branchKeyId="kms-arn-attribute-is-lying"
+kmsArn="arn:aws:kms:us-west-2:370957321024:key/bc127593-f7da-452c-a1f3-cd34c46f81f8"
+tableName="KeyStoreDdbTable"
+type="branch:version:$(uuidgen | tr "[A-Z]" "[a-z]")"
+```
+
+#### KMS GenerateDataKeyWithoutPlaintext for DECRYPT_ONLY:
+
+Execute the following, and persist the result as DECRYPT_ONY.json.
+
+```sh
+aws kms generate-data-key-without-plaintext \
+    --key-id arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126 \
+    --number-of-bytes 32 \
+    --encryption-context "kms-arn=$kmsArn, branch-key-id=$branchKeyId, hierarchy-version=1, create-time=$createTime, tablename=$tableName, type=$type"
+```
+
+#### KMS ReEncrypt for ACTIVE
+
+Execute the following, and persist the result as ACTIVE.json.
+
+Set `cipherText` as the `"CipherTextBlob"` from DECRYPT_ONLY.json.
+
+```sh
+typeActive="branch:ACTIVE"
+cipherText="<Set `cipherText` as the `"CipherTextBlob"` from DECRYPT_ONLY.json.>"
+aws kms re-encrypt \
+    --source-key-id arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126 \
+    --destination-key-id arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126 \
+    --source-encryption-context "kms-arn=$kmsArn, branch-key-id=$branchKeyId, hierarchy-version=1, create-time=$createTime, tablename=$tableName, type=$type" \
+    --destination-encryption-context "kms-arn=$kmsArn, branch-key-id=$branchKeyId, hierarchy-version=1, create-time=$createTime, tablename=$tableName, type=$typeActive, version=$type" \
+    --ciphertext-blob "$cipherText"
+```
+
+#### KMS GenerateDataKeyWithoutPlaintext for Beacon Key
+
+Execute the following, and persist the result as BEACON.json.
+
+```sh
+type="beacon:ACTIVE"
+aws kms generate-data-key-without-plaintext \
+--key-id arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126 \
+--number-of-bytes 32 \
+--encryption-context "kms-arn=$kmsArn, branch-key-id=$branchKeyId, hierarchy-version=1, create-time=$createTime, tablename=$tableName, type=$type"
+```
+
+#### DynamoDB TransactWriteItems
+
+Create a `items.json` file formatted as follows:
+
+```json
+[
+    {
+        "Put": {
+            "TableName": "KeyStoreDdbTable",
+            "Item": {
+                "branch-key-id": {"S": "kms-arn-attribute-is-lying"},
+                "type": {"S": <value of "$type">},
+                "kms-arn": {"S": "arn:aws:kms:us-west-2:370957321024:key/bc127593-f7da-452c-a1f3-cd34c46f81f8"},
+                "hierarchy-version": {"N": "1"},
+                "create-time": {"S": <value of "$createTime"},
+                "enc": {"B":  <value of `"CipherTextBlob"` from DECRYPT_ONLY.json>}
+            },
+            "ConditionExpression" : "attribute_not_exists(#pk)",
+            "ExpressionAttributeNames" : {"#pk": "branch-key-id"}
+        }
+    },
+    {
+        "Put": {
+            "TableName": "KeyStoreDdbTable",
+            "Item": {
+                "branch-key-id": {"S": "kms-arn-attribute-is-lying"},
+                "type": {"S": "branch:ACTIVE"},
+                "kms-arn": {"S": "arn:aws:kms:us-west-2:370957321024:key/bc127593-f7da-452c-a1f3-cd34c46f81f8"},
+                "hierarchy-version": {"N": "1"},
+                "create-time": {"S": <value of "$createTime"},
+                "enc": {"B":  <value of `"CipherTextBlob"` from ACTIVE.json>},
+                "version": {"S": <value of "$type">}
+            },
+            "ConditionExpression" : "attribute_not_exists(#pk)",
+            "ExpressionAttributeNames" : {"#pk": "branch-key-id"}
+        }
+    },
+    {
+        "Put": {
+            "TableName": "KeyStoreDdbTable",
+            "Item": {
+                "branch-key-id": {"S": "kms-arn-attribute-is-lying"},
+                "type": {"S": "beacon:ACTIVE"},
+                "kms-arn": {"S": "arn:aws:kms:us-west-2:370957321024:key/bc127593-f7da-452c-a1f3-cd34c46f81f8"},
+                "hierarchy-version": {"N": "1"},
+                "create-time": {"S": <value of "$createTime"},
+                "enc": {"B":  <value of `"CipherTextBlob"` from BEACON.json>}
+            },
+            "ConditionExpression" : "attribute_not_exists(#pk)",
+            "ExpressionAttributeNames" : {"#pk": "branch-key-id"}
+        }
+    }
+]
+```
+
+Execute the TransactWriteItems request via:
+`aws dynamodb transact-write-items file://items.json`.