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 1d892d6

Browse files
ajewellamzajewellamz
committedAug 2, 2024··
tests
1 parent 55c521a commit 1d892d6

File tree

2 files changed

+166
-21
lines changed

2 files changed

+166
-21
lines changed
 

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

Lines changed: 135 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,10 @@ module QueryTransformTest {
88
import opened DynamoDbEncryptionTransforms
99
import opened TestFixtures
1010
import DDB = ComAmazonawsDynamodbTypes
11-
import AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
11+
import DBT = AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
12+
import DBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes
13+
import Types = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
14+
import AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
1215

1316
method {:test} TestQueryInputPassthrough() {
1417
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms();
@@ -53,23 +56,7 @@ module QueryTransformTest {
5356
);
5457
var tableName := GetTableName("no_such_table");
5558
var input := DDB.QueryInput(
56-
TableName := tableName,
57-
IndexName := None(),
58-
Select := None(),
59-
AttributesToGet := None(),
60-
Limit := None(),
61-
ConsistentRead := None(),
62-
KeyConditions := None(),
63-
QueryFilter := None(),
64-
ConditionalOperator := None(),
65-
ScanIndexForward := None(),
66-
ExclusiveStartKey := None(),
67-
ReturnConsumedCapacity := None(),
68-
ProjectionExpression := None(),
69-
FilterExpression := None(),
70-
KeyConditionExpression := None(),
71-
ExpressionAttributeNames := None(),
72-
ExpressionAttributeValues := None()
59+
TableName := tableName
7360
);
7461
var transformed := middlewareUnderTest.QueryOutputTransform(
7562
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.QueryOutputTransformInput(
@@ -81,4 +68,134 @@ module QueryTransformTest {
8168
expect_ok("QueryOutput", transformed);
8269
expect_equal("QueryOutput", transformed.value.transformedOutput, output);
8370
}
71+
72+
function method DDBS(x : string) : DDB.AttributeValue {
73+
DDB.AttributeValue.S(x)
74+
}
75+
76+
const Actions1 : DBE.AttributeActions := map[
77+
GetAttrName("bar") := CSE.SIGN_ONLY,
78+
GetAttrName("sortKey") := CSE.SIGN_ONLY,
79+
GetAttrName("encrypt1") := CSE.ENCRYPT_AND_SIGN,
80+
GetAttrName("encrypt2") := CSE.ENCRYPT_AND_SIGN,
81+
GetAttrName("sign1") := CSE.SIGN_ONLY,
82+
GetAttrName("sign2") := CSE.SIGN_ONLY
83+
]
84+
85+
method {:test} TestDecryptErrorWithSortKey() {
86+
var config := TestFixtures.GetEncryptorConfigFromActions(Actions1, Some("sortKey"));
87+
var encryptor := TestFixtures.GetDynamoDbItemEncryptorFrom(config);
88+
89+
var inputItem : map<DDB.AttributeName, DDB.AttributeValue> := map[
90+
"bar" := DDB.AttributeValue.N("00001234"),
91+
"sortKey" := DDB.AttributeValue.B([1,2,3,4]),
92+
"encrypt1" := DDBS("some text"),
93+
"encrypt2" := DDBS("more text"),
94+
"sign1" := DDBS("stuff"),
95+
"sign2" := DDB.AttributeValue.BOOL(false)
96+
];
97+
98+
var encryptRes :- expect encryptor.EncryptItem(
99+
Types.EncryptItemInput(
100+
plaintextItem:=inputItem
101+
)
102+
);
103+
var item1 := encryptRes.encryptedItem;
104+
expect "encrypt1" in item1;
105+
expect item1["encrypt1"] != DDBS("some text");
106+
107+
inputItem := map[
108+
"bar" := DDB.AttributeValue.N("567"),
109+
"sortKey" := DDB.AttributeValue.B([5,6,7]),
110+
"encrypt1" := DDBS("some text"),
111+
"encrypt2" := DDBS("more text"),
112+
"sign1" := DDBS("stuff"),
113+
"sign2" := DDB.AttributeValue.BOOL(false)
114+
];
115+
encryptRes :- expect encryptor.EncryptItem(
116+
Types.EncryptItemInput(
117+
plaintextItem:=inputItem
118+
)
119+
);
120+
var item2 := encryptRes.encryptedItem;
121+
expect "encrypt1" in item2;
122+
expect item2["encrypt1"] != DDBS("some text");
123+
124+
inputItem := map[
125+
"bar" := DDB.AttributeValue.N("890"),
126+
"sortKey" := DDB.AttributeValue.B([3,1,4]),
127+
"encrypt1" := DDBS("some text"),
128+
"encrypt2" := DDBS("more text"),
129+
"sign1" := DDBS("stuff"),
130+
"sign2" := DDB.AttributeValue.BOOL(false)
131+
];
132+
encryptRes :- expect encryptor.EncryptItem(
133+
Types.EncryptItemInput(
134+
plaintextItem:=inputItem
135+
)
136+
);
137+
var item3 := encryptRes.encryptedItem;
138+
expect "encrypt1" in item3;
139+
expect item3["encrypt1"] != DDBS("some text");
140+
141+
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms2(Actions1, Some("sortKey"));
142+
var tableName := GetTableName("foo");
143+
var input := DDB.QueryInput(
144+
TableName := tableName
145+
);
146+
147+
var transformed := middlewareUnderTest.QueryOutputTransform(
148+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.QueryOutputTransformInput(
149+
sdkOutput := DDB.QueryOutput(Items := Some([item1, item2, item3])),
150+
originalInput := input
151+
)
152+
);
153+
154+
TestFixtures.expect_ok("QueryOutput", transformed);
155+
expect transformed.value.transformedOutput.Items.Some?;
156+
var itemList := transformed.value.transformedOutput.Items.value;
157+
expect |itemList| == 3;
158+
expect "encrypt1" in itemList[0];
159+
expect itemList[0]["encrypt1"] == DDBS("some text");
160+
161+
162+
/// now do some damage
163+
item1 := item1["encrypt1" := item2["encrypt1"]];
164+
transformed := middlewareUnderTest.QueryOutputTransform(
165+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.QueryOutputTransformInput(
166+
sdkOutput := DDB.QueryOutput(Items := Some([item1, item2, item3])),
167+
originalInput := input
168+
)
169+
);
170+
expect transformed.Failure?;
171+
print "\n", transformed.error, "\n";
172+
expect transformed.error ==
173+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.CollectionOfErrors(
174+
[
175+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "No recipient tag matched.")))),
176+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 1234\nsortKey = 01020304")
177+
],
178+
message := "Error(s) found decrypting Query results."
179+
);
180+
181+
/// do more damage
182+
item3 := item3["encrypt1" := item2["encrypt1"]];
183+
transformed := middlewareUnderTest.QueryOutputTransform(
184+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.QueryOutputTransformInput(
185+
sdkOutput := DDB.QueryOutput(Items := Some([item1, item2, item3])),
186+
originalInput := input
187+
)
188+
);
189+
expect transformed.Failure?;
190+
print "\n", transformed.error, "\n";
191+
expect transformed.error ==
192+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.CollectionOfErrors(
193+
[
194+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "No recipient tag matched.")))),
195+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 1234\nsortKey = 01020304"),
196+
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 890\nsortKey = 030104")
197+
],
198+
message := "Error(s) found decrypting Query results."
199+
);
200+
}
84201
}

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

Lines changed: 31 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,10 +23,12 @@ module TestFixtures {
2323
expect DDB.IsValid_TableName(s);
2424
return s;
2525
}
26-
method GetAttrName(s : string) returns (output : DDB.AttributeName)
26+
function method GetAttrName(s : string) : DDB.AttributeName
2727
{
28-
expect DDB.IsValid_AttributeName(s);
29-
return s;
28+
if DDB.IsValid_AttributeName(s) then
29+
s
30+
else
31+
"abc"
3032
}
3133
method GetStatement(s : string) returns (output : DDB.PartiQLStatement)
3234
{
@@ -235,6 +237,32 @@ module TestFixtures {
235237
assume {:axiom} fresh(encryption.Modifies);
236238
}
237239

240+
method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
241+
returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
242+
ensures encryption.ValidState()
243+
ensures fresh(encryption)
244+
ensures fresh(encryption.Modifies)
245+
{
246+
var keyring := GetKmsKeyring();
247+
encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
248+
DynamoDbTablesEncryptionConfig(
249+
tableEncryptionConfigs := map[
250+
"foo" := DynamoDbTableEncryptionConfig(
251+
logicalTableName := "foo",
252+
partitionKeyName := "bar",
253+
sortKeyName := sortKey,
254+
attributeActionsOnEncrypt := actions,
255+
allowedUnsignedAttributes := Some(["plain"]),
256+
allowedUnsignedAttributePrefix := None(),
257+
algorithmSuiteId := None(),
258+
keyring := Some(keyring)
259+
)
260+
]
261+
)
262+
);
263+
assume {:axiom} fresh(encryption.Modifies);
264+
}
265+
238266
// type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
239267

240268
const MultiActions : AttributeActions :=

0 commit comments

Comments
 (0)
Please sign in to comment.