feat(BKS): Get* HV-2 Branch Keys #1342

texastony · 2025-03-19T16:24:28Z

Issue #, if available:

Description of changes:

Squash/merge commit message, if applicable:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

The key store now allows for both a default DynamoDB table, or any custom storage system. The important aspect about the key store is the fact that branch keys can be versioned easily, and are cryptographically safe to use. The actual storage medium is not important. See: https://github.com/awslabs/aws-encryption-sdk-specification/blob/master/changes/2024-6-17_key-store-persistance/background.md#background

@seebees

Explicitly: - Change InitializeMutationFlag from a union to an enum for ToString reasons - Model `DoNotVersion` flag for Initialize Mutation - Refactor Describe Mutation output to detail Input so resume can be done - Refactor System Key to be optional, detailing that TrustStorage is the default - More errors - Smithy changes from PR feedback on #854 - Correction of spelling mistakes - Mutation Token's UUID is required Why change the flag to an enum? Dafny/Smithy-Dafny's support for Union's results in structures that do not print well. The intention of the `InitializeMutationFlag` is to inform customers about the result of their request. Such information may, possibly even should, be logged. Initialize Mutation and Apply Mutation MUST ensure that the UUID of the Index and Commitment agree. Apply MUST ensure that the UUID of the Commitment and Token agree. The Mutation Token's UUID is REQUIRED. It is how we track a mutation, much like how CFN tracks a change set. Fixed bug where UUID is a reserved word in DDB. Refactored some of the error messages. Utilize Java Example to demonstrate resume and restart. Finally, addressed some of the feedback on PR #854. feat(Mutations): Idempotent Resume (#854) Refactor Storage: - Rename Mutation Lock to Mutation Commitment - Introduce Mutation Index to describe what items of a Branch Key have been mutated - Add Input field to Mutation Commitment - Add Ciphertext field to Mutation Commitment - When Mutating an item, always write with an optimistic lock - Allow Initialize Mutation to over write a Version, instead of only creating a version - When Overwriting a Mutation Index, ensure it has not changed - Whenever writing for Mutation, ensure the Mutation Commitment's ENC is as expected (along with original and terminal) Refactor Storage to contain operations that: 1. Allow for Atomic Mutations (maybe cut later) 2. Allow for Deleting a Mutation 3. Allow for Creating a Mutation Index Refactor KeyStoreAdmin: - Support a System Key for Mutations - Stub out the System Key - Logic for handling Mutation Index Refactor Initialize Mutation: - If Commitment & Index already exist and match Input, write nothing and return token - If Commitment already exists and matches input, write index, and return token - If Commitment already exists and does not match input, fail - If no commitment, Initialize Mutation Refactor Apply Mutation: - Write an update Page Index. fix: Dafny intendation formatting chore: fix Java test examples chore: more fomratting for CI feat(Mutations): Native test for Loose access in-flight feat(Mutations): Example In Flight Mutation Scanner feat(Mutations-TODO): Some Terminal KMS Exceptions (#795) If the KMS Call, for mutating the Beacon, fails, it MAY indicate the MPL Consumer does not have access to the terminal KMS Key. If the KMS call for verifying a terminal version fails, it MAY indicate the MPL Consumer does not have access to the terminal KMS Key. Also fix some Dafny tests failing verification. feat(KS+): More modeled errors (#754) * refactor(Storage): Use TransactGet instead of BatchGet for GetInitMut (#753) This resolves feedback from both @seebees and @josecorella on Mutations branch. * chore(Mutations): address #754\#discussion_r1775676091 #754 (comment) * chore(Mutations): Address feedback from #750 See #750 * chore(Mutations): address feedback on #742 See #742 refactor(Storage): Use TransactGet instead of BatchGet for GetInitMut (#753) This resolves feedback from both @seebees and @josecorella on Mutations branch. Verification failure is due to (just like in #751 ): 1. Key Store Admin's Index.dfy not proving Fresh, which has been a long standing issue with the Admin 2. In `AwsCryptographyKeyStore/test/Storage/TestGetItemsForInitializeMutation.dfy`, the test assumes `type` is in the Encryption Context. It is, but Structure.dfy does not prove that, so it must be proven else where. A .NET MPL job failed due to .NET 48 Sig V4 Auth bug. test(Mutations): additional testing for Mutations feat(Mutations): more clean up feat(Mutations): log statements for ApplyMutation fix(Storage): typo fix(Storage): ensure KmsArn is valid chore(Mutations): respond to comments on PR #720 test(GHW): Run Java Examples for PR CI (#749) chore(Java): Examples for Mutations (#742) chore(Mutations): comment out non-GA Mutations (#750) Crypto Tools, at this time, intends to release Branch Key Mutations without some operations useful for recovering a dropped Mutation Token or dealing with the disagreement of a Mutation Token and a Mutation Lock. Additionally, we intend to release the Key Store Admin with only support for one Key Management Strategy. All checks are green except for Verification. Verification is failing for the Key Store Admin's Index.dfy. Verification for the Key Store Admin's Index.dfy has been failing for a long time. feat: Mutations BETA (#720) Beta build of Mutations with several substantial gaps

There are still more refactoring we could do in MutationsErrorRefinement, but this should be sufficient for now.

Co-authored-by: Jose Corella <[email protected]>

Co-authored-by: José Corella <[email protected]>

* fix(KSA): Describe Mutation bugs * fix(Java): Always clean up test resources

Fixes: - Wrong assertion for Java Example Test of In-Flight Mutation scanner - Initialize Mutation, when using Decrypt/Encrypt, must use Decrypt/Encrypt to mutate the Beacon Tests: - Explicitly Test Decrypt/Encrypt with different credentials that only can use the relevant KMS Keys - Refactor Examples to be easier to test across inputs Other: - Add Documentation to the Java Examples Co-authored-by: José Corella <[email protected]>

#1081) * test(KSA-Java): explicitly check for deletion of Index and Commitment at end of Mutation * chore: polish examples

This ensures that our implementation is correct, as if it was not, the incorrect KMS Client would be used, and the request would fail.

- Polish Documentation for Mutations and the Key Store Admin - Make the System Key parameter required for Initialize and Apply - Improve Java Example Tests to assert that all items of a Branch Key are use-able post Mutation and require the correct KMS Key.

Co-authored-by: Andy Jewell <[email protected]>

Co-authored-by: Tony Knapp <[email protected]>

…#1235) This addresses KMS Exceptions when the KMS Key is disabled OR when the caller does not have permission to call GenerateDataKeyWithoutPlaintext on the terminal KMS Key.

…e/src/ErrorMessages.dfy Co-authored-by: Tony Knapp <[email protected]>

texastony

Looks good; few nits and a couple of blocks.

texastony · 2025-03-21T22:50:53Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy

+        EncryptionContext := hv2EC,
+        CiphertextBlob := branchKeyItemFromStorage.CiphertextBlob
+      );
+      var branchKey: KMS.DecryptResponse :- KMSKeystoreOperations.DecryptKeyForHV2(


This is most definitely not a branchKey ;)

Suggested change

var branchKey: KMS.DecryptResponse :- KMSKeystoreOperations.DecryptKeyForHV2(

var kmsDecryptRes: KMS.DecryptResponse :- KMSKeystoreOperations.DecryptKeyForHV2(

https://github.com/aws/aws-cryptographic-material-providers-library/pull/1354/files#r2011028197

texastony · 2025-03-21T22:51:15Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy

+            "Failed to create SHA of MD Digest.");
+        return Failure(e);
+      }
+      var plaintextBranchKeyWithMdDigest := branchKey.Plaintext.value;


Suggested change

var plaintextBranchKeyWithMdDigest := branchKey.Plaintext.value;

var plaintextBranchKeyWithMdDigest := kmsDecryptRes.Plaintext.value;

texastony · 2025-03-21T22:58:22Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/ErrorMessages.dfy

+    "This Branch Key item has failed the authentication check. Either it has been tampered with or the wrong 'Logical Key Store Name' has been provided."
+
+  const KMS_DECRYPT_INVALID_KEY_LENGTH_HV2 :=
+    "Invalid response from AWS KMS Decrypt: Key is not of 80 bytes. This could mean Branch Key Item in the Storage has been tampered."


Suggested change

"Invalid response from AWS KMS Decrypt: Key is not of 80 bytes. This could mean Branch Key Item in the Storage has been tampered."

"Invalid response from AWS KMS Decrypt: Plaintext is not 80 bytes. This could mean the persisted branch key Item has been tampered."

https://github.com/aws/aws-cryptographic-material-providers-library/pull/1354/files#r2011028677

texastony · 2025-03-21T22:59:05Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/ErrorMessages.dfy

+    "Invalid response from AWS KMS Decrypt: Key is not of 80 bytes. This could mean Branch Key Item in the Storage has been tampered."
+
+  const INVALID_BRANCH_KEY_CONTEXT := 
+    "The branch key item is missing a required attribute. The branch key item might have been tampered to remove some attribute(s)."


Suggested change

"The branch key item is missing a required attribute. The branch key item might have been tampered to remove some attribute(s)."

"The branch key item is missing a required attribute. The branch key item might have been tampered with."

https://github.com/aws/aws-cryptographic-material-providers-library/pull/1354/files#r2011029177

texastony · 2025-03-21T22:59:24Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/ErrorMessages.dfy

+    "Invalid hierarchy version. Expected version 1 or 2."
+
+  const MD_DIGEST_SHA_NOT_MATCHED :=
+    "This Branch Key item has failed the authentication check. Either it has been tampered with or the wrong 'Logical Key Store Name' has been provided."


Suggested change

"This Branch Key item has failed the authentication check. Either it has been tampered with or the wrong 'Logical Key Store Name' has been provided."

"This branch key item has failed the authentication check. Either it has been tampered with or the wrong 'Logical Key Store Name' has been provided."

texastony · 2025-03-21T23:06:56Z

...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/HierarchicalVersionUtils.dfy

+      :: k := item[k]
+  }
+
+  method GetHV2EC(


I get it, but for today, let's distinguish b/w the various ECs.
KMS EC :: What KMS sees.

Suggested change

method GetHV2EC(

method GetHv2KmsEc(

texastony · 2025-03-21T23:08:44Z

...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/HierarchicalVersionUtils.dfy

+    {
+        var item :| item in items;
+        items := items - { item };
+        if (|item.0| >= |Structure.ENCRYPTION_CONTEXT_PREFIX| && item.0[..|Structure.ENCRYPTION_CONTEXT_PREFIX|] == Structure.ENCRYPTION_CONTEXT_PREFIX) {
+          var newKey := item.0[|Structure.ENCRYPTION_CONTEXT_PREFIX|..];
+          newMap := newMap[newKey := item.1];
+        } else {
+          newMap := newMap[item.0 := item.1];
+        }
+    }


For M1, this OK... but we probably will need to refactor to a more efficient solution.
Dafny maps are not mutable... so these are new allocations (I think).
i.e: each iteration is a new allocation of the map.

There is a action we can use.

Added a TODO for this method. I think I might need to change this method into a function so that i can use it in pre and post condition for verification.

texastony · 2025-03-21T23:10:29Z

...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/HierarchicalVersionUtils.dfy

+  function method RemoveRestrictedFields(a:map<string, string>) : (output:map<string, string>)
+    ensures Structure.Hv2EncryptionContext?(output)
+  {
+    a - Structure.BRANCH_KEY_RESTRICTED_FIELD_NAMES
+  }


Nit: I hate bad variable names. I get it, input vs a really does not matter.
But some part of me just does not have the flexibility to accept this.

Suggested change

function method RemoveRestrictedFields(a:map<string, string>) : (output:map<string, string>)

ensures Structure.Hv2EncryptionContext?(output)

{

a - Structure.BRANCH_KEY_RESTRICTED_FIELD_NAMES

}

function method RemoveRestrictedFields(input:map<string, string>) : (output:map<string, string>)

ensures Structure.Hv2EncryptionContext?(output)

{

input - Structure.BRANCH_KEY_RESTRICTED_FIELD_NAMES

}

texastony · 2025-03-21T23:11:25Z

...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/HierarchicalVersionUtils.dfy

+        assert forall r | r in parseResults.Values :: r.Success?;
+        var utf8KeysUnique := forall k, k' | k in parseResults && k' in parseResults
+                                :: k != k' ==> parseResults[k].value.0 != parseResults[k'].value.0;
+        if !utf8KeysUnique then Failure(Types.KeyStoreException(
+                                        message := "Encryption context keys are not unique"))  // this should never happen...
+        else Success(map r | r in parseResults.Values :: r.value.0 := r.value.1)


I think I have a helper method in BKSA for proving this.

texastony · 2025-03-21T23:14:09Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy

+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#aws-kms-branch-key-decryption
+    //= type=implication
+    //# - `EncryptionContext` MUST be the [encryption context](#encryption-context) of the provided EncryptedHierarchicalKey
+    && decryptRequest.EncryptionContext == Some(versionItem.EncryptionContext)


Blocking: I suspect this is wrong.
Unless you know versionItem.EncryptionContext is the un-prefixed user supplied EC.

Added a TODO for this predicate. Will get into it later

imabhichow · 2025-03-22T00:51:28Z

...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/HierarchicalVersionUtils.dfy

+        var item :| item in items;
+        items := items - { item };
+        if (|item.0| >= |Structure.ENCRYPTION_CONTEXT_PREFIX| && item.0[..|Structure.ENCRYPTION_CONTEXT_PREFIX|] == Structure.ENCRYPTION_CONTEXT_PREFIX) {
+          var newKey := item.0[|Structure.ENCRYPTION_CONTEXT_PREFIX|..];
+          newMap := newMap[newKey := item.1];
+        } else {
+          newMap := newMap[item.0 := item.1];


It looks like this method doesn't actually remove ENCRYPTION_CONTEXT_PREFIX. I think we should write some tests around EC.

Yes it does not remove ENCRYPTION_CONTEXT_PREFIX if it is not in the EC (else block) but if ENCRYPTION_CONTEXT_PREFIX is there it will remove it (if block)

But, there is definitely a bug in GetHV2EC because it is returning withoutRestrictedField instead of newMap

imabhichow · 2025-03-22T01:13:22Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy

+    } else if (branchKeyItemFromStorage.EncryptionContext[Structure.HIERARCHY_VERSION] == Structure.HIERARCHY_VERSION_2) {
+      // branchKeyItemFromStorage.EncryptionContext comes from storage is not the actual EC. 
+      // branchKeyItemFromStorage.EncryptionContext contains all the items in the dynamodb table and table name.
+      var hv2EC := HierarchicalVersionUtils.GetHV2EC(branchKeyItemFromStorage.EncryptionContext);


I think we can use either before calling KMS.Decrypt or Here.

Suggested change

var hv2EC := HierarchicalVersionUtils.GetHV2EC(branchKeyItemFromStorage.EncryptionContext);

var hv2EC := Structure.ExtractCustomEncryptionContextAs(branchKeyItemFromStorage.EncryptionContext);

The reason ExtractCustomEncryptionContextAs won't work is it filters EC that are greater than ENCRYPTION_CONTEXT_PREFIX (here). So, if EC is ["Robbie":"is a dog"] then it removes this key-value which is not expected. In Get operation we only remove ENCRYPTION_CONTEXT_PREFIX if its there because there could be a customer who might be extending MPL having their own create operation. So, to untransform the EC in get operation, we remove the restricted fields and then remove the prefix only if its there.

texastony and others added 30 commits January 22, 2025 10:43

chore(Java): version by properties file only

11687e8

fix(Mutations): KMS Exception improvements

c4af12f

There are still more refactoring we could do in MutationsErrorRefinement, but this should be sufficient for now.

feat(KSA): Describe Mutation

f8e91e7

feat(KSA): KMS Decrypt/Encrypt Strategy (#1020)

8795bf5

Co-authored-by: Jose Corella <[email protected]>

feat(KSA): System Key (#1021) (#1055)

0f0ede0

Co-authored-by: José Corella <[email protected]>

chore: percolate changes from HEAD to mutations branch

c44f328

fix(KS-Smithy): explicit error for tampered Branch Key (#1058)

5896cf8

chore: fix decrypt encrypt strategy (#1059)

621116e

fix(KSA): Describe Mutation bugs (#1062)

34683eb

* fix(KSA): Describe Mutation bugs * fix(Java): Always clean up test resources

chore: error refinement improvements decrypt/encrypt strategy (#1061)

9d66289

fix: use correct client depending on operation (#1084)

5b2f851

test(KSA-Java): assert deletion of Index/Commitment at end of Mutation (

6714c65

#1081) * test(KSA-Java): explicitly check for deletion of Index and Commitment at end of Mutation * chore: polish examples

docs: update documentation for Key Store Admin Errors (#1086)

42149ec

test(KSA): Utilize Limit KMS Clients in Mutation D/E test (#1089)

b26fbb3

This ensures that our implementation is correct, as if it was not, the incorrect KMS Client would be used, and the request would fail.

feat(KSA): DoNotVersion for Initialize Mutation (#1082)

a914309

fix(MPL): remove un-used imports (#1103)

3f9f7d7

chore(Rust): fix Rust import of the KSA (#1110)

180a7d8

Co-authored-by: Andy Jewell <[email protected]>

docs(KSA): clarify mutation behvior (#1112)

528d8f0

chore(Smithy): remove Smithy trait un-supported by Smithy-Dafny (#1134)

90a390e

test: add concurrency testing for storage operations (#1132)

2fc52ac

Co-authored-by: Tony Knapp <[email protected]>

fix(KeyStoreAdmin): Go support (#1242)

af0078d

fix(GHW): Library Example (#1269)

eb56365

fix(KeyStoreAdmin): Exceptions for Mutations when KMS Key is Disabled (…

0c5cfa7

…#1235) This addresses KMS Exceptions when the KMS Key is disabled OR when the caller does not have permission to call GenerateDataKeyWithoutPlaintext on the terminal KMS Key.

Add GetEncryptionContextHV1 and GetEncryptionContextHV2

53abc2c

Add INVALID_HIERARCHY_VERSION error message

64f45de

Add need for H version check

c769619

rishav-karanjit temporarily deployed to Duvet CI March 20, 2025 17:47 — with GitHub Actions Inactive

rishav-karanjit added 2 commits March 20, 2025 14:00

Add DecryptKeyForHV2

d0c1f23

use DecryptKeyForHV2

84a5829

rishav-karanjit temporarily deployed to Duvet CI March 20, 2025 21:13 — with GitHub Actions Inactive

rishav-karanjit added 2 commits March 20, 2025 14:18

Add Hv2EncryptionContext?

8c53237

fix path to predicates

9348860

rishav-karanjit temporarily deployed to Duvet CI March 20, 2025 21:19 — with GitHub Actions Inactive

Update AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStor…

45efb9c

…e/src/ErrorMessages.dfy Co-authored-by: Tony Knapp <[email protected]>

rishav-karanjit temporarily deployed to Duvet CI March 20, 2025 21:37 — with GitHub Actions Inactive

Add KMS_DECRYPT_INVALID_KEY_LENGTH_HV2

da2be20

rishav-karanjit temporarily deployed to Duvet CI March 20, 2025 21:44 — with GitHub Actions Inactive

Add INVALID_BRANCH_KEY_CONTEXT

af9c4a5

rishav-karanjit temporarily deployed to Duvet CI March 20, 2025 22:33 — with GitHub Actions Inactive

rishav-karanjit added 2 commits March 21, 2025 09:28

refactoring for verification

bbfab39

Add AwsKmsBranchKeyHV2Decryption?

6cd7f44

rishav-karanjit temporarily deployed to Duvet CI March 21, 2025 16:29 — with GitHub Actions Inactive

Add ValidateMdDigest

159aaa9

rishav-karanjit temporarily deployed to Duvet CI March 21, 2025 23:08 — with GitHub Actions Inactive

texastony commented Mar 21, 2025

View reviewed changes

beacon and branch key version

67de9db

rishav-karanjit temporarily deployed to Duvet CI March 21, 2025 23:18 — with GitHub Actions Inactive

fix

32df5db

rishav-karanjit temporarily deployed to Duvet CI March 21, 2025 23:21 — with GitHub Actions Inactive

imabhichow reviewed Mar 22, 2025

View reviewed changes

This was referenced Mar 23, 2025

feat(BKS & BKSA): Smithy Model for HV-2 #1350

Merged

(WIP)feat(HV-2): CreateKey #1349

Closed

rishav-karanjit mentioned this pull request Mar 24, 2025

chore: consolidate Get* and Create* changes #1354

Closed

texastony force-pushed the hv-2/hv-2 branch 2 times, most recently from 2e99106 to 999ae15 Compare April 14, 2025 23:24

	var branchKey: KMS.DecryptResponse :- KMSKeystoreOperations.DecryptKeyForHV2(
	var kmsDecryptRes: KMS.DecryptResponse :- KMSKeystoreOperations.DecryptKeyForHV2(

	var plaintextBranchKeyWithMdDigest := branchKey.Plaintext.value;
	var plaintextBranchKeyWithMdDigest := kmsDecryptRes.Plaintext.value;

	"Invalid response from AWS KMS Decrypt: Key is not of 80 bytes. This could mean Branch Key Item in the Storage has been tampered."
	"Invalid response from AWS KMS Decrypt: Plaintext is not 80 bytes. This could mean the persisted branch key Item has been tampered."

	"The branch key item is missing a required attribute. The branch key item might have been tampered to remove some attribute(s)."
	"The branch key item is missing a required attribute. The branch key item might have been tampered with."

	"This Branch Key item has failed the authentication check. Either it has been tampered with or the wrong 'Logical Key Store Name' has been provided."
	"This branch key item has failed the authentication check. Either it has been tampered with or the wrong 'Logical Key Store Name' has been provided."

	var hv2EC := HierarchicalVersionUtils.GetHV2EC(branchKeyItemFromStorage.EncryptionContext);
	var hv2EC := Structure.ExtractCustomEncryptionContextAs(branchKeyItemFromStorage.EncryptionContext);

feat(BKS): Get* HV-2 Branch Keys #1342

Are you sure you want to change the base?

feat(BKS): Get* HV-2 Branch Keys #1342

Uh oh!

Conversation

texastony commented Mar 19, 2025

Uh oh!

texastony left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!