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 07946e7

Browse files
ajewellamzajewellamz
committedFeb 11, 2025··
m
1 parent 4bb289a commit 07946e7

File tree

4 files changed

+253
-28
lines changed

4 files changed

+253
-28
lines changed
 

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,8 @@ module BatchWriteItemTransform {
8181
return Success(BatchWriteItemInputTransformOutput(transformedInput := input.sdkInput.(RequestItems := result)));
8282
}
8383

84+
// Given the encrypted item, find the original plaintext item, based on the never encrypted PK and SK.
85+
// We don't have to worry about duplicates, because DynamoDB will report an error if there are duplicates
8486
method GetOrigItem(
8587
tableConfig : ValidTableConfig,
8688
srcRequests : DDB.WriteRequests,
@@ -109,11 +111,20 @@ module BatchWriteItemTransform {
109111

110112
method Output(config: Config, input: BatchWriteItemOutputTransformInput)
111113
returns (output: Result<BatchWriteItemOutputTransformOutput, Error>)
114+
115+
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-batchwriteitem
116+
//= type=implication
117+
//# If there are no UnprocessedItems, then the BatchWriteItemOutput MUST be returned unchanged.
118+
ensures input.sdkOutput.UnprocessedItems.None? ==>
119+
&& output.Success?
120+
&& output.value.transformedOutput == input.sdkOutput
112121
{
113122
if input.sdkOutput.UnprocessedItems.None? {
114123
return Success(BatchWriteItemOutputTransformOutput(transformedOutput := input.sdkOutput));
115124
}
116125

126+
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-batchwriteitem
127+
//# Each item in UnprocessedItems MUST be replaced by its original plaintext value.
117128
var srcItems := input.originalInput.RequestItems;
118129
var unprocessed := input.sdkOutput.UnprocessedItems.value;
119130
var tableNames := unprocessed.Keys;

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

Lines changed: 203 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module BatchWriteItemTransformTest {
88
import opened DynamoDbEncryptionTransforms
99
import opened TestFixtures
1010
import DDB = ComAmazonawsDynamodbTypes
11-
import AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
11+
import TTypes = AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
1212

1313
method {:test} TestBatchWriteItemInputTransform() {
1414
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms();
@@ -25,7 +25,7 @@ module BatchWriteItemTransformTest {
2525
ReturnItemCollectionMetrics := None
2626
);
2727
var transformed := middlewareUnderTest.BatchWriteItemInputTransform(
28-
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.BatchWriteItemInputTransformInput(
28+
TTypes.BatchWriteItemInputTransformInput(
2929
sdkInput := input
3030
)
3131
);
@@ -34,6 +34,35 @@ module BatchWriteItemTransformTest {
3434
expect_equal("BatchWriteItemInput", transformed.value.transformedInput, input);
3535
}
3636

37+
38+
const Item1 : DDB.AttributeMap := map[
39+
"bar" := DDB.AttributeValue.S("bar1"),
40+
"sign" := DDB.AttributeValue.S("sign1"),
41+
"encrypt" := DDB.AttributeValue.S("encrypt1"),
42+
"plain" := DDB.AttributeValue.S("plain1")
43+
]
44+
45+
const Item2 : DDB.AttributeMap := map[
46+
"bar" := DDB.AttributeValue.S("bar2"),
47+
"sign" := DDB.AttributeValue.S("sign2"),
48+
"encrypt" := DDB.AttributeValue.S("encrypt2"),
49+
"plain" := DDB.AttributeValue.S("plain2")
50+
]
51+
52+
const Item3 : DDB.AttributeMap := map[
53+
"bar" := DDB.AttributeValue.S("bar3"),
54+
"sign" := DDB.AttributeValue.S("sign3"),
55+
"encrypt" := DDB.AttributeValue.S("encrypt3"),
56+
"plain" := DDB.AttributeValue.S("plain3")
57+
]
58+
59+
const Item4 : DDB.AttributeMap := map[
60+
"bar" := DDB.AttributeValue.S("bar4"),
61+
"sign" := DDB.AttributeValue.S("sign4"),
62+
"encrypt" := DDB.AttributeValue.S("encrypt4"),
63+
"plain" := DDB.AttributeValue.S("plain4")
64+
]
65+
3766
method {:test} TestBatchWriteItemOutputTransform() {
3867
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms();
3968
var output := DDB.BatchWriteItemOutput(
@@ -55,7 +84,7 @@ module BatchWriteItemTransformTest {
5584
ReturnItemCollectionMetrics := None
5685
);
5786
var transformed := middlewareUnderTest.BatchWriteItemOutputTransform(
58-
AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.BatchWriteItemOutputTransformInput(
87+
TTypes.BatchWriteItemOutputTransformInput(
5988
sdkOutput := output,
6089
originalInput := input
6190
)
@@ -65,4 +94,175 @@ module BatchWriteItemTransformTest {
6594
expect_equal("BatchWriteItemOutput", transformed.value.transformedOutput, output);
6695
}
6796

97+
function method MakePut(item : DDB.AttributeMap) : DDB.WriteRequest
98+
{
99+
DDB.WriteRequest ( DeleteRequest := None, PutRequest := Some(DDB.PutRequest(Item := item)))
100+
}
101+
102+
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-batchwriteitem
103+
//= type=test
104+
//# Each item in UnprocessedItems MUST be replaced by its original plaintext value.
105+
method {:test} TestBatchWriteItemOutputTransformUnprocessed() {
106+
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms();
107+
var tableName := GetTableName("foo");
108+
109+
var theRequests := GetBatchWriteItemRequestMap(map[tableName := [MakePut(Item1), MakePut(Item2), MakePut(Item3), MakePut(Item4)]]);
110+
111+
var input := DDB.BatchWriteItemInput(
112+
RequestItems := theRequests
113+
);
114+
var transInput :- expect middlewareUnderTest.BatchWriteItemInputTransform(
115+
TTypes.BatchWriteItemInputTransformInput(
116+
sdkInput := input
117+
)
118+
);
119+
120+
var unProcessed : DDB.BatchWriteItemRequestMap := transInput.transformedInput.RequestItems;
121+
expect unProcessed != input.RequestItems;
122+
var output := DDB.BatchWriteItemOutput(
123+
UnprocessedItems := Some(unProcessed)
124+
);
125+
126+
var transOutput :- expect middlewareUnderTest.BatchWriteItemOutputTransform(
127+
TTypes.BatchWriteItemOutputTransformInput(
128+
sdkOutput := output,
129+
originalInput := input
130+
)
131+
);
132+
133+
expect_equal("BatchWriteOutput", transOutput.transformedOutput.UnprocessedItems, Some(theRequests));
134+
}
135+
136+
method {:test} TestBatchWriteItemOutputTransformUnprocessed2() {
137+
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms();
138+
var tableName1 := GetTableName("foo");
139+
var tableName2 := GetTableName("baz");
140+
141+
var theRequests := GetBatchWriteItemRequestMap(map[tableName1 := [MakePut(Item1), MakePut(Item2)], tableName2 := [MakePut(Item3), MakePut(Item4)]]);
142+
143+
var input := DDB.BatchWriteItemInput(
144+
RequestItems := theRequests
145+
);
146+
var transInput :- expect middlewareUnderTest.BatchWriteItemInputTransform(
147+
TTypes.BatchWriteItemInputTransformInput(
148+
sdkInput := input
149+
)
150+
);
151+
152+
var unProcessed : DDB.BatchWriteItemRequestMap := transInput.transformedInput.RequestItems;
153+
expect unProcessed != input.RequestItems;
154+
var output := DDB.BatchWriteItemOutput(
155+
UnprocessedItems := Some(unProcessed)
156+
);
157+
158+
var transOutput :- expect middlewareUnderTest.BatchWriteItemOutputTransform(
159+
TTypes.BatchWriteItemOutputTransformInput(
160+
sdkOutput := output,
161+
originalInput := input
162+
)
163+
);
164+
165+
expect_equal("BatchWriteOutput", transOutput.transformedOutput.UnprocessedItems, Some(theRequests));
166+
}
167+
168+
method {:test} {:vcs_split_on_every_assert} TestBatchWriteItemOutputTransformUnprocessed3() {
169+
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms();
170+
var tableName1 := GetTableName("foo");
171+
var tableName2 := GetTableName("baz");
172+
173+
var theRequests := GetBatchWriteItemRequestMap(map[tableName1 := [MakePut(Item1), MakePut(Item2)], tableName2 := [MakePut(Item3), MakePut(Item4)]]);
174+
175+
var input := DDB.BatchWriteItemInput(
176+
RequestItems := theRequests
177+
);
178+
var transInput :- expect middlewareUnderTest.BatchWriteItemInputTransform(
179+
TTypes.BatchWriteItemInputTransformInput(
180+
sdkInput := input
181+
)
182+
);
183+
184+
expect tableName1 in transInput.transformedInput.RequestItems;
185+
expect tableName2 in transInput.transformedInput.RequestItems;
186+
187+
var list := map[
188+
tableName1 := transInput.transformedInput.RequestItems[tableName1][0..1],
189+
tableName2 := transInput.transformedInput.RequestItems[tableName2][0..1]
190+
];
191+
expect DDB.IsValid_BatchWriteItemRequestMap(list);
192+
var unProcessed : DDB.BatchWriteItemRequestMap := list;
193+
194+
var orig_list := map [
195+
tableName1 := [MakePut(Item1)],
196+
tableName2 := [MakePut(Item3)]
197+
];
198+
expect DDB.IsValid_BatchWriteItemRequestMap(orig_list);
199+
var originalUnProcessed : DDB.BatchWriteItemRequestMap := orig_list;
200+
201+
expect unProcessed != input.RequestItems;
202+
var output := DDB.BatchWriteItemOutput(
203+
UnprocessedItems := Some(unProcessed)
204+
);
205+
206+
var transOutput :- expect middlewareUnderTest.BatchWriteItemOutputTransform(
207+
TTypes.BatchWriteItemOutputTransformInput(
208+
sdkOutput := output,
209+
originalInput := input
210+
)
211+
);
212+
213+
expect_equal("BatchWriteOutput", transOutput.transformedOutput.UnprocessedItems, Some(originalUnProcessed));
214+
}
215+
216+
const Item1a : DDB.AttributeMap := map[
217+
"bar" := DDB.AttributeValue.S("bar1"),
218+
"sign" := DDB.AttributeValue.S("sign2"),
219+
"encrypt" := DDB.AttributeValue.S("encrypt2"),
220+
"plain" := DDB.AttributeValue.S("plain2")
221+
]
222+
223+
const Item1b : DDB.AttributeMap := map[
224+
"bar" := DDB.AttributeValue.S("bar1"),
225+
"sign" := DDB.AttributeValue.S("sign3"),
226+
"encrypt" := DDB.AttributeValue.S("encrypt3"),
227+
"plain" := DDB.AttributeValue.S("plain3")
228+
]
229+
230+
const Item1c : DDB.AttributeMap := map[
231+
"bar" := DDB.AttributeValue.S("bar1"),
232+
"sign" := DDB.AttributeValue.S("sign4"),
233+
"encrypt" := DDB.AttributeValue.S("encrypt4"),
234+
"plain" := DDB.AttributeValue.S("plain4")
235+
]
236+
237+
method {:test} TestBatchWriteItemOutputTransformUnprocessed4() {
238+
var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms2();
239+
var tableName1 := GetTableName("foo");
240+
var tableName2 := GetTableName("baz");
241+
242+
var theRequests := GetBatchWriteItemRequestMap(map[tableName1 := [MakePut(Item1), MakePut(Item1a)], tableName2 := [MakePut(Item1b), MakePut(Item1c)]]);
243+
244+
var input := DDB.BatchWriteItemInput(
245+
RequestItems := theRequests
246+
);
247+
var transInput :- expect middlewareUnderTest.BatchWriteItemInputTransform(
248+
TTypes.BatchWriteItemInputTransformInput(
249+
sdkInput := input
250+
)
251+
);
252+
253+
var unProcessed : DDB.BatchWriteItemRequestMap := transInput.transformedInput.RequestItems;
254+
expect unProcessed != input.RequestItems;
255+
var output := DDB.BatchWriteItemOutput(
256+
UnprocessedItems := Some(unProcessed)
257+
);
258+
259+
var transOutput :- expect middlewareUnderTest.BatchWriteItemOutputTransform(
260+
TTypes.BatchWriteItemOutputTransformInput(
261+
sdkOutput := output,
262+
originalInput := input
263+
)
264+
);
265+
266+
expect_equal("BatchWriteOutput", transOutput.transformedOutput.UnprocessedItems, Some(theRequests));
267+
}
68268
}

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

Lines changed: 32 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ module TestFixtures {
1919
import DDB = ComAmazonawsDynamodbTypes
2020

2121
method GetTableName(s : string) returns (output : DDB.TableName)
22+
ensures DDB.IsValid_TableArn(output)
2223
{
2324
expect DDB.IsValid_TableName(s);
2425
return s;
@@ -237,31 +238,37 @@ module TestFixtures {
237238
assume {:axiom} fresh(encryption.Modifies);
238239
}
239240

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-
// }
241+
method GetDynamoDbEncryptionTransforms2()
242+
returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
243+
ensures encryption.ValidState()
244+
ensures fresh(encryption)
245+
ensures fresh(encryption.Modifies)
246+
{
247+
expect DDB.IsValid_TableName("foo");
248+
var keyring := GetKmsKeyring();
249+
encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
250+
DynamoDbTablesEncryptionConfig(
251+
tableEncryptionConfigs := map[
252+
"foo" := DynamoDbTableEncryptionConfig(
253+
logicalTableName := "foo",
254+
partitionKeyName := "bar",
255+
sortKeyName := Some("sign"),
256+
attributeActionsOnEncrypt := map[
257+
"bar" := CSE.SIGN_ONLY,
258+
"sign" := CSE.SIGN_ONLY,
259+
"encrypt" := CSE.ENCRYPT_AND_SIGN,
260+
"plain" := CSE.DO_NOTHING
261+
],
262+
allowedUnsignedAttributes := Some(["plain"]),
263+
allowedUnsignedAttributePrefix := None(),
264+
algorithmSuiteId := None(),
265+
keyring := Some(keyring)
266+
)
267+
]
268+
)
269+
);
270+
assume {:axiom} fresh(encryption.Modifies);
271+
}
265272

266273
// type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
267274

‎specification/dynamodb-encryption-client/ddb-sdk-integration.md

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -125,6 +125,7 @@ MUST have the following modified behavior:
125125
- [Encrypt before PutItem](#encrypt-before-putitem)
126126
- [Encrypt before BatchWriteItem](#encrypt-before-batchwriteitem)
127127
- [Encrypt before TransactWriteItems](#encrypt-before-transactwriteitems)
128+
- [Decrypt after BatchWriteItem](#encrypt-before-batchwriteitem)
128129
- [Decrypt after GetItem](#decrypt-after-getitem)
129130
- [Decrypt after PutItem](#decrypt-after-putitem)
130131
- [Decrypt after UpdateItem](#decrypt-after-updateitem)
@@ -319,6 +320,12 @@ If there is a `Put` that refers to a `TableName` that refers to an [encrypted-ta
319320
the result [Encrypted DynamoDB Item](./encrypt-item.md#encrypted-dynamodb-item)
320321
calculated above.
321322

323+
### Decrypt after BatchWriteItem
324+
325+
If there are no UnprocessedItems, then the BatchWriteItemOutput MUST be returned unchanged.
326+
327+
Each item in UnprocessedItems MUST be replaced by its original plaintext value.
328+
322329
### Decrypt after GetItem
323330

324331
After a [GetItem](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_GetItem.html)

0 commit comments

Comments
 (0)
Please sign in to comment.