Skip to content

Commit 394afc0

Browse files
seebeestexastony
authored andcommitted
feat: Adding a storage option to the KeyStore (#594)
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
1 parent 75d60fa commit 394afc0

File tree

82 files changed

+11112
-1660
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

82 files changed

+11112
-1660
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
diff --git b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
2+
index 25bd45838..3ddedde75 100644
3+
--- b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
4+
+++ a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
5+
@@ -611,7 +611,7 @@ abstract module AbstractAwsCryptographyKeyStoreService
6+
import opened Types = AwsCryptographyKeyStoreTypes
7+
import Operations : AbstractAwsCryptographyKeyStoreOperations
8+
function method DefaultKeyStoreConfig(): KeyStoreConfig
9+
- method KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
10+
+ method {:isoluate_asserations} {:resource_limit 94000000 } KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
11+
returns (res: Result<KeyStoreClient, Error>)
12+
requires config.ddbClient.Some? ==>
13+
config.ddbClient.value.ValidState()

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsHierarchicalKeyring/TestAwsKmsHierarchicalKeyring.dfy

+84-28
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ module TestAwsKmsHierarchicalKeyring {
6969
return encryptionMaterialsIn;
7070
}
7171

72-
method {:test} TestHierarchyClientESDKSuite()
72+
method {:test} {:vcs_split_on_every_assert} TestHierarchyClientESDKSuite()
7373
{
7474
var branchKeyId := BRANCH_KEY_ID;
7575
// TTL = 166.67 hours
@@ -84,10 +84,17 @@ module TestAwsKmsHierarchicalKeyring {
8484
id := None,
8585
kmsConfiguration := kmsConfig,
8686
logicalKeyStoreName := logicalKeyStoreName,
87-
grantTokens := None,
88-
ddbTableName := branchKeyStoreName,
89-
ddbClient := Some(ddbClient),
90-
kmsClient := Some(kmsClient)
87+
storage := Some(
88+
KeyStoreTypes.ddb(
89+
KeyStoreTypes.DynamoDBTable(
90+
ddbTableName := branchKeyStoreName,
91+
ddbClient := Some(ddbClient)
92+
))),
93+
keyManagement := Some(
94+
KeyStoreTypes.kms(
95+
KeyStoreTypes.AwsKms(
96+
kmsClient := Some(kmsClient)
97+
)))
9198
);
9299

93100
var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
@@ -113,7 +120,7 @@ module TestAwsKmsHierarchicalKeyring {
113120
TestRoundtrip(hierarchyKeyring, materials, TEST_ESDK_ALG_SUITE_ID, branchKeyId);
114121
}
115122

116-
method {:test} TestHierarchyClientDBESuite() {
123+
method {:test} {:vcs_split_on_every_assert} TestHierarchyClientDBESuite() {
117124
var branchKeyId := BRANCH_KEY_ID;
118125
// TTL = 166.67 hours
119126
var ttl : Types.PositiveLong := (1 * 60000) * 10;
@@ -127,10 +134,17 @@ module TestAwsKmsHierarchicalKeyring {
127134
id := None,
128135
kmsConfiguration := kmsConfig,
129136
logicalKeyStoreName := logicalKeyStoreName,
130-
grantTokens := None,
131-
ddbTableName := branchKeyStoreName,
132-
ddbClient := Some(ddbClient),
133-
kmsClient := Some(kmsClient)
137+
storage := Some(
138+
KeyStoreTypes.ddb(
139+
KeyStoreTypes.DynamoDBTable(
140+
ddbTableName := branchKeyStoreName,
141+
ddbClient := Some(ddbClient)
142+
))),
143+
keyManagement := Some(
144+
KeyStoreTypes.kms(
145+
KeyStoreTypes.AwsKms(
146+
kmsClient := Some(kmsClient)
147+
)))
134148
);
135149

136150
var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
@@ -156,7 +170,7 @@ module TestAwsKmsHierarchicalKeyring {
156170
TestRoundtrip(hierarchyKeyring, materials, TEST_DBE_ALG_SUITE_ID, branchKeyId);
157171
}
158172

159-
method {:test} TestBranchKeyIdSupplier()
173+
method {:test} {:vcs_split_on_every_assert} TestBranchKeyIdSupplier()
160174
{
161175
var branchKeyIdSupplier: Types.IBranchKeyIdSupplier := new DummyBranchKeyIdSupplier();
162176
// TTL = 166.67 hours
@@ -171,10 +185,17 @@ module TestAwsKmsHierarchicalKeyring {
171185
id := None,
172186
kmsConfiguration := kmsConfig,
173187
logicalKeyStoreName := logicalKeyStoreName,
174-
grantTokens := None,
175-
ddbTableName := branchKeyStoreName,
176-
ddbClient := Some(ddbClient),
177-
kmsClient := Some(kmsClient)
188+
storage := Some(
189+
KeyStoreTypes.ddb(
190+
KeyStoreTypes.DynamoDBTable(
191+
ddbTableName := branchKeyStoreName,
192+
ddbClient := Some(ddbClient)
193+
))),
194+
keyManagement := Some(
195+
KeyStoreTypes.kms(
196+
KeyStoreTypes.AwsKms(
197+
kmsClient := Some(kmsClient)
198+
)))
178199
);
179200

180201
var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
@@ -202,7 +223,7 @@ module TestAwsKmsHierarchicalKeyring {
202223
TestRoundtrip(hierarchyKeyring, materials, TEST_DBE_ALG_SUITE_ID, BRANCH_KEY_ID_B);
203224
}
204225

205-
method {:test} TestInvalidDataKeyError()
226+
method {:test} {:vcs_split_on_every_assert} TestInvalidDataKeyError()
206227
{
207228
var branchKeyIdSupplier: Types.IBranchKeyIdSupplier := new DummyBranchKeyIdSupplier();
208229
// TTL = 166.67 hours
@@ -215,10 +236,17 @@ module TestAwsKmsHierarchicalKeyring {
215236
id := None,
216237
kmsConfiguration := kmsConfig,
217238
logicalKeyStoreName := logicalKeyStoreName,
218-
grantTokens := None,
219-
ddbTableName := branchKeyStoreName,
220-
ddbClient := Some(ddbClient),
221-
kmsClient := Some(kmsClient)
239+
storage := Some(
240+
KeyStoreTypes.ddb(
241+
KeyStoreTypes.DynamoDBTable(
242+
ddbTableName := branchKeyStoreName,
243+
ddbClient := Some(ddbClient)
244+
))),
245+
keyManagement := Some(
246+
KeyStoreTypes.kms(
247+
KeyStoreTypes.AwsKms(
248+
kmsClient := Some(kmsClient)
249+
)))
222250
);
223251
var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
224252
var hierarchyKeyring :- expect mpl.CreateAwsKmsHierarchicalKeyring(
@@ -341,6 +369,13 @@ module TestAwsKmsHierarchicalKeyring {
341369
var kmsClientWest :- expect KMS.KMSClientForRegion(regionWest);
342370
var kmsClientEast :- expect KMS.KMSClientForRegion(regionEast);
343371
var ddbClient :- expect DDB.DynamoDBClient();
372+
// Recommend commenting the assume out while developing this method,
373+
// and just ignore the modifies exeptions,
374+
// and then re-enabling it once everything is safe
375+
assume {:axiom} && kmsClientWest.Modifies == {}
376+
&& kmsClientEast.Modifies == {}
377+
&& ddbClient.Modifies == {};
378+
344379
var kmsConfig := KeyStoreTypes.KMSConfiguration.kmsKeyArn(keyArn);
345380

346381
// Create a Key Store with the a KMS configuration and
@@ -351,7 +386,7 @@ module TestAwsKmsHierarchicalKeyring {
351386
kmsConfiguration := kmsConfig,
352387
logicalKeyStoreName := logicalKeyStoreName,
353388
grantTokens := None,
354-
ddbTableName := branchKeyStoreName,
389+
ddbTableName := Some(branchKeyStoreName),
355390
ddbClient := Some(ddbClient),
356391
kmsClient := Some(kmsClientWest)
357392
);
@@ -367,7 +402,7 @@ module TestAwsKmsHierarchicalKeyring {
367402
kmsConfiguration := kmsConfig,
368403
logicalKeyStoreName := logicalKeyStoreName,
369404
grantTokens := None,
370-
ddbTableName := branchKeyStoreName,
405+
ddbTableName := Some(branchKeyStoreName),
371406
ddbClient := Some(ddbClient),
372407
kmsClient := Some(kmsClientEast)
373408
);
@@ -481,6 +516,13 @@ module TestAwsKmsHierarchicalKeyring {
481516
var kmsClientWest :- expect KMS.KMSClientForRegion(regionWest);
482517
var kmsClientEast :- expect KMS.KMSClientForRegion(regionEast);
483518
var ddbClient :- expect DDB.DynamoDBClient();
519+
// Recommend commenting the assume out while developing this method,
520+
// and just ignore the modifies exeptions,
521+
// and then re-enabling it once everything is safe
522+
assume {:axiom} && kmsClientWest.Modifies == {}
523+
&& kmsClientEast.Modifies == {}
524+
&& ddbClient.Modifies == {};
525+
484526
var kmsConfig := KeyStoreTypes.KMSConfiguration.kmsKeyArn(keyArn);
485527

486528
// Create a Key Store with the a KMS configuration and
@@ -491,7 +533,7 @@ module TestAwsKmsHierarchicalKeyring {
491533
kmsConfiguration := kmsConfig,
492534
logicalKeyStoreName := logicalKeyStoreName,
493535
grantTokens := None,
494-
ddbTableName := branchKeyStoreName,
536+
ddbTableName := Some(branchKeyStoreName),
495537
ddbClient := Some(ddbClient),
496538
kmsClient := Some(kmsClientWest)
497539
);
@@ -507,7 +549,7 @@ module TestAwsKmsHierarchicalKeyring {
507549
kmsConfiguration := kmsConfig,
508550
logicalKeyStoreName := logicalKeyStoreName,
509551
grantTokens := None,
510-
ddbTableName := branchKeyStoreName,
552+
ddbTableName := Some(branchKeyStoreName),
511553
ddbClient := Some(ddbClient),
512554
kmsClient := Some(kmsClientEast)
513555
);
@@ -601,6 +643,13 @@ module TestAwsKmsHierarchicalKeyring {
601643
var kmsClientWest :- expect KMS.KMSClientForRegion(regionWest);
602644
var kmsClientEast :- expect KMS.KMSClientForRegion(regionEast);
603645
var ddbClient :- expect DDB.DynamoDBClient();
646+
// Recommend commenting the assume out while developing this method,
647+
// and just ignore the modifies exeptions,
648+
// and then re-enabling it once everything is safe
649+
assume {:axiom} && kmsClientWest.Modifies == {}
650+
&& kmsClientEast.Modifies == {}
651+
&& ddbClient.Modifies == {};
652+
604653
var kmsConfig := KeyStoreTypes.KMSConfiguration.kmsKeyArn(keyArn);
605654

606655
// Create a Key Store with the a KMS configuration and
@@ -611,7 +660,7 @@ module TestAwsKmsHierarchicalKeyring {
611660
kmsConfiguration := kmsConfig,
612661
logicalKeyStoreName := logicalKeyStoreName,
613662
grantTokens := None,
614-
ddbTableName := branchKeyStoreName,
663+
ddbTableName := Some(branchKeyStoreName),
615664
ddbClient := Some(ddbClient),
616665
kmsClient := Some(kmsClientWest)
617666
);
@@ -627,7 +676,7 @@ module TestAwsKmsHierarchicalKeyring {
627676
kmsConfiguration := kmsConfig,
628677
logicalKeyStoreName := logicalKeyStoreName,
629678
grantTokens := None,
630-
ddbTableName := branchKeyStoreName,
679+
ddbTableName := Some(branchKeyStoreName),
631680
ddbClient := Some(ddbClient),
632681
kmsClient := Some(kmsClientEast)
633682
);
@@ -719,6 +768,13 @@ module TestAwsKmsHierarchicalKeyring {
719768
var kmsClientWest :- expect KMS.KMSClientForRegion(regionWest);
720769
var kmsClientEast :- expect KMS.KMSClientForRegion(regionEast);
721770
var ddbClient :- expect DDB.DynamoDBClient();
771+
772+
// Recommend commenting the assume out while developing this method,
773+
// and just ignore the modifies exeptions,
774+
// and then re-enabling it once everything is safe
775+
assume {:axiom} && kmsClientWest.Modifies == {}
776+
&& kmsClientEast.Modifies == {}
777+
&& ddbClient.Modifies == {};
722778
var kmsConfig := KeyStoreTypes.KMSConfiguration.kmsKeyArn(keyArn);
723779

724780
// Different logical key store names for both Key Stores
@@ -733,7 +789,7 @@ module TestAwsKmsHierarchicalKeyring {
733789
kmsConfiguration := kmsConfig,
734790
logicalKeyStoreName := logicalKeyStoreName,
735791
grantTokens := None,
736-
ddbTableName := branchKeyStoreName,
792+
ddbTableName := Some(branchKeyStoreName),
737793
ddbClient := Some(ddbClient),
738794
kmsClient := Some(kmsClientWest)
739795
);
@@ -750,7 +806,7 @@ module TestAwsKmsHierarchicalKeyring {
750806
kmsConfiguration := kmsConfig,
751807
logicalKeyStoreName := logicalKeyStoreNameNew,
752808
grantTokens := None,
753-
ddbTableName := branchKeyStoreName,
809+
ddbTableName := Some(branchKeyStoreName),
754810
ddbClient := Some(ddbClient),
755811
kmsClient := Some(kmsClientEast)
756812
);

0 commit comments

Comments
 (0)