Skip to content

Commit 91f67cf

Browse files
ajewellamzajewellamz
committed
m
1 parent 9e4115a commit 91f67cf

File tree

4 files changed

+32
-78
lines changed

4 files changed

+32
-78
lines changed

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

Lines changed: 11 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -224,7 +224,6 @@ module DynamoDBSupport {
224224
Success(DoRemoveBeacons(item))
225225
}
226226
const BucketName : string := ":aws_dbe_bucket"
227-
const BucketQueriesName : string := ":aws_dbe_bucket_queries"
228227

229228
function method GetNumber(val : DDB.AttributeValue, name : string) : Result<uint32, Error>
230229
{
@@ -236,16 +235,14 @@ module DynamoDBSupport {
236235
Failure(E("Value of " + name + " is not numeric (i.e. 'N')"))
237236
}
238237

239-
// Unlike Query, Scan must not specify BucketName nor BucketQueriesName
238+
// Unlike Query, Scan must not specify BucketName
240239
function method TestBucketForScan(names : Option<DDB.ExpressionAttributeValueMap>)
241240
: Result<bool, Error>
242241
{
243242
if names.None? then
244243
Success(true)
245244
else if BucketName in names.value then
246245
Failure(E("A value for " + BucketName + " must not be specified for Scan operations."))
247-
else if BucketQueriesName in names.value then
248-
Failure(E("A value for " + BucketQueriesName + " must not be specified for Scan operations."))
249246
else
250247
Success(true)
251248
}
@@ -267,60 +264,31 @@ module DynamoDBSupport {
267264
Success((None, None))
268265
}
269266

270-
function method ExtractBucketQueries(names : Option<DDB.ExpressionAttributeValueMap>)
271-
: Result<(Option<DDB.ExpressionAttributeValueMap>, Option<uint32>), Error>
272-
{
273-
if names.None? then
274-
Success((None, None))
275-
else if BucketQueriesName in names.value then
276-
var val :- GetNumber(names.value[BucketQueriesName], BucketQueriesName);
277-
if |names.value| == 1 then
278-
Success((None, Some(val)))
279-
else
280-
Success((Some(names.value - {BucketQueriesName}), Some(val)))
281-
else
282-
Success((None, None))
283-
}
284-
285267
// Extract aws_dbe_bucket = NN from filterExpr and return bucket
286268
method ExtractBucket(search : SearchableEncryptionInfo.BeaconVersion, keyExpr : Option<string>, filterExpr : Option<string>, names : Option<DDB.ExpressionAttributeNameMap>, values : Option<DDB.ExpressionAttributeValueMap>, actions : AttributeActions)
287-
returns (output : Result<(Option<DDB.ExpressionAttributeValueMap>, BucketNumber, Option<BucketCount>), Error>)
269+
returns (output : Result<(Option<DDB.ExpressionAttributeValueMap>, BucketNumber), Error>)
288270
ensures output.Success? ==> output.value.1 < search.numBuckets
289-
ensures output.Success? && output.value.2.Some? ==> output.value.1 < output.value.2.value <= search.numBuckets
290271
{
291272
if search.numBuckets <= 1 {
292-
:- Need(values.None? || BucketName !in values.value, E(""));
293-
:- Need(values.None? || BucketQueriesName !in values.value, E(""));
294-
return Success((values, 0, None));
273+
:- Need(values.None? || BucketName !in values.value, E("If no buckets are configured, do not specify " + BucketName));
274+
return Success((values, 0));
295275
}
296276

297277
var foo :- ExtractBucketNumber(values);
298278
var (values2, bucket) := foo;
299279
if bucket.Some? {
300280
:- Need(bucket.value < search.numBuckets as uint32, E(BucketName + " specified in FilterExpression was " + String.Base10Int2String(bucket.value as int) + " must be less than the number of buckets: " + String.Base10Int2String(search.numBuckets as int)));
301281
var nBucket := (bucket.value as nat) as BucketNumber;
302-
303-
var bar :- ExtractBucketQueries(values2);
304-
var (values3, queries) := bar;
305-
if queries.Some? {
306-
:- Need(0 < queries.value <= search.numBuckets as uint32, E(BucketQueriesName + " specified in FilterExpression was " + String.Base10Int2String(queries.value as int) + " must be greater than zero and less than or equal to the number of buckets: " + String.Base10Int2String(search.numBuckets as int)));
307-
:- Need(bucket.value < queries.value, E(BucketName + " value of " + String.Base10Int2String(bucket.value as int) + " should have been less than the " + BucketQueriesName + " value of " + String.Base10Int2String(queries.value as int)));
308-
var nQueries := (queries.value as nat) as BucketCount;
309-
return Success((values3, nBucket, Some(nQueries)));
310-
} else {
311-
return Success((values2, nBucket, None));
312-
}
282+
return Success((values2, nBucket));
313283
}
314284

315-
:- Need(values.None? || BucketQueriesName !in values.value, E(""));
316-
317285
// No bucket specified is OK if no encrypted fields are searched
318286
var filterHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(filterExpr), actions, names);
319287
var keyHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(keyExpr), actions, names);
320288
if keyHasEncField.Some? || filterHasEncField.Some? {
321-
return Failure(E("When numberOfBuckets is greater than one, FilterExpression must start with 'aws_dbe_bucket = NN && '"));
289+
return Failure(E("When numberOfBuckets is greater than one, XXXValues must contain " + BucketName));
322290
} else {
323-
return Success((values, 0, None));
291+
return Success((values, 0));
324292
}
325293
}
326294

@@ -341,18 +309,13 @@ module DynamoDBSupport {
341309
var keyId :- Filter.GetBeaconKeyId(search.value.curr(), req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
342310

343311
var foo :- ExtractBucket(search.value.curr(), req.FilterExpression, req.KeyConditionExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues, actions);
344-
var (newValues, bucket, bucket_queries) := foo;
312+
var (newValues, bucket) := foo;
345313
var numQueries :- Filter.GetNumQueries(actions, req.KeyConditionExpression, req.ExpressionAttributeNames, search.value.curr());
346-
if numQueries < bucket {
314+
if numQueries <= bucket {
347315
return Failure(E("Bucket number was " + String.Base10Int2String(bucket as int) + " but should have been less than number of queries : " + String.Base10Int2String(numQueries as int)));
348316
}
349-
if bucket_queries.Some? {
350-
if numQueries != bucket_queries.value {
351-
return Failure(E("Number of queries was " + String.Base10Int2String(numQueries as int) + " but should have been " + String.Base10Int2String(bucket_queries.value as int)));
352-
}
353-
}
354317
var oldContext := Filter.ExprContext(req.KeyConditionExpression, req.FilterExpression, newValues, req.ExpressionAttributeNames);
355-
var newContext :- Filter.DoBeaconize(search.value.curr(), oldContext, keyId, bucket, bucket_queries);
318+
var newContext :- Filter.DoBeaconize(search.value.curr(), oldContext, keyId, bucket, numQueries);
356319
return Success(req.(
357320
KeyConditionExpression := newContext.keyExpr,
358321
FilterExpression := newContext.filterExpr,
@@ -424,9 +387,7 @@ module DynamoDBSupport {
424387
var keyId :- Filter.GetBeaconKeyId(search.value.curr(), None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
425388
var _ :- TestBucketForScan(req.ExpressionAttributeValues);
426389
var context := Filter.ExprContext(None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames);
427-
// For Scan, we always treat it as {:aws_dbe_bucket := 0, :aws_dbe_bucket_queries := 1}
428-
var numQueries := if search.value.curr().numBuckets == 1 then None else Some(1);
429-
var newContext :- Filter.DoBeaconize(search.value.curr(), context, keyId, 0, Some(1));
390+
var newContext :- Filter.DoBeaconize(search.value.curr(), context, keyId, 0, 1);
430391
return Success(req.(
431392
FilterExpression := newContext.filterExpr,
432393
ExpressionAttributeNames := newContext.names,

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1833,16 +1833,16 @@ module DynamoDBFilterExpr {
18331833
context : ExprContext,
18341834
keyId : MaybeKeyId,
18351835
bucket : BucketNumber,
1836-
queries : Option<BucketCount>
1836+
queries : BucketCount
18371837
)
18381838
returns (output : Result<ExprContext, Error>)
18391839
requires b.ValidState()
18401840
requires bucket < b.numBuckets
1841-
requires queries.Some? ==> bucket < queries.value <= b.numBuckets
1841+
requires bucket < queries <= b.numBuckets
18421842
ensures b.ValidState()
18431843
modifies b.Modifies()
18441844
{
1845-
if queries.None? || queries.value == b.numBuckets || (b.numBuckets - bucket) <= queries.value || context.filterExpr.None? {
1845+
if queries == b.numBuckets || (b.numBuckets - bucket) <= queries || context.filterExpr.None? {
18461846
output := Beaconize(b, context, keyId, bucket);
18471847
} else {
18481848
var curr_bucket : BucketNumber := bucket;
@@ -1857,10 +1857,10 @@ module DynamoDBFilterExpr {
18571857
} else {
18581858
tmpOutput :- AddContext(tmpOutput, localOut);
18591859
}
1860-
if (b.numBuckets - curr_bucket) <= queries.value {
1860+
if (b.numBuckets - curr_bucket) <= queries {
18611861
break;
18621862
} else {
1863-
curr_bucket := curr_bucket + queries.value;
1863+
curr_bucket := curr_bucket + queries;
18641864
}
18651865
}
18661866
return Success(tmpOutput);

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ module TestBaseBeacon {
2727
var primitives :- expect Primitives.AtomicPrimitives();
2828

2929
var bb := BeaconBase(client := primitives, name := "foo", beaconName := "aws_dbe_b_foo");
30-
var b := StandardBeacon(bb, 8, TermLocMap("foo"), false, false, None, 0);
30+
var b := StandardBeacon(bb, 8, TermLocMap("foo"), false, false, None, 1);
3131
var bytes :- expect bb.getHmac([1,2,3], key := [1,2]);
3232
expect bytes == [0x27, 0x93, 0x93, 0x8b, 0x26, 0xe9, 0x52, 0x7e];
3333
var str :- expect b.hash([1,2,3], key := [1,2], bucket := 0);

‎TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

Lines changed: 15 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
185185
]
186186
}
187187

188-
method DoBucketQuery(client : DDB.IDynamoDBClient, bucket : nat, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, filtered : bool, numQueries : nat)
188+
method DoBucketQuery(client : DDB.IDynamoDBClient, bucket : nat, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, numQueries : nat)
189189
requires counts.Length == 100
190190
requires client.ValidState()
191191
requires client.Modifies !! {counts}
@@ -203,10 +203,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
203203
var bucketNumber := DDB.AttributeValue.N(String.Base10Int2String(bucket));
204204
var values : DDB.ExpressionAttributeValueMap := query.ExpressionAttributeValues.UnwrapOr(map[]);
205205
values := values[":aws_dbe_bucket" := bucketNumber];
206-
if filtered {
207-
var bucketQueries := DDB.AttributeValue.N(String.Base10Int2String(numQueries));
208-
values := values[":aws_dbe_bucket_queries" := bucketQueries];
209-
}
210206
var q := query.(ExclusiveStartKey := lastKey, ExpressionAttributeValues := Some(values));
211207
var result :- expect client.Query(q);
212208
if result.Items.Some? {
@@ -242,7 +238,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
242238
}
243239
}
244240

245-
method TestBucketQueryFailure(client : DDB.IDynamoDBClient, bucket : nat, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, filtered : bool, numQueries : nat)
241+
method TestBucketQueryFailure(client : DDB.IDynamoDBClient, bucket : nat, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, numQueries : nat)
246242
requires counts.Length == 100
247243
requires client.ValidState()
248244
requires client.Modifies !! {counts}
@@ -254,28 +250,24 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
254250
var bucketNumber := DDB.AttributeValue.N(String.Base10Int2String(bucket));
255251
var values : DDB.ExpressionAttributeValueMap := query.ExpressionAttributeValues.UnwrapOr(map[]);
256252
values := values[":aws_dbe_bucket" := bucketNumber];
257-
if filtered {
258-
var bucketQueries := DDB.AttributeValue.N(String.Base10Int2String(numQueries));
259-
values := values[":aws_dbe_bucket_queries" := bucketQueries];
260-
}
261253
var q := query.(ExpressionAttributeValues := Some(values));
262254
var result := client.Query(q);
263-
// expect result.Failure?;
255+
expect result.Failure?;
264256
}
265257

266258

267-
method TestBucketQueries(client : DDB.IDynamoDBClient, numQueries : nat, q : DDB.QueryInput, queryName : string, custom : bool := false, filtered : bool := false)
259+
method TestBucketQueries(client : DDB.IDynamoDBClient, numQueries : nat, q : DDB.QueryInput, queryName : string, custom : bool := false)
268260
requires 0 < numQueries <= 5
269261
requires client.ValidState()
270262
ensures client.ValidState()
271263
modifies client.Modifies
272264
{
273265
var counts: array<int> := new int[100](i => 0);
274266
for i := 0 to numQueries {
275-
DoBucketQuery(client, i, q, counts, queryName, custom, filtered, numQueries);
267+
DoBucketQuery(client, i, q, counts, queryName, custom, numQueries);
276268
}
277269
for i := numQueries to 5 {
278-
TestBucketQueryFailure(client, i, q, counts, queryName, custom, filtered, numQueries);
270+
TestBucketQueryFailure(client, i, q, counts, queryName, custom, numQueries);
279271
}
280272

281273
var wasBad : bool := false;
@@ -414,6 +406,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
414406

415407
method BucketTests()
416408
{
409+
print "BucketTests\n";
417410
BucketTest1();
418411
BucketTest2();
419412
}
@@ -447,10 +440,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
447440
TestBucketQueries(rClient, 5, GetBucketQuery51(), "bucket query 51");
448441
TestBucketQueries(rClient, 5, GetBucketQuery23(), "bucket query 23");
449442

450-
TestBucketQueries(rClient, 1, GetBucketQuery15F(), "bucket query 15F", false, true);
451-
TestBucketQueries(rClient, 2, GetBucketQuery25F(), "bucket query 25F", false, true);
452-
TestBucketQueries(rClient, 3, GetBucketQuery35F(), "bucket query 35F", false, true);
453-
TestBucketQueries(rClient, 4, GetBucketQuery45F(), "bucket query 45F", false, true);
443+
TestBucketQueries(rClient, 1, GetBucketQuery15F(), "bucket query 15F", false);
444+
TestBucketQueries(rClient, 2, GetBucketQuery25F(), "bucket query 25F", false);
445+
TestBucketQueries(rClient, 3, GetBucketQuery35F(), "bucket query 35F", false);
446+
TestBucketQueries(rClient, 4, GetBucketQuery45F(), "bucket query 45F", false);
454447
}
455448

456449
// As BucketTest1, but with custom bucket selector
@@ -482,10 +475,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
482475
TestBucketQueries(rClient, 5, GetBucketQuery51(), "bucket query 51a", true);
483476
TestBucketQueries(rClient, 5, GetBucketQuery23(), "bucket query 23a", true);
484477

485-
TestBucketQueries(rClient, 1, GetBucketQuery15F(), "bucket query 15Fa", true, true);
486-
TestBucketQueries(rClient, 2, GetBucketQuery25F(), "bucket query 25Fa", true, true);
487-
TestBucketQueries(rClient, 3, GetBucketQuery35F(), "bucket query 35Fa", true, true);
488-
TestBucketQueries(rClient, 4, GetBucketQuery45F(), "bucket query 45Fa", true, true);
478+
TestBucketQueries(rClient, 1, GetBucketQuery15F(), "bucket query 15Fa", true);
479+
TestBucketQueries(rClient, 2, GetBucketQuery25F(), "bucket query 25Fa", true);
480+
TestBucketQueries(rClient, 3, GetBucketQuery35F(), "bucket query 35Fa", true);
481+
TestBucketQueries(rClient, 4, GetBucketQuery45F(), "bucket query 45Fa", true);
489482
}
490483

491484
function NewOrderRecord(i : nat, str : string) : Record

0 commit comments

Comments
 (0)