Skip to content

Commit bd5e532

Browse files
ajewellamzajewellamz
committed
m
1 parent 082a815 commit bd5e532

File tree

6 files changed

+95
-32
lines changed

6 files changed

+95
-32
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy‎

Lines changed: 62 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,14 @@ module DynamoDBSupport {
2323
import opened DynamoDbEncryptionUtil
2424
import opened DdbVirtualFields
2525
import opened SearchableEncryptionInfo
26+
import StandardLibrary.String
2627
import UTF8
2728
import SortedSets
2829
import Seq
2930
import Update = DynamoDbUpdateExpr
3031
import Filter = DynamoDBFilterExpr
3132
import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
33+
import NN = DynamoDbNormalizeNumber
3234

3335
// IsWritable examines an AttributeMap and fails if it is unsuitable for writing.
3436
// At the moment, this means that no attribute names starts with "aws_dbe_",
@@ -222,8 +224,51 @@ module DynamoDBSupport {
222224
Success(DoRemoveBeacons(item))
223225
}
224226

227+
// If filter expression is 'bucket=NN ...' return (..., NN)
228+
// else return (None, 0)
229+
function method ExtractBucketNumber(filterExpr : Option<string>) : (Option<string>, uint32)
230+
{
231+
if filterExpr.None? then
232+
(None, 0)
233+
else if "bucket=" < filterExpr.value then
234+
var nFilter := filterExpr.value[7..];
235+
var nDigits := NN.CountDigits(nFilter);
236+
if nDigits == 0 then
237+
(None, 0)
238+
else
239+
var num := NN.StrToInt(nFilter[..nDigits]);
240+
if num.Failure? then
241+
(None, 0)
242+
else if INT32_MAX_LIMIT < num.value then
243+
(None, 0)
244+
else
245+
(Some(nFilter[nDigits..]), num.value as uint32)
246+
else
247+
(None, 0)
248+
}
249+
250+
// Extract aws_dbe_bucket = NN from filterExpr and return bucket
251+
function method ExtractBucket(search : SearchableEncryptionInfo.BeaconVersion, filterExpr : Option<string>)
252+
: Result<(Option<string>, seq<uint8>), Error>
253+
{
254+
if search.numBuckets <= 1 then
255+
Success((filterExpr, []))
256+
else
257+
var (nFilter, bucket) := ExtractBucketNumber(filterExpr);
258+
if nFilter.Some? then
259+
:- Need(bucket < search.numBuckets, E("Bucket number specified in FilterExpression was " + String.Base10Int2String(bucket as int) + "but it must be less than the number of buckets " + String.Base10Int2String(search.numBuckets as int)));
260+
:- Need(bucket < 256, E("Bucket must be less than 256")); // unreachable
261+
if bucket == 0 then
262+
Success((nFilter, []))
263+
else
264+
Success((nFilter, [bucket as uint8]))
265+
else
266+
// TODO - if no encrypted beacons then OK
267+
Failure(E("When numberOfBuckets is greater than one, FilterExpression must start with 'aws_dbe_bucket = NN && '"))
268+
}
269+
225270
// Transform a QueryInput object for searchable encryption.
226-
method QueryInputForBeacons(search : Option<ValidSearchInfo>, actions : AttributeActions, req : DDB.QueryInput, bucket : Bytes)
271+
method QueryInputForBeacons(search : Option<ValidSearchInfo>, actions : AttributeActions, req : DDB.QueryInput)
227272
returns (output : Result<DDB.QueryInput, Error>)
228273
modifies if search.Some? then search.value.Modifies() else {}
229274
{
@@ -237,7 +282,10 @@ module DynamoDBSupport {
237282
return Success(req);
238283
} else {
239284
var keyId :- Filter.GetBeaconKeyId(search.value.curr(), req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
240-
var oldContext := Filter.ExprContext(req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
285+
286+
var foo :- ExtractBucket(search.value.curr(), req.FilterExpression);
287+
var (newFilter, bucket) := foo;
288+
var oldContext := Filter.ExprContext(req.KeyConditionExpression, newFilter, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
241289
var newContext :- Filter.Beaconize(search.value.curr(), oldContext, keyId, bucket);
242290
return Success(req.(
243291
KeyConditionExpression := newContext.keyExpr,
@@ -249,7 +297,7 @@ module DynamoDBSupport {
249297
}
250298

251299
// Transform a QueryOutput object for searchable encryption.
252-
method QueryOutputForBeacons(search : Option<ValidSearchInfo>, req : DDB.QueryInput, resp : DDB.QueryOutput, bucket : Bytes)
300+
method QueryOutputForBeacons(search : Option<ValidSearchInfo>, req : DDB.QueryInput, resp : DDB.QueryOutput)
253301
returns (output : Result<DDB.QueryOutput, Error>)
254302
requires resp.Items.Some?
255303
ensures output.Success? ==> output.value.Items.Some?
@@ -259,11 +307,13 @@ module DynamoDBSupport {
259307
var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), resp.Items.value);
260308
return Success(resp.(Items := Some(trimmedItems)));
261309
} else {
310+
var foo :- ExtractBucket(search.value.curr(), req.FilterExpression);
311+
var (newFilter, bucket) := foo;
262312
var newItems :- Filter.FilterResults(
263313
search.value.curr(),
264314
resp.Items.value,
265315
req.KeyConditionExpression,
266-
req.FilterExpression,
316+
newFilter,
267317
req.ExpressionAttributeNames,
268318
req.ExpressionAttributeValues,
269319
bucket);
@@ -295,7 +345,7 @@ module DynamoDBSupport {
295345
}
296346

297347
// Transform a ScanInput object for searchable encryption.
298-
method ScanInputForBeacons(search : Option<ValidSearchInfo>, actions : AttributeActions, req : DDB.ScanInput, bucket : Bytes)
348+
method ScanInputForBeacons(search : Option<ValidSearchInfo>, actions : AttributeActions, req : DDB.ScanInput)
299349
returns (output : Result<DDB.ScanInput, Error>)
300350
modifies if search.Some? then search.value.Modifies() else {}
301351
{
@@ -309,7 +359,9 @@ module DynamoDBSupport {
309359
return Success(req);
310360
} else {
311361
var keyId :- Filter.GetBeaconKeyId(search.value.curr(), None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
312-
var context := Filter.ExprContext(None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
362+
var foo :- ExtractBucket(search.value.curr(), req.FilterExpression);
363+
var (newFilter, bucket) := foo;
364+
var context := Filter.ExprContext(None, newFilter, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
313365
var newContext :- Filter.Beaconize(search.value.curr(), context, keyId, bucket);
314366
return Success(req.(
315367
FilterExpression := newContext.filterExpr,
@@ -320,7 +372,7 @@ module DynamoDBSupport {
320372
}
321373

322374
// Transform a ScanOutput object for searchable encryption.
323-
method ScanOutputForBeacons(search : Option<ValidSearchInfo>, req : DDB.ScanInput, resp : DDB.ScanOutput, bucket : Bytes)
375+
method ScanOutputForBeacons(search : Option<ValidSearchInfo>, req : DDB.ScanInput, resp : DDB.ScanOutput)
324376
returns (ret : Result<DDB.ScanOutput, Error>)
325377
requires resp.Items.Some?
326378
ensures ret.Success? ==> ret.value.Items.Some?
@@ -330,11 +382,13 @@ module DynamoDBSupport {
330382
var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), resp.Items.value);
331383
return Success(resp.(Items := Some(trimmedItems)));
332384
} else {
385+
var foo :- ExtractBucket(search.value.curr(), req.FilterExpression);
386+
var (newFilter, bucket) := foo;
333387
var newItems :- Filter.FilterResults(
334388
search.value.curr(),
335389
resp.Items.value,
336390
None,
337-
req.FilterExpression,
391+
newFilter,
338392
req.ExpressionAttributeNames,
339393
req.ExpressionAttributeValues,
340394
bucket);

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy‎

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1794,21 +1794,35 @@ module DynamoDBFilterExpr {
17941794
}
17951795

17961796
// return an error if any encrypted field exists in the query
1797-
method TestParsedExpr(
1797+
method UsesEncryptedField(
17981798
expr : seq<Token>,
17991799
encrypted : set<string>,
18001800
names : Option<DDB.ExpressionAttributeNameMap>
18011801
)
1802-
returns (output : Outcome<Error>)
1802+
returns (output : Option<string>)
18031803
{
18041804
for i := 0 to |expr| {
18051805
if expr[i].Attr? {
18061806
var name := GetAttrName(expr[i], names);
18071807
if name in encrypted {
1808-
return Fail(E("Query is using encrypted field : " + name + "."));
1808+
return Some(name);
18091809
}
18101810
}
18111811
}
1812+
return None;
1813+
}
1814+
1815+
method TestParsedExpr(
1816+
expr : seq<Token>,
1817+
encrypted : set<string>,
1818+
names : Option<DDB.ExpressionAttributeNameMap>
1819+
)
1820+
returns (output : Outcome<Error>)
1821+
{
1822+
var hasEncField := UsesEncryptedField(expr, encrypted, names);
1823+
if hasEncField.Some? {
1824+
return Fail(E("Query is using encrypted field : " + hasEncField.value + "."));
1825+
}
18121826
return Pass;
18131827
}
18141828

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ module TestDDBSupport {
5151
ExpressionAttributeValues := Some(expressionAttributeValues),
5252
KeyConditionExpression := Some("TheKeyField = :value")
5353
);
54-
var result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []);
54+
var result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput);
5555

5656
// Verify Success with branch key id plus beacon
5757
expressionAttributeValues := map[
@@ -63,15 +63,15 @@ module TestDDBSupport {
6363
ExpressionAttributeValues := Some(expressionAttributeValues),
6464
KeyConditionExpression := Some("TheKeyField = :value AND std2 = :other")
6565
);
66-
result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []);
66+
result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput);
6767

6868
// Verify Failure with beacon but no branch key id
6969
queryInput := DDB.QueryInput (
7070
TableName := "foo",
7171
ExpressionAttributeValues := Some(expressionAttributeValues),
7272
KeyConditionExpression := Some("std2 = :other")
7373
);
74-
var result2 := QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []);
74+
var result2 := QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput);
7575
expect result2 == Failure(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.DynamoDbEncryptionException(
7676
message := "Need KeyId because of beacon std2 but no KeyId found in query"));
7777

@@ -86,6 +86,6 @@ module TestDDBSupport {
8686
ExpressionAttributeValues := Some(expressionAttributeValues),
8787
KeyConditionExpression := Some("#keyfield = :value AND #beacon = :other")
8888
);
89-
result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []);
89+
result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput);
9090
}
9191
}

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

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -185,50 +185,50 @@ module DynamoDbMiddlewareSupport {
185185
}
186186

187187
// Transform a QueryInput object for searchable encryption.
188-
method {:opaque} QueryInputForBeacons(config : ValidTableConfig, req : DDB.QueryInput, bucket : seq<uint8>)
188+
method {:opaque} QueryInputForBeacons(config : ValidTableConfig, req : DDB.QueryInput)
189189
returns (output : Result<DDB.QueryInput, Error>)
190190
requires OneSearchValidState(config)
191191
ensures OneSearchValidState(config)
192192
modifies OneSearchModifies(config)
193193
{
194-
var ret := BS.QueryInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req, bucket);
194+
var ret := BS.QueryInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req);
195195
return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
196196
}
197197

198198
// Transform a QueryOutput object for searchable encryption.
199-
method QueryOutputForBeacons(config : ValidTableConfig, req : DDB.QueryInput, resp : DDB.QueryOutput, bucket : seq<uint8>)
199+
method QueryOutputForBeacons(config : ValidTableConfig, req : DDB.QueryInput, resp : DDB.QueryOutput)
200200
returns (output : Result<DDB.QueryOutput, Error>)
201201
requires resp.Items.Some?
202202
ensures output.Success? ==> output.value.Items.Some?
203203
requires OneSearchValidState(config)
204204
ensures OneSearchValidState(config)
205205
modifies OneSearchModifies(config)
206206
{
207-
var ret := BS.QueryOutputForBeacons(config.search, req, resp, bucket);
207+
var ret := BS.QueryOutputForBeacons(config.search, req, resp);
208208
return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
209209
}
210210

211211
// Transform a ScanInput object for searchable encryption.
212-
method ScanInputForBeacons(config : ValidTableConfig, req : DDB.ScanInput, bucket : seq<uint8>)
212+
method ScanInputForBeacons(config : ValidTableConfig, req : DDB.ScanInput)
213213
returns (output : Result<DDB.ScanInput, Error>)
214214
requires OneSearchValidState(config)
215215
ensures OneSearchValidState(config)
216216
modifies OneSearchModifies(config)
217217
{
218-
var ret := BS.ScanInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req, bucket);
218+
var ret := BS.ScanInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req);
219219
return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
220220
}
221221

222222
// Transform a ScanOutput object for searchable encryption.
223-
method ScanOutputForBeacons(config : ValidTableConfig, req : DDB.ScanInput, resp : DDB.ScanOutput, bucket : seq<uint8>)
223+
method ScanOutputForBeacons(config : ValidTableConfig, req : DDB.ScanInput, resp : DDB.ScanOutput)
224224
returns (output : Result<DDB.ScanOutput, Error>)
225225
requires resp.Items.Some?
226226
ensures output.Success? ==> output.value.Items.Some?
227227
requires OneSearchValidState(config)
228228
ensures OneSearchValidState(config)
229229
modifies OneSearchModifies(config)
230230
{
231-
var ret := BS.ScanOutputForBeacons(config.search, req, resp, bucket);
231+
var ret := BS.ScanOutputForBeacons(config.search, req, resp);
232232
return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
233233
}
234234

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

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -44,9 +44,7 @@ module QueryTransform {
4444
:- Need(NoMap(input.sdkInput.QueryFilter), E("Legacy parameter 'QueryFilter' not supported in Query with Encryption"));
4545
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in Query with Encryption"));
4646
var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
47-
48-
var bucket := []; // TODO
49-
var finalResult :- QueryInputForBeacons(tableConfig, input.sdkInput, bucket);
47+
var finalResult :- QueryInputForBeacons(tableConfig, input.sdkInput);
5048
return Success(QueryInputTransformOutput(transformedInput := finalResult));
5149
}
5250
}
@@ -106,8 +104,7 @@ module QueryTransform {
106104
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-query
107105
//# The resulting decrypted response MUST be [filtered](ddb-support.md#queryoutputforbeacons) from the result.
108106
var decryptedOutput := input.sdkOutput.(Items := Some(decryptedItems));
109-
var bucket := []; // Not used
110-
var finalResult :- QueryOutputForBeacons(tableConfig, input.originalInput, decryptedOutput, bucket);
107+
var finalResult :- QueryOutputForBeacons(tableConfig, input.originalInput, decryptedOutput);
111108
return Success(QueryOutputTransformOutput(transformedOutput := finalResult));
112109
}
113110
}

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

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,7 @@ module ScanTransform {
4343
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
4444
var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
4545

46-
var bucket := []; // TODO
47-
var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput, bucket);
46+
var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput);
4847
return Success(ScanInputTransformOutput(transformedInput := finalResult));
4948
}
5049
}
@@ -104,8 +103,7 @@ module ScanTransform {
104103
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-scan
105104
//# The resulting decrypted response MUST be [filtered](ddb-support.md#scanoutputforbeacons) from the result.
106105
var decryptedOutput := input.sdkOutput.(Items := Some(decryptedItems));
107-
var bucket := []; // Not used
108-
var finalResult :- ScanOutputForBeacons(tableConfig, input.originalInput, decryptedOutput, bucket);
106+
var finalResult :- ScanOutputForBeacons(tableConfig, input.originalInput, decryptedOutput);
109107
return Success(ScanOutputTransformOutput(transformedOutput := finalResult));
110108
}
111109
}

0 commit comments

Comments
 (0)