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

imabhichow · 2025-03-21T23:18:21Z

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.

This reverts commit 35333e1.

…orHV1?" This reverts commit 1aa9758.

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

…ow/hv-2-smithy-changes # Conflicts: # AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy # AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/HierarchicalVersionUtils.dfy

texastony

I think this is great progress;
we need to get some consolidation going on Monday between the various PRs to make our mile-stone.

It is too hard for me to review 48 commits of code at once;
the three of us need to work together to collapse our efforts/changes.

texastony · 2025-03-24T04:14:43Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/ErrorMessages.dfy

@@ -57,6 +57,9 @@ module {:options "/functionSyntax:4" } KeyStoreErrorMessages {
  const INVALID_HIERARCHY_VERSION :=
    "Invalid hierarchy version. Expected version 1 or 2."

+  const BRANCH_KEY_MD_DIGEST_SHA_INCORRECT_LENGTH :=
+    "Branch key + md digest sha is of incorrect length."


Blocking: No customer will know what this means.
Look at this comment on made on Rishav's PR:
#1342 (comment)

#1354 (comment)

texastony · 2025-03-24T04:18:16Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy

      }
      var branchKeyMaterials :- Structure.ToBranchKeyMaterials(
        branchKeyItemFromStorage,
-        plaintextBranchKey
+        branchKey.Plaintext.value[Structure.MD_DIGEST_LENGTH..]


Blocking: We need to validate the PDK is the right length before returning it.
Break the PDK out before calling Structure.ToBranchKeyMaterials.
I get that other logic in the current code path
ensures that the PDK is the right length today;
but it is fragile to assume that will always be the case.

We need to validate the PDK is the right length before returning it.

This is done inside ValidateMdDigest because we also need valid length to validate MD Digest

Break the PDK out before calling Structure.ToBranchKeyMaterials.

Added a TODO

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

texastony · 2025-03-24T04:20:37Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy

+      // 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);
+      var hv2BranchKey := Types.EncryptedHierarchicalKey(
+        Identifier := branchKeyItemFromStorage.Identifier,
+        Type := branchKeyItemFromStorage.Type,
+        CreateTime := branchKeyItemFromStorage.CreateTime,
+        KmsArn := branchKeyItemFromStorage.KmsArn,
+        EncryptionContext := hv2EC,
+        CiphertextBlob := branchKeyItemFromStorage.CiphertextBlob
+      );
+      var branchKey: KMS.DecryptResponse :- KMSKeystoreOperations.DecryptKeyForHV2(
+        hv2BranchKey,
+        kmsConfiguration,
+        grantTokens,
+        kmsClient
+      );
+      var validateResult := HierarchicalVersionUtils.ValidateMdDigest(branchKey.Plaintext.value, branchKeyItemFromStorage);
+      if (validateResult.Failure?) {
+        return Failure(validateResult.error);
+      }
+      var branchKeyMaterials :- Structure.ToBranchKeyMaterials(
+        branchKeyItemFromStorage,
+        branchKey.Plaintext.value[0..Structure.AES_256_LENGTH]
+      );
+      return Success(
+          Types.GetBranchKeyVersionOutput(
+            branchKeyMaterials := branchKeyMaterials
+          ));


Blocking: This looks a lot like copy-and-paste/code duplication...
Can we make a helper method in HierarchicalVersionUtils that can be used to consolidate this?

#1354 (comment)

texastony · 2025-03-24T04:22:24Z

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

+    branchKeyItemFromStorage: Types.EncryptedHierarchicalKey
+  )
+    returns (output: Result<(), Types.Error>)
+    // The plaintext should be large enough to contain both AES key and MD digest


Suggested change

// The plaintext should be large enough to contain both AES key and MD digest

// The plaintext-tuple MUST be large enough to contain both AES key and MD digest

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

texastony · 2025-03-24T04:25:39Z

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

@@ -111,4 +126,59 @@ module HierarchicalVersionUtils {
    assume {:axiom} fresh(Crypto) && fresh(Crypto.Modifies);
    return Success(Crypto);
  }
+
+  method ValidateMdDigest (
+    plainText: KMS.PlaintextType,


Suggestion: There are so many plain-texts in our lives;
plain-text messages/content,
plain-text data keys,
plain-text wrapping keys...
let's give this variable a little distinctiveness by calling it plainTextTuple;
we know it is the concatenation of the PDK + protected-MD-Digest;
we could call that concatenation a tuple for short (
it sort of is, sort of isn't, but I think tuple is good enough and better than plainText).

Suggested change

plainText: KMS.PlaintextType,

plainTextTuple: KMS.PlaintextType,

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

texastony · 2025-03-24T04:27:49Z

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

@@ -111,4 +126,59 @@ module HierarchicalVersionUtils {
    assume {:axiom} fresh(Crypto) && fresh(Crypto.Modifies);
    return Success(Crypto);
  }
+
+  method ValidateMdDigest (


OK. I think see where you are going;
you are going to replace the duplicated code in GetKeys with this method,
yes?

texastony · 2025-03-24T04:31:25Z

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy

@@ -718,8 +723,82 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {

  }

+  ghost predicate AwsKmsBranchKeyHV2Decryption?(
+    versionItem: Types.EncryptedHierarchicalKey,


Blocking/Question: I think just call this a branchKeyItem;
I do not see any reason to restrict it to just version types, as compared to branch:ACTIVE or beacon:ACTIVE.

Need predicate needs more update. A verification is also failing. So, I just added TODO for now.

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

rishav-karanjit and others added 30 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

hv2 getkey rought sketch

bcd0a8c

Some clean ups

108284c

formatting

02c3898

Add HierarchicalVersionUtils utils

e1db473

refactoring

304c832

revert storage helper

11e266a

fix GetMdDigestFromEC

dfac4ae

MD_DIGEST_LENGTH and AES_256_LENGTH

c8052ba

chores in get key

d80676a

rename to DecryptKeyForHV1

7dbeabb

rename predicate AttemptKmsOperation? to AttemptKmsOperationForHV1?

1aa9758

rename AttemptKmsOperation? to AttemptKmsOperationForHV1?

35333e1

Revert "rename AttemptKmsOperation? to AttemptKmsOperationForHV1?"

045a853

This reverts commit 35333e1.

Revert "rename predicate AttemptKmsOperation? to AttemptKmsOperationF…

aa6e810

…orHV1?" This reverts commit 1aa9758.

Add DecryptKeyForHV2

d0c1f23

use DecryptKeyForHV2

84a5829

Add Hv2EncryptionContext?

8c53237

fix path to predicates

9348860

Update AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStor…

45efb9c

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

Add KMS_DECRYPT_INVALID_KEY_LENGTH_HV2

da2be20

Add INVALID_BRANCH_KEY_CONTEXT

af9c4a5

feat: Smithy Model for HV-2

af4bdeb

texastony and others added 18 commits March 21, 2025 00:14

chore: revise HV-2 Smithy for PR Feedback

0492ac6

fix: enum names must start with a letter

02215b3

fix: typo = -> :

92500b7

chore(BKS): polymorph

7b6307a

fix: WIP but some dafny resolve and verify issues

52a0316

WIP: create key

7a66a6c

remove table name from EC

b64c9f8

refactoring for verification

bbfab39

Add AwsKmsBranchKeyHV2Decryption?

6cd7f44

WIP: Encrypt

ce4782c

WIP: Encrypt

8beafe4

Add ValidateMdDigest

159aaa9

WIP

020fd10

beacon and branch key version

67de9db

fix

32df5db

feat: Create Key and Write a HappyCase Test to verify

0654db4

format

13984d6

texastony mentioned this pull request Mar 23, 2025

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

Merged

texastony requested changes Mar 24, 2025

View reviewed changes

rishav-karanjit mentioned this pull request Mar 24, 2025

chore: consolidate Get* and Create* changes #1354

Closed

texastony deleted the branch hv-2/smithy-model March 26, 2025 02:49

texastony closed this Mar 26, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

imabhichow commented Mar 21, 2025

texastony left a comment

texastony Mar 24, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 24, 2025

rishav-karanjit Mar 24, 2025 •

edited

Loading

rishav-karanjit Mar 24, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 24, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 24, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 24, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 24, 2025

rishav-karanjit Mar 24, 2025

texastony Mar 24, 2025

rishav-karanjit Mar 24, 2025

	// The plaintext should be large enough to contain both AES key and MD digest
	// The plaintext-tuple MUST be large enough to contain both AES key and MD digest

	plainText: KMS.PlaintextType,
	plainTextTuple: KMS.PlaintextType,

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

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

Conversation

imabhichow commented Mar 21, 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

rishav-karanjit Mar 24, 2025 • edited Loading

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

rishav-karanjit Mar 24, 2025 •

edited

Loading