Skip to content

Commit 0e3011c

Browse files
rishav-karanjitrishav-karanjit
authored
chore(dafny): refactor HV1 MRK test to use helper methods (#1399)
1 parent 71f482d commit 0e3011c

File tree

2 files changed

+153
-103
lines changed

2 files changed

+153
-103
lines changed

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy

+53-4
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,19 @@ module Fixtures {
100100
const KmsMrkConfigAP : Types.KMSConfiguration := Types.KMSConfiguration.kmsMRKeyArn(MrkArnAP)
101101
const KmsMrkEC : Types.EncryptionContext := map[UTF8.EncodeAscii("abc") := UTF8.EncodeAscii("123")]
102102
const EastBranchKey : string := "MyEastBranch2"
103+
const EastBranchKeyIdActiveVersion : string := "6f22825b-bd56-4434-83e2-2782e2160172"
104+
const EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes: seq<uint8> := [
105+
54, 102, 50, 50, 56, 50, 53, 98, 45, 98, 100,
106+
53, 54, 45, 52, 52, 51, 52, 45, 56, 51, 101, 50,
107+
45, 50, 55, 56, 50, 101, 50, 49, 54, 48, 49, 55, 50
108+
]
103109
const WestBranchKey : string := "MyWestBranch2"
110+
const WestBranchKeyIdActiveVersion : string := "094715a4-b98d-4c98-bf50-17422a8938f4"
111+
const WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes: seq<uint8> := [
112+
48, 57, 52, 55, 49, 53, 97, 52, 45, 98, 57, 56,
113+
100, 45, 52, 99, 57, 56, 45, 98, 102, 53, 48, 45,
114+
49, 55, 52, 50, 50, 97, 56, 57, 51, 56, 102, 52
115+
]
104116
const publicKeyArn := "arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f"
105117

106118
// TODO: After ~2024/06/11 launch, add the next two lines to cfn/ESDK-Hierarchy-CI.yaml
@@ -243,36 +255,73 @@ module Fixtures {
243255
return Success(keyStore);
244256
}
245257

246-
method KeyStoreWithNoClient(
258+
method KeyStoreWithOptionalClient(
247259
nameonly kmsId: string := keyArn,
248260
nameonly physicalName: string := branchKeyStoreName,
249-
nameonly logicalName: string := logicalKeyStoreName
261+
nameonly logicalName: string := logicalKeyStoreName,
262+
nameonly ddbClient?: Option<DDB.Types.IDynamoDBClient> := None,
263+
nameonly kmsClient?: Option<KMS.Types.IKMSClient> := None,
264+
nameonly srkKey: bool := true,
265+
nameonly mrkKey: bool := false
250266
)
251267
returns (output: Result<Types.IKeyStoreClient, Types.Error>)
252268
requires DDB.Types.IsValid_TableName(physicalName)
253269
requires KMS.Types.IsValid_KeyIdType(kmsId)
270+
requires srkKey != mrkKey
254271
ensures output.Success? ==> output.value.ValidState()
255272
ensures output.Success?
256273
==>
257274
&& output.value.ValidState()
258275
&& fresh(output.value)
259276
&& fresh(output.value.Modifies)
260277
{
261-
var kmsConfig := Types.KMSConfiguration.kmsKeyArn(kmsId);
278+
if ddbClient?.Some? {
279+
assume {:axiom} fresh(ddbClient?.value) && fresh(ddbClient?.value.Modifies);
280+
}
281+
if kmsClient?.Some? {
282+
assume {:axiom} fresh(kmsClient?.value) && fresh(kmsClient?.value.Modifies);
283+
}
284+
expect srkKey != mrkKey;
285+
var kmsConfig := if srkKey then
286+
createSrkKMSConfig(kmsId)
287+
else
288+
createMrkKMSConfig(kmsId);
289+
expect srkKey ==> kmsConfig.kmsKeyArn?;
290+
expect mrkKey ==> kmsConfig.kmsMRKeyArn?;
262291
var keyStoreConfig := Types.KeyStoreConfig(
263292
id := None,
264293
kmsConfiguration := kmsConfig,
265294
logicalKeyStoreName := logicalName,
266295
storage := Some(
267296
Types.ddb(
268297
Types.DynamoDBTable(
269-
ddbTableName := physicalName
298+
ddbTableName := physicalName,
299+
ddbClient := ddbClient?
300+
))),
301+
keyManagement := Some(
302+
Types.kms(
303+
Types.AwsKms(
304+
kmsClient := kmsClient?
270305
)))
271306
);
272307
var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
273308
return Success(keyStore);
274309
}
275310

311+
function method createSrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration)
312+
requires KMS.Types.IsValid_KeyIdType(kmsId)
313+
ensures output.kmsKeyArn?
314+
{
315+
Types.KMSConfiguration.kmsKeyArn(kmsId)
316+
}
317+
318+
function method createMrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration)
319+
requires KMS.Types.IsValid_KeyIdType(kmsId)
320+
ensures output.kmsMRKeyArn?
321+
{
322+
Types.KMSConfiguration.kmsMRKeyArn(kmsId)
323+
}
324+
276325
datatype allThree = | allThree (
277326
active: Types.EncryptedHierarchicalKey,
278327
beacon: Types.EncryptedHierarchicalKey,

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy

+100-99
Original file line numberDiff line numberDiff line change
@@ -77,128 +77,89 @@ module TestGetKeys {
7777
{
7878
var ddbClient :- expect DDB.DynamoDBClient();
7979

80-
var eastKeyStoreConfig := Types.KeyStoreConfig(
81-
id := None,
82-
kmsConfiguration := KmsConfigEast,
83-
logicalKeyStoreName := logicalKeyStoreName,
84-
storage := Some(
85-
Types.ddb(
86-
Types.DynamoDBTable(
87-
ddbTableName := branchKeyStoreName,
88-
ddbClient := Some(ddbClient)
89-
)))
80+
var westKeyStore :- expect KeyStoreWithOptionalClient(
81+
kmsId := MrkArnWest,
82+
physicalName := branchKeyStoreName,
83+
logicalName := logicalKeyStoreName,
84+
ddbClient? := Some(ddbClient)
9085
);
9186

92-
var westKeyStoreConfig := Types.KeyStoreConfig(
93-
id := None,
94-
kmsConfiguration := KmsConfigWest,
95-
logicalKeyStoreName := logicalKeyStoreName,
96-
storage := Some(
97-
Types.ddb(
98-
Types.DynamoDBTable(
99-
ddbTableName := branchKeyStoreName,
100-
ddbClient := Some(ddbClient)
101-
)))
87+
var eastKeyStore :- expect KeyStoreWithOptionalClient(
88+
kmsId := MrkArnEast,
89+
physicalName := branchKeyStoreName,
90+
logicalName := logicalKeyStoreName,
91+
ddbClient? := Some(ddbClient)
10292
);
10393

104-
var eastMrkKeyStoreConfig := Types.KeyStoreConfig(
105-
id := None,
106-
kmsConfiguration := KmsMrkConfigEast,
107-
logicalKeyStoreName := logicalKeyStoreName,
108-
storage := Some(
109-
Types.ddb(
110-
Types.DynamoDBTable(
111-
ddbTableName := branchKeyStoreName,
112-
ddbClient := Some(ddbClient)
113-
)))
94+
var westMrkKeyStore :- expect KeyStoreWithOptionalClient(
95+
kmsId := MrkArnWest,
96+
physicalName := branchKeyStoreName,
97+
logicalName := logicalKeyStoreName,
98+
ddbClient? := Some(ddbClient),
99+
srkKey := false,
100+
mrkKey := true
114101
);
115102

116-
var westMrkKeyStoreConfig := Types.KeyStoreConfig(
117-
id := None,
118-
kmsConfiguration := KmsMrkConfigWest,
119-
logicalKeyStoreName := logicalKeyStoreName,
120-
storage := Some(
121-
Types.ddb(
122-
Types.DynamoDBTable(
123-
ddbTableName := branchKeyStoreName,
124-
ddbClient := Some(ddbClient)
125-
)))
103+
var eastMrkKeyStore :- expect KeyStoreWithOptionalClient(
104+
kmsId := MrkArnEast,
105+
physicalName := branchKeyStoreName,
106+
logicalName := logicalKeyStoreName,
107+
ddbClient? := Some(ddbClient),
108+
srkKey := false,
109+
mrkKey := true
126110
);
127111

128-
// KmsMrkConfigAP is NOT created
129-
var apMrkKeyStoreConfig := Types.KeyStoreConfig(
130-
id := None,
131-
kmsConfiguration := KmsMrkConfigAP,
132-
logicalKeyStoreName := logicalKeyStoreName,
133-
storage := Some(
134-
Types.ddb(
135-
Types.DynamoDBTable(
136-
ddbTableName := branchKeyStoreName,
137-
ddbClient := Some(ddbClient)
138-
)))
112+
var apMrkKeyStore :- expect KeyStoreWithOptionalClient(
113+
kmsId := MrkArnAP,
114+
physicalName := branchKeyStoreName,
115+
logicalName := logicalKeyStoreName,
116+
ddbClient? := Some(ddbClient),
117+
srkKey := false,
118+
mrkKey := true
139119
);
140120

121+
// All four set of keys (branch, beacon and version) should work when the regions match
122+
testActiveBranchKeyHappyCase(westKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
123+
testBeaconKeyHappyCase(westKeyStore, WestBranchKey);
124+
testBranchKeyVersionHappyCase(westKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
141125

142-
var westKeyStore :- expect KeyStore.KeyStore(westKeyStoreConfig);
143-
var eastKeyStore :- expect KeyStore.KeyStore(eastKeyStoreConfig);
144-
var westMrkKeyStore :- expect KeyStore.KeyStore(westMrkKeyStoreConfig);
145-
var eastMrkKeyStore :- expect KeyStore.KeyStore(eastMrkKeyStoreConfig);
146-
var apMrkKeyStore :- expect KeyStore.KeyStore(apMrkKeyStoreConfig);
126+
testActiveBranchKeyHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
127+
testBeaconKeyHappyCase(eastKeyStore, EastBranchKey);
128+
testBranchKeyVersionHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
147129

148-
// All four should work when the regions match
130+
testActiveBranchKeyHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
131+
testBeaconKeyHappyCase(westMrkKeyStore, WestBranchKey);
132+
testBranchKeyVersionHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
149133

150-
var activeResult :- expect westKeyStore.GetActiveBranchKey(
151-
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
152-
expect activeResult.branchKeyMaterials.branchKeyIdentifier == WestBranchKey;
153-
expect |activeResult.branchKeyMaterials.branchKey| == 32;
154-
155-
activeResult :- expect eastKeyStore.GetActiveBranchKey(
156-
Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey));
157-
expect activeResult.branchKeyMaterials.branchKeyIdentifier == EastBranchKey;
158-
expect |activeResult.branchKeyMaterials.branchKey| == 32;
159-
160-
activeResult :- expect westMrkKeyStore.GetActiveBranchKey(
161-
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
162-
expect activeResult.branchKeyMaterials.branchKeyIdentifier == WestBranchKey;
163-
expect |activeResult.branchKeyMaterials.branchKey| == 32;
164-
165-
activeResult :- expect eastMrkKeyStore.GetActiveBranchKey(
166-
Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey));
167-
expect activeResult.branchKeyMaterials.branchKeyIdentifier == EastBranchKey;
168-
expect |activeResult.branchKeyMaterials.branchKey| == 32;
134+
testActiveBranchKeyHappyCase(eastMrkKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
135+
testBeaconKeyHappyCase(eastMrkKeyStore, EastBranchKey);
136+
testBranchKeyVersionHappyCase(eastMrkKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
169137

170138
// MRK Configuration should work with the other region
171139

172-
activeResult :- expect westMrkKeyStore.GetActiveBranchKey(
173-
Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey));
174-
expect activeResult.branchKeyMaterials.branchKeyIdentifier == EastBranchKey;
175-
expect |activeResult.branchKeyMaterials.branchKey| == 32;
140+
testActiveBranchKeyHappyCase(westMrkKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
141+
testBeaconKeyHappyCase(westMrkKeyStore, EastBranchKey);
142+
testBranchKeyVersionHappyCase(westMrkKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
176143

177-
activeResult :- expect eastMrkKeyStore.GetActiveBranchKey(
178-
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
179-
expect activeResult.branchKeyMaterials.branchKeyIdentifier == WestBranchKey;
180-
expect |activeResult.branchKeyMaterials.branchKey| == 32;
144+
testActiveBranchKeyHappyCase(eastMrkKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
145+
testBeaconKeyHappyCase(eastMrkKeyStore, WestBranchKey);
146+
testBranchKeyVersionHappyCase(eastMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
181147

182148
// Plain Configuration should fail with the other region
183149

184-
var badResult := westKeyStore.GetActiveBranchKey(
185-
Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey));
186-
expect badResult.Failure?;
187-
expect badResult.error == Types.Error.KeyStoreException(message := ErrorMessages.GET_KEY_ARN_DISAGREEMENT);
150+
GetActiveKeyWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey);
151+
GetBeaconKeyWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey);
152+
GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion);
188153

189-
badResult := eastKeyStore.GetActiveBranchKey(
190-
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
191-
expect badResult.Failure?;
192-
expect badResult.error == Types.Error.KeyStoreException(message := ErrorMessages.GET_KEY_ARN_DISAGREEMENT);
154+
GetActiveKeyWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey);
155+
GetBeaconKeyWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey);
156+
GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion);
193157

194158
// apMrkKeyStore should always fail
195159

196-
badResult := apMrkKeyStore.GetActiveBranchKey(
197-
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
198-
expect badResult.Failure?;
199-
expect badResult.error.ComAmazonawsKms?;
200-
expect badResult.error.ComAmazonawsKms.OpaqueWithText?;
201-
// it's an opaque error, so I can't test its contents
160+
testActiveBranchKeyKMSFailureCase(apMrkKeyStore, WestBranchKey);
161+
testBranchKeyVersionKMSFailureCase(apMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion);
162+
testBeaconKeyKMSFailureCase(apMrkKeyStore, WestBranchKey);
202163
}
203164

204165
method {:test} TestKeyWithIncorrectKmsKeyArn() {
@@ -246,7 +207,7 @@ module TestGetKeys {
246207
method {:test} TestGetKeysWithNoClients() {
247208
var kmsConfig := Types.KMSConfiguration.kmsKeyArn(keyArn);
248209

249-
var keyStore :- expect KeyStoreWithNoClient(kmsId:=keyArn, physicalName:=branchKeyStoreName, logicalName := logicalKeyStoreName);
210+
var keyStore :- expect KeyStoreWithOptionalClient(kmsId:=keyArn, physicalName:=branchKeyStoreName, logicalName := logicalKeyStoreName);
250211

251212
testActiveBranchKeyHappyCase(keyStore, branchKeyId, branchKeyIdActiveVersionUtf8Bytes);
252213
testActiveBranchKeyHappyCase(keyStore, hv2BranchKeyId, hv2BranchKeyIdActiveVersionUtf8Bytes);
@@ -462,6 +423,46 @@ module TestGetKeys {
462423
&& |versionResult.branchKeyMaterials.branchKey| == 32
463424
}
464425

426+
method testActiveBranchKeyKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string)
427+
requires keyStore.ValidState()
428+
modifies keyStore.Modifies
429+
{
430+
var branchKeyResult := keyStore.GetActiveBranchKey(
431+
Types.GetActiveBranchKeyInput(
432+
branchKeyIdentifier := branchKeyId
433+
));
434+
expect branchKeyResult.Failure?;
435+
expect branchKeyResult.error.ComAmazonawsKms?;
436+
expect branchKeyResult.error.ComAmazonawsKms.OpaqueWithText?;
437+
}
438+
439+
method testBranchKeyVersionKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string, branchKeyIdActiveVersion: string)
440+
requires keyStore.ValidState()
441+
modifies keyStore.Modifies
442+
{
443+
var versionResult := keyStore.GetBranchKeyVersion(
444+
Types.GetBranchKeyVersionInput(
445+
branchKeyIdentifier := branchKeyId,
446+
branchKeyVersion := branchKeyIdActiveVersion
447+
));
448+
expect versionResult.Failure?;
449+
expect versionResult.error.ComAmazonawsKms?;
450+
expect versionResult.error.ComAmazonawsKms.OpaqueWithText?;
451+
}
452+
453+
method testBeaconKeyKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string)
454+
requires keyStore.ValidState()
455+
modifies keyStore.Modifies
456+
{
457+
var beaconKeyResult := keyStore.GetBeaconKey(
458+
Types.GetBeaconKeyInput(
459+
branchKeyIdentifier := branchKeyId
460+
));
461+
expect beaconKeyResult.Failure?;
462+
expect beaconKeyResult.error.ComAmazonawsKms?;
463+
expect beaconKeyResult.error.ComAmazonawsKms.OpaqueWithText?;
464+
}
465+
465466
method VerifyGetKeysFromStorage(
466467
identifier : string,
467468
storage : Types.IKeyStorageInterface

0 commit comments

Comments
 (0)