Skip to content

Commit e5687d0

Browse files
ajewellamzajewellamz
committed
test
1 parent 8f3139b commit e5687d0

File tree

2 files changed

+141
-3
lines changed

2 files changed

+141
-3
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ module PutItemTransformTest {
99
import opened TestFixtures
1010
import DDB = ComAmazonawsDynamodbTypes
1111
import AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
12+
import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes
1213

1314
method {:test} TestPutItemInputPassthrough() {
1415
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms();
@@ -35,6 +36,89 @@ module PutItemTransformTest {
3536
expect_equal("PutItemInput", transformed.value.transformedInput, input);
3637
}
3738

39+
// DynamoDB String :: cast string to DDB.AttributeValue.S
40+
function method DS(x : string) : DDB.AttributeValue
41+
{
42+
DDB.AttributeValue.S(x)
43+
}
44+
function method BasicItem() : DDB.AttributeMap
45+
{
46+
map[
47+
"bar" := DS("baz")
48+
]
49+
}
50+
method {:test} TestPutItemInputMultiNone() {
51+
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(None);
52+
var tableName := GetTableName("foo");
53+
var input := DDB.PutItemInput(
54+
TableName := tableName,
55+
Item := BasicItem()
56+
);
57+
var transformed := middlewareUnderTest.PutItemInputTransform(
58+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput(
59+
sdkInput := input
60+
)
61+
);
62+
expect transformed.Failure?;
63+
expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException(
64+
message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy");
65+
}
66+
67+
method {:test} TestPutItemInputMultiForbidForbid() {
68+
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(
69+
Some(PlaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ)
70+
);
71+
var tableName := GetTableName("foo");
72+
var input := DDB.PutItemInput(
73+
TableName := tableName,
74+
Item := BasicItem()
75+
);
76+
var transformed := middlewareUnderTest.PutItemInputTransform(
77+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput(
78+
sdkInput := input
79+
)
80+
);
81+
expect transformed.Failure?;
82+
expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException(
83+
message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy");
84+
}
85+
86+
method {:test} TestPutItemInputMultiForbidAllow() {
87+
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(
88+
Some(PlaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ)
89+
);
90+
var tableName := GetTableName("foo");
91+
var input := DDB.PutItemInput(
92+
TableName := tableName,
93+
Item := BasicItem()
94+
);
95+
var transformed := middlewareUnderTest.PutItemInputTransform(
96+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput(
97+
sdkInput := input
98+
)
99+
);
100+
expect transformed.Failure?;
101+
expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException(
102+
message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy");
103+
}
104+
105+
method {:test} TestPutItemInputMultiForceAllow() {
106+
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(
107+
Some(PlaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ)
108+
);
109+
var tableName := GetTableName("foo");
110+
var input := DDB.PutItemInput(
111+
TableName := tableName,
112+
Item := BasicItem()
113+
);
114+
var transformed := middlewareUnderTest.PutItemInputTransform(
115+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput(
116+
sdkInput := input
117+
)
118+
);
119+
expect transformed.Success?;
120+
}
121+
38122
method {:test} TestPutItemOutputPassthrough() {
39123
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms();
40124
var output := DDB.PutItemOutput(

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy

Lines changed: 57 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0
33
include "../src/Index.dfy"
4+
include "../../DynamoDbEncryption/test/BeaconTestFixtures.dfy"
45

56
module TestFixtures {
67
import opened Wrappers
@@ -9,6 +10,7 @@ module TestFixtures {
910
import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
1011
import opened AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
1112
import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes
13+
import opened BeaconTestFixtures
1214
import DynamoDbEncryptionTransforms
1315
import DynamoDbItemEncryptor
1416
import AwsCryptographyMaterialProvidersTypes
@@ -216,7 +218,7 @@ module TestFixtures {
216218
ensures fresh(encryption.Modifies)
217219
{
218220
var keyring := GetKmsKeyring();
219-
var encryption2 : IDynamoDbEncryptionTransformsClient :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
221+
encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
220222
DynamoDbTablesEncryptionConfig(
221223
tableEncryptionConfigs := map[
222224
"foo" := DynamoDbTableEncryptionConfig(
@@ -241,8 +243,60 @@ module TestFixtures {
241243
]
242244
)
243245
);
244-
assert encryption2 is DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient;
245-
encryption := encryption2 as DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient;
246246
assume {:axiom} fresh(encryption.Modifies);
247247
}
248+
249+
// type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
250+
251+
function method GetMultiActions() : AttributeActions
252+
{
253+
map[
254+
"bar" := SE.SIGN_ONLY,
255+
"std2" := SE.ENCRYPT_AND_SIGN,
256+
"std4" := SE.ENCRYPT_AND_SIGN,
257+
"std6" := SE.ENCRYPT_AND_SIGN,
258+
"Name" := SE.ENCRYPT_AND_SIGN,
259+
"Title" := SE.ENCRYPT_AND_SIGN,
260+
"TooBad" := SE.ENCRYPT_AND_SIGN,
261+
"Year" := SE.SIGN_ONLY,
262+
"Date" := SE.SIGN_ONLY,
263+
"TheKeyField" := SE.SIGN_ONLY
264+
]
265+
}
266+
267+
method GetDynamoDbEncryptionTransformsMutli(plaintextOverride : Option<AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride>)
268+
returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
269+
ensures encryption.ValidState()
270+
ensures fresh(encryption)
271+
ensures fresh(encryption.Modifies)
272+
{
273+
var keyring := GetKmsKeyring();
274+
var beacons := GetLotsaBeaconsMulti();
275+
var search := SearchConfig (
276+
versions := [beacons],
277+
writeVersion := 1
278+
);
279+
encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
280+
DynamoDbTablesEncryptionConfig(
281+
tableEncryptionConfigs := map[
282+
"foo" := DynamoDbTableEncryptionConfig(
283+
logicalTableName := "foo",
284+
partitionKeyName := "bar",
285+
sortKeyName := None(),
286+
attributeActionsOnEncrypt := GetMultiActions(),
287+
allowedUnsignedAttributes := Some(["plain"]),
288+
allowedUnsignedAttributePrefix := None(),
289+
algorithmSuiteId := None(),
290+
keyring := Some(keyring),
291+
cmm := None(),
292+
search := Some(search),
293+
legacyOverride := None,
294+
plaintextOverride := plaintextOverride
295+
)
296+
]
297+
)
298+
);
299+
assume {:axiom} fresh(encryption.Modifies);
300+
}
301+
248302
}

0 commit comments

Comments
 (0)