m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

@@ -113,7 +113,7 @@ module BaseBeacon {
     partOnly : bool,
     asSet : bool,
     share : Option<string>,
-    numberOfBuckets : Option<BucketCount>
+    numberOfBuckets : BucketCount
   )
     : (ret : Result<ValidStandardBeacon, Error>)
     ensures ret.Success? ==>
@@ -123,8 +123,6 @@ module BaseBeacon {
     var termLoc :- TermLoc.MakeTermLoc(loc);
     var beaconName := BeaconPrefix + name;
     :- Need(DDB.IsValid_AttributeName(beaconName), E(beaconName + " is not a valid attribute name."));
-    var numBuckets : nat := if numberOfBuckets.Some? then numberOfBuckets.value as nat else 0;
-    // :- Need(numBuckets < 256, E(beaconName + " has numberOfBuckets greater than 255"));
     Success(StandardBeacon.StandardBeacon(
               BeaconBase (
                 client := client,
@@ -136,7 +134,7 @@ module BaseBeacon {
               partOnly,
               asSet,
               share,
-              numBuckets as OptBucketCount
+              numberOfBuckets
             ))
   }
   datatype StandardBeacon = StandardBeacon (
@@ -146,15 +144,15 @@ module BaseBeacon {
     partOnly : bool,
     asSet : bool,
     share : Option<string>,
-    numberOfBuckets : OptBucketCount
+    numberOfBuckets : BucketCount
   ) {
 
     function method constrained_bucket(bucket : BucketNumber) : BucketBytes
     {
       if numberOfBuckets == 0 || bucket == 0 then
         BucketNumberToBytes(bucket)
       else
-        var newBucket : BucketNumber := (bucket as OptBucketCount % numberOfBuckets) as BucketNumber;
+        var newBucket : BucketNumber := (bucket as BucketCount % numberOfBuckets) as BucketNumber;
         BucketNumberToBytes(newBucket)
     }
 

DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy

@@ -132,6 +132,15 @@ 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)
+    }
+
     // no prefix is a prefix of another prefix
     // that is, no ambiguity when determining which prefix is used in a value
     predicate ValidPrefixSet()
@@ -328,6 +337,28 @@ module CompoundBeacon {
           Success(DDB.AttributeValue.S(result))
     }
 
+    function method GetBucketCountsFromParts(inParts : seq<BeaconPart>) : seq<BucketCount>
+    {
+      if |inParts| == 0 then
+        []
+      else if inParts[0].Encrypted? then
+        [inParts[0].beacon.numberOfBuckets]
+      else
+        []
+    }
+
+    // for the given attribute value, return the beacon value
+    function method GetBucketCountsFromValue(value : DDB.AttributeValue) : Result<seq<BucketCount>, Error>
+    {
+      if !value.S? then
+        Failure(E("CompoundBeacon " + base.name + " can only be queried as a string, not as " + AttrTypeToStr(value)))
+      else
+        var parts := Split(value.S, split);
+        var partsUsed :- Sequence.MapWithResult(s => getPartFromPrefix(s), parts);
+        var _ :- ValidatePartOrder(partsUsed, value.S);
+        Success(GetBucketCountsFromParts(partsUsed))
+    }
+
     // return the beacon value for this constructor, if possible
     function method {:opaque} {:tailrecursion} TryConstructor(
       consFields : seq<ConstructorPart>,

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -526,18 +526,25 @@ module SearchConfigToInfo {
       Failure(E("Beacon " + name + " is shared to " + share + " which is not defined."))
   }
 
-  predicate method BucketConstraintOk(outer : DynamoDbTableEncryptionConfig, inner : Option<BucketCount>)
+  function method GetBucketCount(outer : DynamoDbTableEncryptionConfig, inner : Option<BucketCount>, name : string) :
+    Result<BucketCount,Error>
   {
-    if inner.None? || outer.search.None? || |outer.search.value.versions| == 0 then
-      true
+    if outer.search.None? || |outer.search.value.versions| == 0 then
+      Success(1)
     else
       var num := outer.search.value.versions[0].numberOfBuckets;
-      if num.None? then
-        false
+      if BucketCountNone(num) then
+        if !BucketCountNone(inner) then
+          Failure(E("Constrained numberOfBuckets for  " + name + " is " + Base10Int2String(inner.value as int) + " but there is not global numberOfBuckets set."))
+        else
+          Success(1)
+      else if BucketCountNone(inner) then
+        Success(num.value)
+      else if inner.value < num.value then
+        Success(inner.value)
       else
-        inner.value <= num.value
+        Failure(E("Constrained numberOfBuckets for  " + name + " is " + Base10Int2String(inner.value as int) + " but it must be less than the global numberOfBuckets " + Base10Int2String(num.value as int)))
   }
-
   // convert configured StandardBeacons to internal Beacons
   method {:tailrecursion} AddStandardBeacons(
     beacons : seq<StandardBeacon>,
@@ -601,9 +608,9 @@ module SearchConfigToInfo {
         case sharedSet(t) => share := Some(t.other); isAsSet := true;
       }
     }
-    :- Need(BucketConstraintOk(outer, beacons[0].numberOfBuckets), E("Constrained numberOfBuckets for  " + beacons[0].name + " must be less than the global numberOfBuckets."));
+    var bucketCount :- GetBucketCount(outer, beacons[0].numberOfBuckets, beacons[0].name);
     var newBeacon :- B.MakeStandardBeacon(client, beacons[0].name, beacons[0].length as B.BeaconLength, locString,
-                                          isPartOnly, isAsSet, share, beacons[0].numberOfBuckets);
+                                          isPartOnly, isAsSet, share, bucketCount);
 
     //= specification/searchable-encryption/search-config.md#beacon-version-initialization
     //# Initialization MUST fail if the [terminal location](virtual.md#terminal-location)

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

@@ -315,9 +315,8 @@ module DynamoDBSupport {
     :- Need(values.None? || BucketQueriesName !in values.value, E(""));
 
     // No bucket specified is OK if no encrypted fields are searched
-    var encrypted := set k <- actions | actions[k] == SE.ENCRYPT_AND_SIGN :: k;
-    var filterHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(filterExpr), encrypted, names);
-    var keyHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(keyExpr), encrypted, names);
+    var filterHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(filterExpr), actions, names);
+    var keyHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(keyExpr), actions, names);
     if keyHasEncField.Some? || filterHasEncField.Some? {
       return Failure(E("When numberOfBuckets is greater than one, FilterExpression must start with 'aws_dbe_bucket = NN && '"));
     } else {
@@ -343,6 +342,15 @@ module DynamoDBSupport {
 
       var foo :- ExtractBucket(search.value.curr(), req.FilterExpression, req.KeyConditionExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues, actions);
       var (newValues, bucket, bucket_queries) := foo;
+      var numQueries :- Filter.GetNumQueries(actions, req.KeyConditionExpression, req.ExpressionAttributeNames, search.value.curr());
+      if numQueries < bucket {
+        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)));
+      }
+      if bucket_queries.Some? {
+        if numQueries != bucket_queries.value {
+          return Failure(E("Number of queries was " + String.Base10Int2String(numQueries as int) + " but should have been " + String.Base10Int2String(bucket_queries.value as int)));
+        }
+      }
       var oldContext := Filter.ExprContext(req.KeyConditionExpression, req.FilterExpression, newValues, req.ExpressionAttributeNames);
       var newContext :- Filter.DoBeaconize(search.value.curr(), oldContext, keyId, bucket, bucket_queries);
       return Success(req.(

DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

@@ -1796,6 +1796,10 @@ module DynamoDBFilterExpr {
         allUnchanged := false;
         break;
       }
+      if new_context.values.value[new_values[i]] != old_context.values.value[new_values[i]] {
+        allUnchanged := false;
+        break;
+      }
     }
     if allUnchanged {
       return Success(old_context);
@@ -1924,15 +1928,15 @@ module DynamoDBFilterExpr {
   // return an error if any encrypted field exists in the query
   method UsesEncryptedField(
     expr : seq<Token>,
-    encrypted : set<string>,
+    actions : AttributeActions,
     names : Option<DDB.ExpressionAttributeNameMap>
   )
     returns (output : Option<string>)
   {
     for i := 0 to |expr| {
       if expr[i].Attr? {
         var name := GetAttrName(expr[i], names);
-        if name in encrypted {
+        if name in actions && actions[name] == SE.ENCRYPT_AND_SIGN {
           return Some(name);
         }
       }
@@ -1942,12 +1946,12 @@ module DynamoDBFilterExpr {
 
   method TestParsedExpr(
     expr : seq<Token>,
-    encrypted : set<string>,
+    actions : AttributeActions,
     names : Option<DDB.ExpressionAttributeNameMap>
   )
     returns (output : Outcome<Error>)
   {
-    var hasEncField := UsesEncryptedField(expr, encrypted, names);
+    var hasEncField := UsesEncryptedField(expr, actions, names);
     if hasEncField.Some? {
       return Fail(E("Query is using encrypted field : " + hasEncField.value + "."));
     }
@@ -1963,14 +1967,76 @@ module DynamoDBFilterExpr {
   )
     returns (output : Result<bool, Error>)
   {
-    var encrypted := set k <- actions | actions[k] == SE.ENCRYPT_AND_SIGN :: k;
     if keyExpr.Some? {
-      :- TestParsedExpr(ParseExpr(keyExpr.value), encrypted, names);
+      :- TestParsedExpr(ParseExpr(keyExpr.value), actions, names);
     }
     if filterExpr.Some? {
-      :- TestParsedExpr(ParseExpr(filterExpr.value), encrypted, names);
+      :- TestParsedExpr(ParseExpr(filterExpr.value), actions, names);
     }
     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? ==> 0 < output.value
+  {
+    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"));
+    }
+  }
+
+  method GetNumQueries (
+    actions : AttributeActions,
+    expr : Option<string>,
+    names : Option<DDB.ExpressionAttributeNameMap>,
+    b : SI.BeaconVersion
+  )
+    returns (output : Result<BucketCount, Error>)
+  {
+    if expr.None? {
+      return Success(1);
+    }
+    var attrs := GetEncryptedAttrs(actions, expr.value, names);
+    output := GetNumQueriesForAttrs(attrs, b);
+  }
+
 }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -544,6 +544,13 @@ module SearchableEncryptionInfo {
     | Standard(std : BaseBeacon.ValidStandardBeacon)
     | Compound(cmp : CompoundBeacon.ValidCompoundBeacon)
   {
+    function method getNumQueries(globalMax : BucketCount) : BucketCount
+    {
+      if Standard? then
+        std.numberOfBuckets
+      else
+        cmp.getNumQueries(globalMax)
+    }
     predicate method isEncrypted()
     {
       if Standard? then

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy

@@ -101,6 +101,12 @@ module DynamoDbEncryptionUtil {
       [x as uint8]
   }
 
+  // Java is broken, None becomes Some(0)
+  predicate method BucketCountNone(x : Option<BucketCount>)
+  {
+    x.None? || x.value == 0
+  }
+
   predicate method Valid_BucketBytes(x : seq<uint8>)
   {
     && |x| <= 1
@@ -113,4 +119,68 @@ module DynamoDbEncryptionUtil {
     print x,"\n";
     return ();
   }
+  function printFromFunction2<T, U>(x: T, y : U): () {
+    ()
+  } by method {
+    print x, " ", y, "\n";
+    return ();
+  }
+  function printFromFunction3<T, U, V>(x: T, y : U, z : V): () {
+    ()
+  } by method {
+    print x, " ", y, " ", z, "\n";
+    return ();
+  }
+
+  function method gcd(a : nat, b : nat) : nat
+    requires 0 < a || 0 < b
+    ensures 0 < gcd(a, b)
+    ensures 0 < b ==> gcd(a, b) <= b
+    decreases b
+  {
+    if b == 0 then
+      a
+    else
+      gcd(b, a % b)
+  }
+
+  function method lcm(a : nat, b : nat) : nat
+    requires 0 < a && 0 < b
+    ensures 0 < lcm(a, b)
+  {
+    (a / gcd(a, b)) * b
+  }
+
+  function method lcmBucket(a : BucketCount, b : BucketCount, max : BucketCount) : BucketCount
+    requires 0 < a && 0 < b
+    ensures 0 < lcmBucket(a, b, max)
+  {
+    if a == 1 || b == max then
+      b
+    else if b == 1 || a == max then
+      a
+    else
+      var result := lcm(a as nat, b as nat);
+      if result < max as nat then
+        result as BucketCount
+      else
+        max
+  }
+
+  function method lcmSeq(values : seq<BucketCount>, max : BucketCount) : BucketCount
+    // requires forall i <- values :: i <= max
+    decreases |values|
+  {
+    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)
+  }
+
 }