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.

This reverts commit 53abc2c.

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/ErrorMessages.dfy

This reverts commit 35333e1.

…orHV1?" This reverts commit 1aa9758.

…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.

rishav-karanjit added 8 commits March 18, 2025 09:58

Add GetEncryptionContextHV1 and GetEncryptionContextHV2

53abc2c

Add INVALID_HIERARCHY_VERSION error message

64f45de

Add need for H version check

c769619

Revert "Add GetEncryptionContextHV1 and GetEncryptionContextHV2"

5d59de7

This reverts commit 53abc2c.

hv2 changes

d29744f

add constant for HIERARCHY_VERSION number

0f05c52

ToHV2EC method

44cfb48

rough sha impl

ef18557

texastony temporarily deployed to Duvet CI March 19, 2025 16:24 — with GitHub Actions Inactive

rishav-karanjit added 2 commits March 19, 2025 10:27

hv2 getkey rought sketch

bcd0a8c

Some clean ups

108284c

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

rishav-karanjit added 2 commits March 19, 2025 11:22

formatting

02c3898

Add HierarchicalVersionUtils utils

e1db473

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

refactoring

304c832

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

revert storage helper

11e266a

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

fix GetMdDigestFromEC

dfac4ae

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

texastony commented Mar 20, 2025

View reviewed changes

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/ErrorMessages.dfy Outdated Show resolved Hide resolved

MD_DIGEST_LENGTH and AES_256_LENGTH

c8052ba

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

rishav-karanjit added 2 commits March 20, 2025 10:13

chores in get key

d80676a

rename to DecryptKeyForHV1

7dbeabb

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

rename predicate AttemptKmsOperation? to AttemptKmsOperationForHV1?

1aa9758

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

rename AttemptKmsOperation? to AttemptKmsOperationForHV1?

35333e1

rishav-karanjit added 2 commits March 20, 2025 10:45

Revert "rename AttemptKmsOperation? to AttemptKmsOperationForHV1?"

045a853

This reverts commit 35333e1.

Revert "rename predicate AttemptKmsOperation? to AttemptKmsOperationF…

aa6e810

…orHV1?" This reverts commit 1aa9758.

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

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

texastony commented Mar 19, 2025

texastony left a comment

texastony Mar 21, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 21, 2025

texastony Mar 21, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 21, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 21, 2025

texastony Mar 21, 2025

texastony Mar 21, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 21, 2025

texastony Mar 21, 2025

texastony Mar 21, 2025

rishav-karanjit Mar 24, 2025

imabhichow Mar 22, 2025

rishav-karanjit Mar 24, 2025

rishav-karanjit Mar 24, 2025

imabhichow Mar 22, 2025

rishav-karanjit Mar 24, 2025

	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

Conversation

texastony commented Mar 19, 2025

texastony left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment