Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 9deae04

Browse files
rishav-karanjitrishav-karanjit
committedMar 26, 2024
Add more test coverage and decrease resource count
1 parent 09b6134 commit 9deae04

File tree

1 file changed

+230
-29
lines changed

1 file changed

+230
-29
lines changed
 

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy

Lines changed: 230 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -4,46 +4,108 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
44
import DynamoDbEncryption
55
import opened StandardLibrary.UInt
66
import opened StructuredEncryptionHeader
7+
import opened StructuredEncryptionUtil
78
import opened UTF8
89
import Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes
910
import UUID
1011
import ComAmazonawsDynamodbTypes
1112
import EdkWrapping
1213
import AlgorithmSuites
1314

14-
const expectedHead := PartialHeader (
15-
version := 1,
16-
flavor := 1,
17-
msgID := [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32],
18-
legend := [0x65, 0x73],
19-
encContext := map[EncodeAscii("abc") := EncodeAscii("def")],
20-
dataKeys := [CMP.EncryptedDataKey(
21-
keyProviderId := EncodeAscii("aws-kms-hierarchy") ,
22-
keyProviderInfo := EncodeAscii("keyproviderInfo"),
23-
ciphertext := [
24-
64, 92, 115, 7, 85, 121, 112, 79, 69, 12, 82, 25, 67, 34,
25-
11, 66, 93, 45, 40, 23, 90, 61, 16, 28, 59, 114, 52, 122,
26-
50, 23, 11, 101, 48, 53, 30, 120, 51, 74, 77, 53, 57, 99,
27-
53, 13, 30, 21, 109, 85, 15, 86, 47, 84, 91, 85, 87, 60, 4,
28-
56, 67, 74, 29, 87, 85, 106, 8, 82, 63, 114, 100, 110, 68,
29-
58, 83, 24, 111, 41, 21, 91, 122, 61, 118, 37, 72, 38, 67, 2,
30-
17, 61, 17, 121, 7, 90, 117, 49, 30, 20, 89, 68, 33, 111,
31-
107, 5, 120, 20, 95, 78, 70, 2, 49, 84, 39, 50, 40, 40, 115,
32-
114, 76, 18, 103, 84, 34, 123, 1, 125, 61, 33, 13, 18, 81,
33-
24, 53, 53, 26, 60, 52, 85, 81, 96, 85, 72])]
34-
)
35-
const serializedHeader := expectedHead.serialize() + expectedHead.msgID
15+
const testVersion : Version := 1
16+
17+
const testFlavor : Flavor := 1
18+
19+
const testMsgID : MessageID := [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32]
20+
21+
const testLegend : Legend := [0x65, 0x73]
22+
23+
const testEncContext : CMPEncryptionContext := map[EncodeAscii("abc") := EncodeAscii("def")]
24+
25+
const testAwsKmsDataKey := CMP.EncryptedDataKey(
26+
keyProviderId := EncodeAscii("aws-kms") ,
27+
keyProviderInfo := EncodeAscii("keyproviderInfo"),
28+
ciphertext := [1, 2, 3, 4, 5])
29+
30+
const testAwsKmsHDataKey := CMP.EncryptedDataKey(
31+
keyProviderId := EncodeAscii("aws-kms-hierarchy") ,
32+
keyProviderInfo := EncodeAscii("keyproviderInfo"),
33+
ciphertext := [
34+
64, 92, 115, 7, 85, 121, 112, 79, 69, 12, 82, 25, 67, 34,
35+
11, 66, 93, 45, 40, 23, 90, 61, 16, 28, 59, 114, 52, 122,
36+
50, 23, 11, 101, 48, 53, 30, 120, 51, 74, 77, 53, 57, 99,
37+
53, 13, 30, 21, 109, 85, 15, 86, 47, 84, 91, 85, 87, 60, 4,
38+
56, 67, 74, 29, 87, 85, 106, 8, 82, 63, 114, 100, 110, 68,
39+
58, 83, 24, 111, 41, 21, 91, 122, 61, 118, 37, 72, 38, 67, 2,
40+
17, 61, 17, 121, 7, 90, 117, 49, 30, 20, 89, 68, 33, 111,
41+
107, 5, 120, 20, 95, 78, 70, 2, 49, 84, 39, 50, 40, 40, 115,
42+
114, 76, 18, 103, 84, 34, 123, 1, 125, 61, 33, 13, 18, 81,
43+
24, 53, 53, 26, 60, 52, 85, 81, 96, 85, 72])
44+
45+
const testRawRsaDataKey := CMP.EncryptedDataKey(
46+
keyProviderId := EncodeAscii("raw-rsa") ,
47+
keyProviderInfo := [1, 2, 3, 4, 5],
48+
ciphertext := [6, 7, 8, 9])
49+
50+
const testAwsKmsRsaDataKey := CMP.EncryptedDataKey(
51+
keyProviderId := EncodeAscii("aws-kms-rsa") ,
52+
keyProviderInfo := EncodeAscii("keyproviderInfo"),
53+
ciphertext := [1, 2, 3, 4, 5])
54+
3655
const algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384
3756

38-
method {:test} TestHeaderInputCase()
57+
method CreatePartialHeader(version : Version, flavor : Flavor, msgID : MessageID, legend : Legend, encContext : CMPEncryptionContext, dataKeyList : CMPEncryptedDataKeyList)
58+
returns (result: PartialHeader)
59+
ensures result.version == version
60+
ensures result.flavor == flavor
61+
ensures result.msgID == msgID
62+
ensures result.legend == legend
63+
ensures result.encContext == encContext
64+
ensures result.dataKeys == dataKeyList
3965
{
40-
expect EdkWrapping.GetProviderWrappedMaterial(expectedHead.dataKeys[0].ciphertext, algorithmSuite).Success?;
41-
var providerWrappedMaterial := EdkWrapping.GetProviderWrappedMaterial(expectedHead.dataKeys[0].ciphertext, algorithmSuite).Extract();
66+
result := PartialHeader (
67+
version := version,
68+
flavor := flavor,
69+
msgID := msgID,
70+
legend := legend,
71+
encContext := encContext,
72+
dataKeys := dataKeyList
73+
);
74+
}
75+
76+
method {:test} TestHeaderInputAwsKmsDataKeyCase()
77+
{
78+
var expectedHead := CreatePartialHeader(testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey]);
79+
var serializedHeader := expectedHead.serialize() + expectedHead.msgID;
80+
81+
var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption();
82+
83+
var inputVariable: Types.GetEncryptedDataKeyDescriptionInput :=
84+
Types.GetEncryptedDataKeyDescriptionInput(
85+
input := Types.header(header := serializedHeader)
86+
);
87+
88+
var actualDataKeyDescription := ddbEncResources.GetEncryptedDataKeyDescription(inputVariable);
89+
90+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Success?;
91+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Success?;
92+
expect actualDataKeyDescription.Success?;
93+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| > 0;
94+
95+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| == |expectedHead.dataKeys|;
96+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderId == UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Extract();
4297

43-
// The ciphertext structure in the hierarchy keyring contains Salt and IV before Version.
44-
// The length of Salt is 16 and IV is 12 bytes. The length of Version is 16 bytes.
45-
// https://github.com/awslabs/aws-encryption-sdk-specification/blob/master/framework/aws-kms/aws-kms-hierarchical-keyring.md#ciphertext
98+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?;
99+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Extract() == UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Extract();
100+
}
101+
102+
method {:test} TestHeaderInputAwsKmsHDataKeyCase()
103+
{
104+
var expectedHead := CreatePartialHeader(testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsHDataKey]);
105+
var serializedHeader := expectedHead.serialize() + expectedHead.msgID;
46106

107+
expect EdkWrapping.GetProviderWrappedMaterial(expectedHead.dataKeys[0].ciphertext, algorithmSuite).Success?;
108+
var providerWrappedMaterial := EdkWrapping.GetProviderWrappedMaterial(expectedHead.dataKeys[0].ciphertext, algorithmSuite).Extract();
47109
expect |providerWrappedMaterial| >= (16 + 12 + 16);
48110
var expectedBranchKeyVersionUuid := UUID.FromByteArray(providerWrappedMaterial[16 + 12 .. (16 + 12 + 16)]);
49111
var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption();
@@ -76,8 +138,91 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
76138
}
77139
}
78140

79-
method {:test} TestDDBItemInputCase()
141+
method {:test} TestHeaderInputRawRsaDataKeyDataKeyCase()
142+
{
143+
var expectedHead := CreatePartialHeader(testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testRawRsaDataKey]);
144+
var serializedHeader := expectedHead.serialize() + expectedHead.msgID;
145+
146+
var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption();
147+
148+
var inputVariable: Types.GetEncryptedDataKeyDescriptionInput :=
149+
Types.GetEncryptedDataKeyDescriptionInput(
150+
input := Types.header(header := serializedHeader)
151+
);
152+
153+
var actualDataKeyDescription := ddbEncResources.GetEncryptedDataKeyDescription(inputVariable);
154+
155+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Success?;
156+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Success?;
157+
expect actualDataKeyDescription.Success?;
158+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| > 0;
159+
160+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| == |expectedHead.dataKeys|;
161+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderId == UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Extract();
162+
163+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?;
164+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Extract() == UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Extract();
165+
}
166+
167+
method {:test} TestHeaderInputAwsKmsRsaDataKeyCase()
168+
{
169+
var expectedHead := CreatePartialHeader(testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsRsaDataKey]);
170+
var serializedHeader := expectedHead.serialize() + expectedHead.msgID;
171+
172+
var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption();
173+
174+
var inputVariable: Types.GetEncryptedDataKeyDescriptionInput :=
175+
Types.GetEncryptedDataKeyDescriptionInput(
176+
input := Types.header(header := serializedHeader)
177+
);
178+
179+
var actualDataKeyDescription := ddbEncResources.GetEncryptedDataKeyDescription(inputVariable);
180+
181+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Success?;
182+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Success?;
183+
expect actualDataKeyDescription.Success?;
184+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| > 0;
185+
186+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| == |expectedHead.dataKeys|;
187+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderId == UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Extract();
188+
189+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?;
190+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Extract() == UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Extract();
191+
}
192+
193+
194+
method {:test} TestDDBItemInputAwsKmsDataKeyCase()
195+
{
196+
var expectedHead := CreatePartialHeader(testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsDataKey]);
197+
var serializedHeader := expectedHead.serialize() + expectedHead.msgID;
198+
199+
var attr := map["aws_dbe_head" := ComAmazonawsDynamodbTypes.AttributeValue.B(serializedHeader)];
200+
var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption();
201+
202+
var inputVariable: Types.GetEncryptedDataKeyDescriptionInput :=
203+
Types.GetEncryptedDataKeyDescriptionInput(
204+
input := Types.plaintextItem(plaintextItem := attr)
205+
);
206+
207+
var actualDataKeyDescription := ddbEncResources.GetEncryptedDataKeyDescription(inputVariable);
208+
209+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Success?;
210+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Success?;
211+
expect actualDataKeyDescription.Success?;
212+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| > 0;
213+
214+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| == |expectedHead.dataKeys|;
215+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderId == UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Extract();
216+
217+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?;
218+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Extract() == UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Extract();
219+
}
220+
221+
method {:test} TestDDBItemInputAwsKmsHDataKeyCase()
80222
{
223+
var expectedHead := CreatePartialHeader(testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsHDataKey]);
224+
var serializedHeader := expectedHead.serialize() + expectedHead.msgID;
225+
81226
expect EdkWrapping.GetProviderWrappedMaterial(expectedHead.dataKeys[0].ciphertext, algorithmSuite).Success?;
82227
var providerWrappedMaterial := EdkWrapping.GetProviderWrappedMaterial(expectedHead.dataKeys[0].ciphertext, algorithmSuite).Extract();
83228

@@ -115,4 +260,60 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
115260
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].branchKeyVersion.Extract() == expectedBranchKeyVersionUuid.Extract();
116261
}
117262
}
263+
264+
method {:test} TestDDBItemInputRawRsaDataKeyCase()
265+
{
266+
var expectedHead := CreatePartialHeader(testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testRawRsaDataKey]);
267+
var serializedHeader := expectedHead.serialize() + expectedHead.msgID;
268+
269+
var attr := map["aws_dbe_head" := ComAmazonawsDynamodbTypes.AttributeValue.B(serializedHeader)];
270+
var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption();
271+
272+
273+
var inputVariable: Types.GetEncryptedDataKeyDescriptionInput :=
274+
Types.GetEncryptedDataKeyDescriptionInput(
275+
input := Types.plaintextItem(plaintextItem := attr)
276+
);
277+
278+
var actualDataKeyDescription := ddbEncResources.GetEncryptedDataKeyDescription(inputVariable);
279+
280+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Success?;
281+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Success?;
282+
expect actualDataKeyDescription.Success?;
283+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| > 0;
284+
285+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| == |expectedHead.dataKeys|;
286+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderId == UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Extract();
287+
288+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?;
289+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Extract() == UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Extract();
290+
}
291+
292+
method {:test} TestDDBItemInputAwsKmsRsaDataKeyCase()
293+
{
294+
var expectedHead := CreatePartialHeader(testVersion, testFlavor, testMsgID, testLegend, testEncContext, [testAwsKmsRsaDataKey]);
295+
var serializedHeader := expectedHead.serialize() + expectedHead.msgID;
296+
297+
var attr := map["aws_dbe_head" := ComAmazonawsDynamodbTypes.AttributeValue.B(serializedHeader)];
298+
var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption();
299+
300+
301+
var inputVariable: Types.GetEncryptedDataKeyDescriptionInput :=
302+
Types.GetEncryptedDataKeyDescriptionInput(
303+
input := Types.plaintextItem(plaintextItem := attr)
304+
);
305+
306+
var actualDataKeyDescription := ddbEncResources.GetEncryptedDataKeyDescription(inputVariable);
307+
308+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Success?;
309+
expect UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Success?;
310+
expect actualDataKeyDescription.Success?;
311+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| > 0;
312+
313+
expect |actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput| == |expectedHead.dataKeys|;
314+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderId == UTF8.Decode(expectedHead.dataKeys[0].keyProviderId).Extract();
315+
316+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Some?;
317+
expect actualDataKeyDescription.Extract().EncryptedDataKeyDescriptionOutput[0].keyProviderInfo.Extract() == UTF8.Decode(expectedHead.dataKeys[0].keyProviderInfo).Extract();
318+
}
118319
}

0 commit comments

Comments
 (0)
Please sign in to comment.