m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

@@ -154,7 +154,11 @@ module BaseBeacon {
       if numberOfBuckets == 0 || |bucket| as uint64 == 0 then
         bucket
       else
-        [bucket[0] % numberOfBuckets]
+        var newBucket : uint8 := bucket[0] % numberOfBuckets;
+        if newBucket == 0 then
+          []
+        else
+          [newBucket]
     }
     function method {:opaque} hash(val : Bytes, key : Bytes, bucket : Bytes)
       : (ret : Result<string, Error>)

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy

@@ -32,7 +32,7 @@ module AttributeResolver {
         );
     } else {
       var tableConfig := config.tableEncryptionConfigs[input.TableName];
-      var bucket :- GetRandomBucket(tableConfig);
+      var bucket :- GetRandomBucket(tableConfig, input.Item);
       var vf :- GetVirtualFields(tableConfig.search.value, input.Item, input.Version);
       var cb :- GetCompoundBeacons(tableConfig.search.value, input.Item, input.Version, bucket);
       return Success(

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy

@@ -54,7 +54,7 @@ module BatchWriteItemTransform {
             //# The Item MUST be [writable](ddb-support.md#writable).
             var _ :- IsWriteable(tableConfig, req.PutRequest.value.Item);
 
-            var bucket :- GetRandomBucket(tableConfig);
+            var bucket :- GetRandomBucket(tableConfig, req.PutRequest.value.Item);
             var item :- AddSignedBeacons(tableConfig, req.PutRequest.value.Item, bucket);
 
             var encryptRes := tableConfig.itemEncryptor.EncryptItem(EncTypes.EncryptItemInput(plaintextItem:=item));

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy

@@ -53,7 +53,7 @@ module DdbMiddlewareConfig {
   }
 
   datatype TableConfig = TableConfig(
-    physicalTableName: ComAmazonawsDynamodbTypes.TableName,
+    physicalTableName: DDB.TableName,
     logicalTableName: string,
     partitionKeyName: string,
     sortKeyName: Option<string>,
@@ -70,7 +70,7 @@ module DdbMiddlewareConfig {
     || config.tableEncryptionConfigs[tableName].plaintextOverride == AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ
   }
 
-  method GetRandomBucket(config : TableConfig) returns (output : Result<seq<uint8>, Error>)
+  method GetRandomBucket(config : TableConfig, item : DDB.AttributeMap) returns (output : Result<seq<uint8>, Error>)
     modifies config.bucketSelector.Modifies
     requires config.bucketSelector.ValidState()
     ensures config.bucketSelector.ValidState()
@@ -86,9 +86,8 @@ module DdbMiddlewareConfig {
       return Failure(E("Number of buckets exceeds 255"));
     }
 
-    var outR := config.bucketSelector.GetBucketNumber(DDBE.GetBucketNumberInput( item := map[], numberOfBuckets := numBuckets as DDBE.BucketCount));
+    var outR := config.bucketSelector.GetBucketNumber(DDBE.GetBucketNumberInput(item := item, numberOfBuckets := numBuckets as DDBE.BucketCount));
     var out :- outR.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
-
     if out.bucketNumber == 0 {
       return Success([]);
     } else if numBuckets as DDBE.BucketCount <= out.bucketNumber {

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy

@@ -58,7 +58,7 @@ module PutItemTransform {
                                      input.sdkInput.ConditionExpression,
                                      input.sdkInput.ExpressionAttributeNames,
                                      input.sdkInput.ExpressionAttributeValues);
-    var bucket :- GetRandomBucket(tableConfig);
+    var bucket :- GetRandomBucket(tableConfig, input.sdkInput.Item);
     var item :- AddSignedBeacons(tableConfig, input.sdkInput.Item, bucket);
     var encryptRes := tableConfig.itemEncryptor.EncryptItem(
       EncTypes.EncryptItemInput(plaintextItem:=item)

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy

@@ -89,7 +89,7 @@ module TransactWriteItemsTransform {
                                          item.Put.value.ExpressionAttributeNames,
                                          item.Put.value.ExpressionAttributeValues);
 
-        var bucket :- GetRandomBucket(tableConfig);
+        var bucket :- GetRandomBucket(tableConfig, item.Put.value.Item);
         var beaconItem :- AddSignedBeacons(tableConfig, item.Put.value.Item, bucket);
 
         var encryptRes := tableConfig.itemEncryptor.EncryptItem(

TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

@@ -499,6 +499,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
     var compoundBeacons : seq<Types.CompoundBeacon> := [];
     var virtualFields : seq<Types.VirtualField> := [];
     var keySource : Option<Types.BeaconKeySource> := None;
+    var numberOfBuckets: Option<Types.BucketCount> := None;
 
     for i := 0 to |data.obj| {
       var obj := data.obj[i];
@@ -507,6 +508,13 @@ module {:options "-functionSyntax:4"} JsonConfig {
         case "standardBeacons" => standardBeacons :- GetStandardBeacons(obj.1);
         case "compoundBeacons" => compoundBeacons :- GetCompoundBeacons(obj.1);
         case "virtualFields" => virtualFields :- GetVirtualFields(obj.1);
+        case "numberOfBuckets" =>
+          :- Need(obj.1.Number?, "numberOfBuckets must be of type Number.");
+          var num :- DecimalToNat(obj.1.num);
+          expect 0 < num < INT32_MAX_LIMIT;
+          var num2 := num as int32;
+          expect Types.IsValid_BucketCount(num2);
+          numberOfBuckets := Some(num as Types.BucketCount);
         case _ => return Failure("Unexpected part of a beacon version : '" + obj.0 + "'");
       }
     }
@@ -529,7 +537,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
                      compoundBeacons := OptSeq(compoundBeacons),
                      virtualFields := OptSeq(virtualFields),
                      encryptedParts := None,
-                     signedParts := None
+                     signedParts := None,
+                     numberOfBuckets := numberOfBuckets
                    )
       );
   }
@@ -628,7 +637,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
     var results := prev;
     for i := 0 to |gsi| {
       for j := 0 to |gsi[i].KeySchema| {
-        if forall k <- prev :: k.AttributeName != gsi[i].KeySchema[j].AttributeName {
+        if forall k <- results :: k.AttributeName != gsi[i].KeySchema[j].AttributeName {
           results := results +  [DDB.AttributeDefinition(AttributeName := gsi[i].KeySchema[j].AttributeName, AttributeType := DDB.ScalarAttributeType.S)];
         }
       }
@@ -1096,6 +1105,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
     var name : string := "";
     var length : int := -1;
     var loc : Option<Types.TerminalLocation> := None;
+    var numberOfBuckets: Option<Types.BucketCount> := None;
+
     for i := 0 to |data.obj| {
       var obj := data.obj[i];
       match obj.0 {
@@ -1109,12 +1120,19 @@ module {:options "-functionSyntax:4"} JsonConfig {
           :- Need(obj.1.String?, "Standard Beacon Location must be a string");
           :- Need(0 < |obj.1.str|, "Standard Beacon Location must nt be an empty string.");
           loc := Some(obj.1.str);
+        case "numberOfBuckets" =>
+          :- Need(obj.1.Number?, "numberOfBuckets must be of type Number.");
+          var num :- DecimalToNat(obj.1.num);
+          expect 0 < num < INT32_MAX_LIMIT;
+          var num2 := num as int32;
+          expect Types.IsValid_BucketCount(num2);
+          numberOfBuckets := Some(num as Types.BucketCount);
         case _ => return Failure("Unexpected part of a standard beacon : '" + data.obj[i].0 + "'");
       }
     }
     :- Need(0 < |name|, "Each Standard Beacon needs a name.");
     :- Need(0 < length < 100 && Types.IsValid_BeaconBitLength(length as int32), "Each Standard Beacon needs a length between 1 and 63.");
-    return Success(Types.StandardBeacon(name := name, length := length as Types.BeaconBitLength, loc := loc, style := None));
+    return Success(Types.StandardBeacon(name := name, length := length as Types.BeaconBitLength, loc := loc, style := None, numberOfBuckets := numberOfBuckets));
   }
 
   method GetGSIs(data : JSON) returns (output : Result<seq<DDB.GlobalSecondaryIndex> , string>)
@@ -1152,10 +1170,15 @@ module {:options "-functionSyntax:4"} JsonConfig {
                      IndexName := data.arr[0].str,
                      KeySchema := schema,
                      Projection := DDB.Projection(
-                       ProjectionType := None,
+                       ProjectionType := Some(DDB.ProjectionType.ALL),
                        NonKeyAttributes := None
                      ),
-                     ProvisionedThroughput := None
+                     ProvisionedThroughput := Some(
+                       DDB.ProvisionedThroughput (
+                         ReadCapacityUnits:= 5,
+                         WriteCapacityUnits:= 5
+                       )
+                     )
                    ));
   }