Skip to content

Commit 468682b

Browse files
ajewellamzajewellamz
committed
m
1 parent 046489a commit 468682b

File tree

2 files changed

+75
-62
lines changed

2 files changed

+75
-62
lines changed

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

Lines changed: 47 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1832,51 +1832,42 @@ module DynamoDBFilterExpr {
18321832
// old_context : filterExpr = "(X = :x)" values = {":x" := "aaa"}
18331833
// new_context : filterExpr = "X = :x" values = {":x" := "bbb"}
18341834
// output : filterExpr = "(X = :x) OR (X = :xAA)" values = {":x" := "aaa", "xAA" := "bbb"}
1835-
method AddContext(old_context : ExprContext, new_context : ExprContext) returns (output : Result<ExprContext, Error>)
1835+
method AddContext(old_values : DDB.ExpressionAttributeValueMap, new_filter : string, new_values : DDB.ExpressionAttributeValueMap)
1836+
returns (output : Result<(string, DDB.ExpressionAttributeValueMap), Error>)
18361837
{
1837-
if old_context.filterExpr.None? || new_context.filterExpr.None? || old_context.values.None? || new_context.values.None? || new_context.values == old_context.values {
1838-
return Success(old_context);
1839-
}
1840-
var new_values := SortedSets.ComputeSetToSequence(new_context.values.value.Keys);
1841-
SequenceIsSafeBecauseItIsInMemory(new_values);
1838+
var new_value_keys := SortedSets.ComputeSetToSequence(new_values.Keys);
1839+
SequenceIsSafeBecauseItIsInMemory(new_value_keys);
18421840
var allUnchanged := true;
1843-
for i : uint64 := 0 to |new_values| as uint64
1841+
for i : uint64 := 0 to |new_value_keys| as uint64
18441842
{
1845-
if new_values[i] !in old_context.values.value {
1843+
if new_value_keys[i] !in old_values {
18461844
allUnchanged := false;
18471845
break;
18481846
}
1849-
if new_context.values.value[new_values[i]] != old_context.values.value[new_values[i]] {
1847+
if new_values[new_value_keys[i]] != old_values[new_value_keys[i]] {
18501848
allUnchanged := false;
18511849
break;
18521850
}
18531851
}
18541852
if allUnchanged {
1855-
return Success(old_context);
1853+
return Success((new_filter, old_values));
18561854
}
18571855

1858-
var result_values := old_context.values.value;
1859-
var result_filter := new_context.filterExpr.value;
1860-
for i : uint64 := 0 to |new_values| as uint64
1856+
var result_values := old_values;
1857+
var result_filter := new_filter;
1858+
for i : uint64 := 0 to |new_value_keys| as uint64
18611859
{
1862-
var key := new_values[i];
1863-
if key in old_context.values.value && new_context.values.value[key] != old_context.values.value[key] {
1864-
if old_context.keyExpr.Some? {
1865-
var keyInIndex := String.HasSubString(old_context.keyExpr.value, key);
1866-
if keyInIndex.Some? {
1867-
return Failure(E("The value " + key + " is referenced by both the KeyConditionExpression and the FilterExpression, which is not allowed."));
1868-
}
1869-
}
1860+
var key := new_value_keys[i];
1861+
if key in old_values && new_values[key] != old_values[key] {
18701862
if 0 == |key| {
18711863
return Failure(E("Unexpected zero length key in ExpressionAttributeValueMap"));
18721864
}
1873-
var new_key :- MakeNewName(key, result_values, new_context.values.value[key]);
1874-
result_values := result_values[new_key := new_context.values.value[key]];
1875-
result_filter := String.SearchAndReplaceAll(result_filter, key, new_key);
1865+
var new_key :- MakeNewName(key, result_values, new_values[key]);
1866+
result_values := result_values[new_key := new_values[key]];
1867+
result_filter := String.SearchAndReplaceAllNot(result_filter, key, new_key, String.AlphaNumericUnder);
18761868
}
18771869
}
1878-
result_filter := old_context.filterExpr.value + " OR (" + result_filter + ")";
1879-
return Success(old_context.(filterExpr := Some(result_filter), values := Some(result_values)));
1870+
return Success((result_filter, result_values));
18801871
}
18811872

18821873
// Call Beaconize, possibly multiple times if fewer queries than buckets
@@ -1894,28 +1885,52 @@ module DynamoDBFilterExpr {
18941885
ensures b.ValidState()
18951886
modifies b.Modifies()
18961887
{
1897-
if queries == b.numBuckets || (b.numBuckets - bucket) <= queries || context.filterExpr.None? {
1888+
if queries == b.numBuckets || (b.numBuckets - bucket) <= queries || context.filterExpr.None? || context.values.None? {
18981889
output := Beaconize(b, context, keyId, bucket);
18991890
} else {
19001891
var curr_bucket : BucketNumber := bucket;
1901-
var tmpOutput : ExprContext := context;
1892+
var exprs : seq<string> := [];
1893+
var values : DDB.ExpressionAttributeValueMap := map[];
1894+
var keyExpr : Option<DDB.KeyExpression> := None;
1895+
var names : Option<DDB.ExpressionAttributeNameMap> := None;
1896+
19021897
while curr_bucket < b.numBuckets
19031898
invariant b.ValidState()
1899+
invariant curr_bucket == bucket || 0 < |exprs|
19041900
{
19051901
var localOut :- Beaconize(b, context, keyId, curr_bucket);
19061902
if curr_bucket == bucket {
1907-
var old_filter := localOut.filterExpr.UnwrapOr("");
1908-
tmpOutput := localOut.(filterExpr := Some("(" + old_filter + ")"));
1903+
exprs := [localOut.filterExpr.UnwrapOr("")];
1904+
values := localOut.values.UnwrapOr(map[]);
1905+
keyExpr := localOut.keyExpr;
1906+
names := localOut.names;
19091907
} else {
1910-
tmpOutput :- AddContext(tmpOutput, localOut);
1908+
var tmpOutput :- AddContext(values, localOut.filterExpr.UnwrapOr(""), localOut.values.UnwrapOr(map[]));
1909+
var (expr, value) := tmpOutput;
1910+
if expr !in exprs {
1911+
exprs := exprs + [expr];
1912+
}
1913+
values := value;
19111914
}
19121915
if (b.numBuckets - curr_bucket) <= queries {
19131916
break;
19141917
} else {
19151918
curr_bucket := curr_bucket + queries;
19161919
}
19171920
}
1918-
return Success(tmpOutput);
1921+
var result_filter : string;
1922+
SequenceIsSafeBecauseItIsInMemory(exprs);
1923+
var exprs_size : uint64 := |exprs| as uint64;
1924+
assert 0 < exprs_size;
1925+
if exprs_size == 1 {
1926+
result_filter := exprs[0];
1927+
} else {
1928+
result_filter := "(" + exprs[0] + ")";
1929+
for i := 1 to exprs_size {
1930+
result_filter := result_filter + " OR (" + exprs[i] + ")";
1931+
}
1932+
}
1933+
return Success(ExprContext(keyExpr, Some(result_filter), Some(values), names));
19191934
}
19201935
}
19211936

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

Lines changed: 28 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -633,32 +633,38 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
633633
method BucketTests()
634634
{
635635
print "BucketTests\n";
636-
// BucketTest3(); Not doing anything yet
636+
BucketTest3();
637637
BucketTest1();
638638
BucketTest2();
639639
}
640640

641-
// method PrintScanTrans(trans : DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient, q : DDB.ScanInput)
642-
// requires trans.ValidState()
643-
// ensures trans.ValidState()
644-
// modifies trans.Modifies
645-
// {
646-
// var input := Trans.ScanInputTransformInput(sdkInput := q);
647-
// var res :- expect trans.ScanInputTransform(input);
648-
// print "\nScanInputTransform\n", q, "\n", res.transformedInput, "\n";
649-
// }
650-
651-
// method BucketTest3()
652-
// {
653-
// expect "bucket_encrypt" in largeEncryptionConfigs;
654-
// var config := largeEncryptionConfigs["bucket_encrypt"];
655-
// var configs := Types.DynamoDbTablesEncryptionConfig (tableEncryptionConfigs := map[TableName := config.config]);
656-
// assume {:axiom} false;
657-
// var trans :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(configs);
658-
659-
// PrintScanTrans(trans, GetBucketScan2("Attr2", "Attr3"));
660-
// PrintScanTrans(trans, GetBucketScan2("Attr3", "Attr2"));
661-
// }
641+
method TestScanTrans(trans : DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient, q : DDB.ScanInput, expected : string)
642+
requires trans.ValidState()
643+
ensures trans.ValidState()
644+
modifies trans.Modifies
645+
{
646+
var input := Trans.ScanInputTransformInput(sdkInput := q);
647+
var res :- expect trans.ScanInputTransform(input);
648+
if res.transformedInput.FilterExpression != Some(expected) {
649+
print "Transform should have been\n", expected, "\nbut was\n", res.transformedInput.FilterExpression, "\n";
650+
}
651+
}
652+
653+
method BucketTest3()
654+
{
655+
expect "bucket_encrypt" in largeEncryptionConfigs;
656+
var config := largeEncryptionConfigs["bucket_encrypt"];
657+
var configs := Types.DynamoDbTablesEncryptionConfig (tableEncryptionConfigs := map[TableName := config.config]);
658+
assume {:axiom} false;
659+
var trans :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(configs);
660+
661+
TestScanTrans(trans, GetBucketScan1(5), "Attr6 = :attr6");
662+
TestScanTrans(trans, GetBucketScan1(1), "(aws_dbe_b_Attr2 = :attr2) OR (aws_dbe_b_Attr2 = :attr2AA)");
663+
TestScanTrans(trans, GetBucketScan2(5, 1), "(Attr6 = :attr6 AND aws_dbe_b_Attr2 = :attr2) OR (Attr6 = :attr6 AND aws_dbe_b_Attr2 = :attr2AA)");
664+
TestScanTrans(trans, GetBucketScan2(2, 3), "(aws_dbe_b_Attr3 = :attr3 AND aws_dbe_b_Attr4 = :attr4) OR (aws_dbe_b_Attr3 = :attr3AA AND aws_dbe_b_Attr4 = :attr4AA) OR (aws_dbe_b_Attr3 = :attr3AB AND aws_dbe_b_Attr4 = :attr4AB) OR (aws_dbe_b_Attr3 = :attr3 AND aws_dbe_b_Attr4 = :attr4AC) OR (aws_dbe_b_Attr3 = :attr3AA AND aws_dbe_b_Attr4 = :attr4)");
665+
TestScanTrans(trans, GetBucketScan3(1, 2, 3), "(aws_dbe_b_Attr2 = :attr2 AND aws_dbe_b_Attr3 = :attr3 AND aws_dbe_b_Attr4 = :attr4) OR (aws_dbe_b_Attr2 = :attr2AA AND aws_dbe_b_Attr3 = :attr3AA AND aws_dbe_b_Attr4 = :attr4AA) OR (aws_dbe_b_Attr2 = :attr2 AND aws_dbe_b_Attr3 = :attr3AB AND aws_dbe_b_Attr4 = :attr4AB) OR (aws_dbe_b_Attr2 = :attr2AA AND aws_dbe_b_Attr3 = :attr3 AND aws_dbe_b_Attr4 = :attr4AC) OR (aws_dbe_b_Attr2 = :attr2 AND aws_dbe_b_Attr3 = :attr3AA AND aws_dbe_b_Attr4 = :attr4)");
666+
}
667+
662668
// Fill table with 100 records. Different RecNum, same data otherwise
663669
// Make a variety of bucketed queries. Ensure that
664670
// 1) Every item is returned exactly once
@@ -693,24 +699,17 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
693699
TestBucketQueries(rClient, 3, GetBucketQuery35F(), "bucket query 35F", false);
694700
TestBucketQueries(rClient, 4, GetBucketQuery45F(), "bucket query 45F", false);
695701

696-
var scanCount1 := 0;
697-
var scanCount2 := 0;
698-
var scanCount3 := 0;
699702
var scanCount4 := 0;
700703
var scanCount5 := 0;
701-
var scanCount6 := 2;
702704
TestBucketScan(rClient, GetBucketScan6(0,1,2,3,4,5));
703705
TestBucketScan(rClient, GetBucketScan6(5,4,3,2,1,0));
704706
for i := 0 to 6 {
705-
scanCount1 := scanCount1 + 1;
706707
TestBucketScan(rClient, GetBucketScan1(i));
707708
for j := 0 to 6 {
708709
if i != j {
709-
scanCount2 := scanCount2 + 1;
710710
TestBucketScan(rClient, GetBucketScan2(i, j));
711711
for k := 0 to 6 {
712712
if i != k && j != k {
713-
scanCount3 := scanCount3 + 1;
714713
TestBucketScan(rClient, GetBucketScan3(i, j, k));
715714
}
716715
for l := 0 to 6 {
@@ -733,7 +732,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
733732
}
734733
}
735734
}
736-
print "Full Bucket Scan Tests : ", scanCount1, " ", scanCount2, " ", scanCount3, " ", scanCount4, " ", scanCount5, " ", scanCount6, "\n";
737735
}
738736

739737
// As BucketTest1, but with custom bucket selector

0 commit comments

Comments
 (0)