m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy

@@ -132,13 +132,16 @@ module CompoundBeacon {
       && OrderedParts(parts, numSigned)
     }
 
-    function method getNumQueries(globalMax : BucketCount) : BucketCount
-    {
-      var counts := GetBucketCountsFromValue(DDB.AttributeValue.S(""));
-      if counts.Failure? then
-        1
-      else
-        lcmSeq(counts.value, globalMax)
+    method getNumQueries(globalMax : BucketCount, value : string) returns (output : BucketCount)
+      ensures output <= globalMax
+    {
+      var counts := GetBucketCountsFromValue(DDB.AttributeValue.S(value));
+      if counts.Failure? {
+        return 1;
+      } else {
+        output := lcmSeq(counts.value, globalMax);
+        return;
+      }
     }
 
     // no prefix is a prefix of another prefix

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

@@ -32,16 +32,16 @@ module DynamoDBSupport {
   import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import NN = DynamoDbNormalizeNumber
 
-  method GetNumberOfQueries(search : SearchableEncryptionInfo.BeaconVersion, actions : AttributeActions, query : DDB.QueryInput)
+  method GetNumberOfQueries(search : SearchableEncryptionInfo.BeaconVersion, query : DDB.QueryInput)
     returns (output : Result<BucketCount, Error>)
   {
-    // var numberOfQueries :- Filter.GetNumQueries(
-    //   actions,
-    //   query.FilterExpression,
-    //   query.ExpressionAttributeNames,
-    //   search
-    // );
-    return Success(1);
+    var numberOfQueries :- Filter.GetNumQueries(
+      search,
+      query.KeyConditionExpression,
+      query.ExpressionAttributeValues,
+      query.ExpressionAttributeNames
+    );
+    return Success(numberOfQueries);
   }
 
   // IsWritable examines an AttributeMap and fails if it is unsuitable for writing.

DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

@@ -1716,17 +1716,18 @@ module DynamoDBFilterExpr {
     }
     var parsed := ParseExpr(keyExpr.value);
     var values :- GetValues(bv, parsed, values.value, names);
-
-    if |values| == 0 {
-      return Success(1);
-    } else if |values| == 1 {
-      return Success(values[0].0.getNumQueries(bv.numBuckets));
-    } else if |values| == 2 {
-      return Success(lcmBucket(values[0].0.getNumQueries(bv.numBuckets), values[1].0.getNumQueries(bv.numBuckets), bv.numBuckets));
-    } else {
-      print "\nThat's Odd : \n", keyExpr, "\n\n";
-      return Success(1); // FIXME
+    var result : BucketCount := 1;
+    SequenceIsSafeBecauseItIsInMemory(values);
+    for i : uint64 := 0 to |values| as uint64
+      invariant result <= bv.numBuckets
+    {
+      var buckets := values[i].0.getNumQueries(bv.numBuckets, values[0].1);
+      if buckets == 1 || buckets == result {
+        continue;
+      }
+      result := lcmBucket(result, buckets, bv.numBuckets);
     }
+    return Success(result);
   }
 
   // Search through the query expressions to find the Multi-Tenant KeyId
@@ -2026,52 +2027,4 @@ module DynamoDBFilterExpr {
     }
     return Success(true);
   }
-
-  // return an list of encrypted attributes used in expression
-  method GetEncryptedAttrs (
-    actions : AttributeActions,
-    expr : string,
-    names : Option<DDB.ExpressionAttributeNameMap>
-  )
-    returns (output : seq<string>)
-  {
-    var pExpr := ParseExpr(expr);
-    var result : seq<string> := [];
-    for i := 0 to |pExpr| {
-      if pExpr[i].Attr? {
-        var name := GetAttrName(pExpr[i], names);
-        if name in actions && actions[name] == SE.ENCRYPT_AND_SIGN {
-          result := result + [GetAttrName(pExpr[i], names)];
-        }
-      }
-    }
-    return result;
-  }
-
-  // return the number of queries necessary for these encrypted attributes
-  method GetNumQueriesForAttrs(attrs : seq<string>, b : SI.BeaconVersion) returns (output : Result<BucketCount, Error>)
-    ensures output.Success? ==> output.value <= b.numBuckets
-  {
-    if |attrs| == 0 {
-      return Success(1);
-    } else if |attrs| == 1 {
-      var attr := attrs[0];
-      if attr !in b.beacons {
-        return Failure(E("No beacon for " + attr));
-      }
-      return Success(b.beacons[attr].getNumQueries(b.numBuckets));
-    } else if |attrs| == 2 {
-      var attr1 := attrs[0];
-      if attr1 !in b.beacons {
-        return Failure(E("No beacon for " + attr1));
-      }
-      var attr2 := attrs[1];
-      if attr2 !in b.beacons {
-        return Failure(E("No beacon for " + attr2));
-      }
-      return Success(lcmBucket(b.beacons[attr1].getNumQueries(b.numBuckets), b.beacons[attr2].getNumQueries(b.numBuckets), b.numBuckets));
-    } else {
-      return Failure(E("More than two attributes not implemented yet"));
-    }
-  }
 }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -544,16 +544,15 @@ module SearchableEncryptionInfo {
     | Standard(std : BaseBeacon.ValidStandardBeacon)
     | Compound(cmp : CompoundBeacon.ValidCompoundBeacon)
   {
-    function method getNumQueries(globalMax : BucketCount) : BucketCount
-      ensures 0 <= getNumQueries(globalMax) <= globalMax
+    method getNumQueries(globalMax : BucketCount, value : string) returns (output : BucketCount)
+      ensures 0 <= output <= globalMax
     {
-      if Standard? then
-        if std.numberOfBuckets <= globalMax then
-          std.numberOfBuckets
-        else
-          globalMax
-      else
-        cmp.getNumQueries(globalMax)
+      if Standard? {
+        return bmin(std.numberOfBuckets, globalMax);
+      } else {
+        output := cmp.getNumQueries(globalMax, value);
+        return;
+      }
     }
     predicate method isEncrypted()
     {

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy

@@ -8,6 +8,7 @@ module DynamoDbEncryptionUtil {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened StandardLibrary.MemoryMath
   import DDB = ComAmazonawsDynamodbTypes
 
   const ReservedPrefix := "aws_dbe_"
@@ -151,14 +152,24 @@ module DynamoDbEncryptionUtil {
     (a / gcd(a, b)) * b
   }
 
+  function method bmin(a : BucketCount, b : BucketCount) : (output : BucketCount)
+    ensures output <= a
+    ensures output <= b
+  {
+    if a <= b then
+      a
+    else
+      b
+  }
+
   function method lcmBucket(a : BucketCount, b : BucketCount, max : BucketCount) : BucketCount
     requires 0 < a && 0 < b
-    ensures 0 < lcmBucket(a, b, max)
+    ensures 0 < lcmBucket(a, b, max) <= max
   {
-    if a == 1 || b == max then
-      b
+    if a == 1 || b == max || a == b then
+      bmin(b, max)
     else if b == 1 || a == max then
-      a
+      bmin(a, max)
     else
       var result := lcm(a as nat, b as nat);
       if result < max as nat then
@@ -167,20 +178,21 @@ module DynamoDbEncryptionUtil {
         max
   }
 
-  function method lcmSeq(values : seq<BucketCount>, max : BucketCount) : BucketCount
+  method lcmSeq(values : seq<BucketCount>, max : BucketCount) returns (output : BucketCount)
     // requires forall i <- values :: i <= max
-    decreases |values|
+    ensures output <= max
   {
-    if |values| == 0 then
-      1
-    else if |values| == 1 then
-      values[0]
-    else
-      var res := lcmBucket(values[0], values[1], max);
-      if |values| == 2 then
-        res as BucketCount
-      else
-        lcmSeq([res as BucketCount] + values[2..], max)
+    var result : BucketCount := 1;
+    SequenceIsSafeBecauseItIsInMemory(values);
+    for i : uint64 := 0 to |values| as uint64
+      invariant result <= max
+    {
+      var buckets := values[i];
+      if buckets == 1 || buckets == result {
+        continue;
+      }
+      result := lcmBucket(result, buckets, max);
+    }
+    return result;
   }
-
 }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy

@@ -28,7 +28,7 @@ module DynamoDbMiddlewareSupport {
   method GetNumberOfQueries(config : ValidTableConfig, query : DDB.QueryInput) returns (output : Result<ET.BucketCount, Error>)
     requires config.search.Some?
   {
-    var numQueries := BS.GetNumberOfQueries(config.search.value.versions[0], /*config.attributeActionsOnEncrypt*/map[], query);
+    var numQueries := BS.GetNumberOfQueries(config.search.value.versions[0], query);
     return numQueries.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
   }