Skip to content

Commit a47d6f8

Browse files
ajewellamzajewellamz
committed
m
1 parent cfbc2ef commit a47d6f8

File tree

2 files changed

+156
-33
lines changed

2 files changed

+156
-33
lines changed

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

Lines changed: 75 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ module DynamoDBFilterExpr {
4444
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
4545
import Norm = DynamoDbNormalizeNumber
4646
import StandardLibrary.Sequence
47+
import SortedSets
4748

4849
// extract all the attributes from a filter expression
4950
// except for those which do not need the attribute's value
@@ -1746,6 +1747,71 @@ module DynamoDBFilterExpr {
17461747
names : Option<DDB.ExpressionAttributeNameMap>
17471748
)
17481749

1750+
// transform index into character
1751+
function method AsChar(x : uint32) : (output : char)
1752+
requires x < 26
1753+
ensures 'A' <= output <= 'Z'
1754+
{
1755+
'A' + x as char
1756+
}
1757+
1758+
// try different prefixes on `prev` until something is found that is not in `values`
1759+
method MakeNewName(prev : string, values : DDB.ExpressionAttributeValueMap) returns (output : Result<string, Error>)
1760+
requires 0 < |prev|
1761+
ensures output.Success? ==>
1762+
&& 0 < |output.value|
1763+
&& prev < output.value
1764+
&& output.value !in values
1765+
{
1766+
var ch : char := 'A';
1767+
for i : uint32 := 0 to 26 {
1768+
for j : uint32 := 0 to 26 {
1769+
var new_str := prev + [AsChar(i), AsChar(j)];
1770+
if new_str !in values {
1771+
return Success(new_str);
1772+
}
1773+
}
1774+
}
1775+
return Failure(E("Could not find new name"));
1776+
}
1777+
1778+
// Combine old_context and new_context, assuming that both came from Beaconize called with different bucket numbers
1779+
// this updates values and filterExpr, e.g
1780+
// old_context : filterExpr = "(X = :x)" values = {":x" := "aaa"}
1781+
// new_context : filterExpr = "X = :x" values = {":x" := "bbb"}
1782+
// output : filterExpr = "(X = :x) OR (X = :xAA)" values = {":x" := "aaa", "xAA" := "bbb"}
1783+
method AddContext(old_context : ExprContext, new_context : ExprContext) returns (output : Result<ExprContext, Error>)
1784+
{
1785+
if old_context.filterExpr.None? || new_context.filterExpr.None? || old_context.values.None? || new_context.values.None? || new_context.values == old_context.values {
1786+
return Success(old_context);
1787+
}
1788+
var result_values := old_context.values.value;
1789+
var result_filter := old_context.filterExpr.value;
1790+
var new_values := SortedSets.ComputeSetToSequence(new_context.values.value.Keys);
1791+
SequenceIsSafeBecauseItIsInMemory(new_values);
1792+
for i : uint64 := 0 to |new_values| as uint64
1793+
{
1794+
var key := new_values[i];
1795+
if key in old_context.values.value && new_context.values.value[key] != old_context.values.value[key] {
1796+
if old_context.keyExpr.Some? {
1797+
var keyInIndex := String.HasSubString(old_context.keyExpr.value, key);
1798+
if keyInIndex.Some? {
1799+
return Failure(E("The value " + key + " is referenced by both the KeyConditionExpression and the FilterExpression, which is not allowed."));
1800+
}
1801+
}
1802+
if 0 == |key| {
1803+
return Failure(E("Unexpected zero length key in ExpressionAttributeValueMap"));
1804+
}
1805+
var new_key :- MakeNewName(key, result_values);
1806+
result_values := result_values[new_key := new_context.values.value[key]];
1807+
var nFilter := String.SearchAndReplaceAll(new_context.filterExpr.value, key, new_key);
1808+
result_filter := result_filter + " OR (" + nFilter + ")";
1809+
}
1810+
}
1811+
return Success(old_context.(filterExpr := Some(result_filter), values := Some(result_values)));
1812+
}
1813+
1814+
// Call Beaconize, possibly multiple times if fewer queries than buckets
17491815
method DoBeaconize(
17501816
b : SI.BeaconVersion,
17511817
context : ExprContext,
@@ -1760,40 +1826,28 @@ module DynamoDBFilterExpr {
17601826
ensures b.ValidState()
17611827
modifies b.Modifies()
17621828
{
1763-
if queries.None? || queries.value == b.numBuckets || (b.numBuckets - bucket) <= queries.value {
1829+
if queries.None? || queries.value == b.numBuckets || (b.numBuckets - bucket) <= queries.value || context.filterExpr.None? {
17641830
output := Beaconize(b, context, keyId, bucket);
17651831
} else {
17661832
var curr_bucket : BucketNumber := bucket;
1767-
var exprs : seq<string> := [];
1768-
var tmpOutput : ExprContext := ExprContext(None, None, None, None);
1833+
var tmpOutput : ExprContext := context;
17691834
while curr_bucket < b.numBuckets
17701835
invariant b.ValidState()
17711836
{
1772-
tmpOutput :- Beaconize(b, context, keyId, curr_bucket);
1773-
if tmpOutput.filterExpr.Some? {
1774-
if tmpOutput.filterExpr.value !in exprs {
1775-
exprs := exprs + [tmpOutput.filterExpr.value];
1776-
}
1837+
var localOut :- Beaconize(b, context, keyId, curr_bucket);
1838+
if curr_bucket == bucket {
1839+
var old_filter := localOut.filterExpr.UnwrapOr("");
1840+
tmpOutput := localOut.(filterExpr := Some("(" + old_filter + ")"));
1841+
} else {
1842+
tmpOutput :- AddContext(tmpOutput, localOut);
17771843
}
17781844
if (b.numBuckets - curr_bucket) <= queries.value {
17791845
break;
17801846
} else {
17811847
curr_bucket := curr_bucket + queries.value;
17821848
}
17831849
}
1784-
if |exprs| < 2 {
1785-
return Success(tmpOutput);
1786-
} else {
1787-
var new_filter : string := "";
1788-
SequenceIsSafeBecauseItIsInMemory(exprs);
1789-
for i : uint64 := 0 to |exprs| as uint64 {
1790-
if i != 0 {
1791-
new_filter := new_filter + " OR ";
1792-
}
1793-
new_filter := new_filter + "(" + exprs[i] + ")";
1794-
}
1795-
return Success(tmpOutput.(filterExpr := Some(new_filter)));
1796-
}
1850+
return Success(tmpOutput);
17971851
}
17981852
}
17991853

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

Lines changed: 81 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -184,11 +184,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
184184
]
185185
}
186186

187-
method DoBucketQuery(client : DDB.IDynamoDBClient, bucket : nat, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, numBuckets : nat)
187+
method DoBucketQuery(client : DDB.IDynamoDBClient, bucket : nat, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, filtered : bool, numQueries : nat)
188188
requires counts.Length == 100
189189
requires client.ValidState()
190190
requires client.Modifies !! {counts}
191-
requires 0 < numBuckets
191+
requires 0 < numQueries
192192
ensures client.ValidState()
193193
modifies client.Modifies
194194
modifies counts
@@ -201,7 +201,12 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
201201
{
202202
var bucketNumber := DDB.AttributeValue.N(String.Base10Int2String(bucket));
203203
var values : DDB.ExpressionAttributeValueMap := query.ExpressionAttributeValues.UnwrapOr(map[]);
204-
var q := query.(ExclusiveStartKey := lastKey, ExpressionAttributeValues := Some(values[":aws_dbe_bucket" := bucketNumber]));
204+
values := values[":aws_dbe_bucket" := bucketNumber];
205+
if filtered {
206+
var bucketQueries := DDB.AttributeValue.N(String.Base10Int2String(numQueries));
207+
values := values[":aws_dbe_bucket_queries" := bucketQueries];
208+
}
209+
var q := query.(ExclusiveStartKey := lastKey, ExpressionAttributeValues := Some(values));
205210
var result :- expect client.Query(q);
206211
if result.Items.Some? {
207212
numReturned := numReturned + |result.Items.value|;
@@ -220,7 +225,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
220225
expect "PreferredBucket" in item;
221226
expect item["PreferredBucket"].N?;
222227
var stored_bucket :- expect StrToInt(item["PreferredBucket"].N);
223-
expect bucket == stored_bucket % numBuckets;
228+
expect bucket == stored_bucket % numQueries;
224229
}
225230
}
226231
}
@@ -236,15 +241,15 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
236241
}
237242
}
238243

239-
method TestBucketQueries(client : DDB.IDynamoDBClient, numBuckets : nat, q : DDB.QueryInput, queryName : string, custom : bool := false)
240-
requires 0 < numBuckets
244+
method TestBucketQueries(client : DDB.IDynamoDBClient, numQueries : nat, q : DDB.QueryInput, queryName : string, custom : bool := false, filtered : bool := false)
245+
requires 0 < numQueries
241246
requires client.ValidState()
242247
ensures client.ValidState()
243248
modifies client.Modifies
244249
{
245250
var counts: array<int> := new int[100](i => 0);
246-
for i := 0 to numBuckets {
247-
DoBucketQuery(client, i, q, counts, queryName, custom, numBuckets);
251+
for i := 0 to numQueries {
252+
DoBucketQuery(client, i, q, counts, queryName, custom, filtered, numQueries);
248253
}
249254
var wasBad : bool := false;
250255
for i := 0 to 100 {
@@ -279,6 +284,56 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
279284
ExpressionAttributeValues := Some(map[":attr1" := DDB.AttributeValue.S("AAAA"), ":attr5" := DDB.AttributeValue.S("EEEE")])
280285
)
281286
}
287+
function GetBucketQuery15F() : DDB.QueryInput
288+
{
289+
DDB.QueryInput(
290+
TableName := TableName,
291+
IndexName := Some("ATTR_INDEX1"),
292+
FilterExpression := Some("Attr5 = :attr5"),
293+
KeyConditionExpression := Some("Attr1 = :attr1"),
294+
ExpressionAttributeValues := Some(map[":attr1" := DDB.AttributeValue.S("AAAA"), ":attr5" := DDB.AttributeValue.S("EEEE")])
295+
)
296+
}
297+
function GetBucketQuery25F() : DDB.QueryInput
298+
{
299+
DDB.QueryInput(
300+
TableName := TableName,
301+
IndexName := Some("ATTR_INDEX2"),
302+
FilterExpression := Some("Attr5 = :attr5"),
303+
KeyConditionExpression := Some("Attr2 = :attr2"),
304+
ExpressionAttributeValues := Some(map[":attr2" := DDB.AttributeValue.S("BBBB"), ":attr5" := DDB.AttributeValue.S("EEEE")])
305+
)
306+
}
307+
function GetBucketQuery35F() : DDB.QueryInput
308+
{
309+
DDB.QueryInput(
310+
TableName := TableName,
311+
IndexName := Some("ATTR_INDEX3"),
312+
FilterExpression := Some("Attr5 = :attr5"),
313+
KeyConditionExpression := Some("Attr3 = :attr3"),
314+
ExpressionAttributeValues := Some(map[":attr3" := DDB.AttributeValue.S("CCCC"), ":attr5" := DDB.AttributeValue.S("EEEE")])
315+
)
316+
}
317+
function GetBucketQuery45F() : DDB.QueryInput
318+
{
319+
DDB.QueryInput(
320+
TableName := TableName,
321+
IndexName := Some("ATTR_INDEX4"),
322+
FilterExpression := Some("Attr5 = :attr5"),
323+
KeyConditionExpression := Some("Attr4 = :attr4"),
324+
ExpressionAttributeValues := Some(map[":attr4" := DDB.AttributeValue.S("DDDD"), ":attr5" := DDB.AttributeValue.S("EEEE")])
325+
)
326+
}
327+
function GetBucketQuery23() : DDB.QueryInput
328+
{
329+
DDB.QueryInput(
330+
TableName := TableName,
331+
IndexName := Some("ATTR_INDEX23"),
332+
FilterExpression := None,
333+
KeyConditionExpression := Some("Attr2 = :attr2 and Attr3 = :attr3"),
334+
ExpressionAttributeValues := Some(map[":attr2" := DDB.AttributeValue.S("BBBB"), ":attr3" := DDB.AttributeValue.S("CCCC")])
335+
)
336+
}
282337
function GetBucketQuery51() : DDB.QueryInput
283338
{
284339
DDB.QueryInput(
@@ -360,8 +415,15 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
360415
TestBucketQueries(rClient, 3, GetBucketQuery3(), "bucket query 3");
361416
TestBucketQueries(rClient, 2, GetBucketQuery2(), "bucket query 2");
362417
TestBucketQueries(rClient, 1, GetBucketQuery1(), "bucket query 1");
363-
TestBucketQueries(rClient, 5, GetBucketQuery15(), "bucket query 5");
364-
TestBucketQueries(rClient, 5, GetBucketQuery51(), "bucket query 5");
418+
419+
TestBucketQueries(rClient, 5, GetBucketQuery15(), "bucket query 15");
420+
TestBucketQueries(rClient, 5, GetBucketQuery51(), "bucket query 51");
421+
TestBucketQueries(rClient, 5, GetBucketQuery23(), "bucket query 23");
422+
423+
TestBucketQueries(rClient, 1, GetBucketQuery15F(), "bucket query 15F", false, true);
424+
TestBucketQueries(rClient, 2, GetBucketQuery25F(), "bucket query 25F", false, true);
425+
TestBucketQueries(rClient, 3, GetBucketQuery35F(), "bucket query 35F", false, true);
426+
TestBucketQueries(rClient, 4, GetBucketQuery45F(), "bucket query 45F", false, true);
365427
}
366428

367429
// As BucketTest1, but with custom bucket selector
@@ -388,8 +450,15 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
388450
TestBucketQueries(rClient, 3, GetBucketQuery3(), "bucket query 3", true);
389451
TestBucketQueries(rClient, 2, GetBucketQuery2(), "bucket query 2", true);
390452
TestBucketQueries(rClient, 1, GetBucketQuery1(), "bucket query 1", true);
391-
TestBucketQueries(rClient, 5, GetBucketQuery15(), "bucket query 5", true);
392-
TestBucketQueries(rClient, 5, GetBucketQuery51(), "bucket query 5", true);
453+
454+
TestBucketQueries(rClient, 5, GetBucketQuery15(), "bucket query 15", true);
455+
TestBucketQueries(rClient, 5, GetBucketQuery51(), "bucket query 51", true);
456+
TestBucketQueries(rClient, 5, GetBucketQuery23(), "bucket query 23", true);
457+
458+
TestBucketQueries(rClient, 1, GetBucketQuery15F(), "bucket query 15F", true, true);
459+
TestBucketQueries(rClient, 2, GetBucketQuery25F(), "bucket query 25F", true, true);
460+
TestBucketQueries(rClient, 3, GetBucketQuery35F(), "bucket query 35F", true, true);
461+
TestBucketQueries(rClient, 4, GetBucketQuery45F(), "bucket query 45F", true, true);
393462
}
394463

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

0 commit comments

Comments
 (0)