feat(dafny): Branch Key Store without modifying Encryption Context #1416

texastony · 2025-04-09T17:45:53Z

Issue #, if available:

Description of changes:

This is ONLY a breaking change to consumers of the mutation/mutation branch
that introduced the Branch Key Store Admin.

Squash/merge commit message, if applicable:

feat(dafny)!: Branch Key Store without modifying Encryption Context

BREAKING CHANGE: Branch Key Store Admin has the following breaking changes for eventual MRK support:
- The MRK option in `KmsSymmetricKeyArn` has been removed entirely; it never worked properly and never could work as the region was not supplied.

TODO Key Words

TODO-HV-2-M# :: related to a milestone
TODO-HV-2-BLOCKER :: blocker for internal launch
TODO-HV-2-FOLLOW :: post internal launch
TODO-HV-2-GA :: blocker for going to main

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

…re module (#1356)

BREAKING CHANGE: Branch Key Store Admin has the following breaking changes for MRK support: - `KmsSymmetricKeyArn` has dropped the MRK option entirely

… HV-2 (#1366) Co-authored-by: texastony <[email protected]>

Co-authored-by: Tony Knapp <[email protected]> By-passing after Verification checks were met.

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

Co-authored-by: Tony Knapp <[email protected]> Overriding CI check as only one .NET workflow failed due to a typical failure in .NET with SigV4 creds.

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

…1401) Skipping CI to ensure that all future PRs from us do not impact mainline.

Interopt testing does not cover this change

…1400) Co-authored-by: Tony Knapp <[email protected]> Co-authored-by: Rishav karanjit <[email protected]> Modified to account for MRK

Duvet references in the code base are from spec reference that has not been pushed to mutations/mutations. For now, we will disable duvet, and re-enable it once mutations has been updated.

Hitting DDB Race condition bug in .NET.

…tation (#1440)

…rarchy versions (#1453)

…rsion (#1449)

test(dafny): KATs for Branch Key Context Digest (#1451) Co-authored-by: Tony Knapp <[email protected]>

Co-authored-by: rishav-karanjit <[email protected]>

…ations(#1460) Co-authored-by: texastony <[email protected]>

…1465)

…rom hv-2 (#1475)

)

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

@josecorella

Bypassing strict approval requirements. PR was written by @josecorella, approved by @texastony, and then has 2 commits by @texastony; GitHub will not let @josecorella approve these last 2 commits, so we bypassing the rule.

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

…ey (#1487)

Co-authored-by: Darwin Chowdary <[email protected]>

…ion (#1507)

I am By passing a CI failure in Java . It is with Mutations, one of the three Java tests failed: ``` TestMutateHierarchyVersion.TestHV1toHV2HappyCaseDecryptEncrypt: FAILED dafny/AwsCryptographyKeyStoreAdmin/test/Mutations/TestMutationHappyPath.dfy(313,6): Actual customer send EC and expected customer send EC did not match. ``` We should look into this...

imabhichow and others added 27 commits April 8, 2025 18:02

chore: fix CI for HV-2 (#1353)

e17db6f

chore: move ProvideCryptoClient to HierarchicalVersionUtils in KeySto…

51c7198

…re module (#1356)

ci(Go, Rust): disable for current HV-2 work (#1360)

5e55f9c

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

faf9622

BREAKING CHANGE: Branch Key Store Admin has the following breaking changes for MRK support: - `KmsSymmetricKeyArn` has dropped the MRK option entirely

chore(BKS): pack & unpack plainTextTuple (#1362)

db67136

chore(BKS): Add Helper functions to select KMS Encryption Context for…

1328a4e

… HV-2 (#1366) Co-authored-by: texastony <[email protected]>

chore: refactor hv1 functions and methods (#1367)

c35f991

chore(bks): Add createMdDigest in hvutils (#1361)

de7ef56

chore(BKS): add decrypt hook For Hv2 (#1368)

9274827

chore(dafny): Add todo for test (#1377)

18e1075

chore(dafny): BranchKeyContext for HV-2 (#1381)

f378730

chore(dafny): KS Refactor KeyStoreException (#1383)

b8802b9

Co-authored-by: Tony Knapp <[email protected]> By-passing after Verification checks were met.

chore(dafny): BKS Encrypt Key for HV-1 & HV-2 (#1372)

95c62f8

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

chore(dafny): wire get keys with the decrypt hook (#1376)

ef37253

chore(dafny): BKS Refactor GetKeys (#1389)

8bd469d

chore(dafny): add test for get keys (#1388)

29f7b9f

Co-authored-by: Tony Knapp <[email protected]> Overriding CI check as only one .NET workflow failed due to a typical failure in .NET with SigV4 creds.

chore(dafny): add VerifyGetKeysFromStorage to test (#1392)

73bb512

chore(dafny): Add helper function to VerifyGetKeys (#1396)

c5f51ab

feat(dafny): KSA Create Key Operation for HV-2 (#1374)

545885f

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

test(dafny): no touching the static branch-key-id in the dev branch (#…

8ea5cbe

…1401) Skipping CI to ensure that all future PRs from us do not impact mainline.

test(dafny): restore static test branch key id (#1403)

83211d8

Interopt testing does not cover this change

chore(dafny): refactor HV1 MRK test to use helper methods (#1399)

63b6409

chore(dafny): KSA Add test coverage for creating a hv-2 branch key. (#…

f5f1de3

…1400) Co-authored-by: Tony Knapp <[email protected]> Co-authored-by: Rishav karanjit <[email protected]> Modified to account for MRK

chore: disable duvet (#1414)

6d1db95

Duvet references in the code base are from spec reference that has not been pushed to mutations/mutations. For now, we will disable duvet, and re-enable it once mutations has been updated.

chore(java): create key example for HV-2 branch key (#1425)

8d61b10

refactor(dafny): rename BKS Error Messages class for legibility (#1429)

be086cd

chore(dafny): Add helper method to decrypt branch key item (#1439)

999ae15

Hitting DDB Race condition bug in .NET.

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

rishav-karanjit and others added 2 commits April 14, 2025 16:37

chore(dafny): add checks and tests to fail on EC collision on init mu…

cad6d00

…tation (#1440)

fix(dafny): BKSA CreateKey formal verification (#1427)

43a87ba

josecorella and others added 29 commits April 17, 2025 14:24

chore(dafny): refactor VersionActiveBranchKey to support multiple hie…

354bca2

…rarchy versions (#1453)

fix(dafny): BKS Mutation Items treat hierarchy-version as schema ve…

8939be9

…rsion (#1449)

test(dafny): ensures lying branch keys throws exception (#1422)

500b96d

test(dafny): KATs for Branch Key Context Digest (#1451) Co-authored-by: Tony Knapp <[email protected]>

chore(dafny): BKSA Mutate from HV-1 to HV-2 only Simple (#1458)

ae81599

Co-authored-by: rishav-karanjit <[email protected]>

chore(dafny): BKSA test pre-HV-2 static branch keys for in-flight mut…

20cfd18

…ations(#1460) Co-authored-by: texastony <[email protected]>

chore(dafny): move static branch keys to static key store table (#1459)

49bb228

chore: refactor helper methods for copy & delete branch keys (#1462)

cd3cafd

chore(dafny): Test hv1 to hv2 mutation (#1461)

4867143

refactor(dafny): move TestMutateToHV2FromHV1 to mutation directory (#…

0379078

…1465)

chore(dafny): Add TODO to support terminal hv-1 but not downgrading f…

f7f093a

…rom hv-2 (#1475)

feat(dafny): support decrypt/encrypt strategy for mutation to hv2 (#1466

fd4bbc2

)

feat(dafny): mutate HV-2 to HV-2 without new version (#1474)

1ec8cda

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

chore(java): add examples for mutation to hv-2 (#1477)

63b1008

test(java): BKSA in-flight mutations access denied (#1480)

d3b94a4

feat(dafny): support hv-2 versionKey in KeyStoreAdmin (#1455)

e3eacb5

Bypassing strict approval requirements. PR was written by @josecorella, approved by @texastony, and then has 2 commits by @texastony; GitHub will not let @josecorella approve these last 2 commits, so we bypassing the rule.

chore(dafny): add version on mutate functionality (#1485)

3b74ecf

chore(dafny): fix verification in kms keyring ondecrypt (#1489)

92b6258

chore(dafny): BKSA Mutations Tests for HV-1 to HV-1 (#1482)

bd5c1b8

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

chore(dafny): Complete Strategy Support for BKSA VersionKey & CreateK…

42612ab

…ey (#1487)

chore(dafny): add hv-2 create key proofs (#1499)

e8e869f

chore(dafny): support kms simple for v1 to v1 mutations (#1491)

0fe76f7

chore(dafny): add version key hv-2 proofs (#1504)

ac1d634

chore(dafny): BKS CreateKey remove redundant EC checks for HV-2 (#1508)

66ae3df

Co-authored-by: Darwin Chowdary <[email protected]>

chore(dafny): BKSA refine KMS Error mapping to MutationTo/From except…

4f6887f

…ion (#1507)

chore(dafny): BKSA Tests for Restarting Mutations (#1501)

8f822b4

chore(dafny): cleanup todos in hv-2 (#1511)

70bf132

chore(dafny): add failure for unexpected attribute in EC on HV-2 (#1516)

61406ea

chore(dafny): remove duplicate proof in kms keyring (#1526)

268ffd7

texastony mentioned this pull request May 21, 2025

feat(dafny): Branch Key Store without modifying Encryption Context #1535

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(dafny): Branch Key Store without modifying Encryption Context #1416

feat(dafny): Branch Key Store without modifying Encryption Context #1416

texastony commented Apr 9, 2025 •

edited

Loading

feat(dafny): Branch Key Store without modifying Encryption Context #1416

Are you sure you want to change the base?

feat(dafny): Branch Key Store without modifying Encryption Context #1416

Conversation

texastony commented Apr 9, 2025 • edited Loading

Issue #, if available:

Description of changes:

Squash/merge commit message, if applicable:

TODO Key Words

texastony commented Apr 9, 2025 •

edited

Loading