m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -42,10 +42,12 @@ module SearchConfigToInfo {
     requires ValidSearchConfig(outer.search)
     requires outer.search.Some? ==> ValidSharedCache(outer.search.value.versions[0].keySource)
     modifies if outer.search.Some? then outer.search.value.versions[0].keyStore.Modifies else {}
+    modifies if outer.search.Some? && outer.search.value.versions[0].bucketSelector.Some? then outer.search.value.versions[0].bucketSelector.value.Modifies else {}
     ensures outer.search.Some? ==> ValidSharedCache(outer.search.value.versions[0].keySource)
     ensures output.Success? && output.value.Some? ==>
               && output.value.value.ValidState()
               && fresh(output.value.value.versions[0].keySource.client)
+              && fresh(output.value.value.versions[0].bucketSelector)
     //= specification/searchable-encryption/search-config.md#initialization
     //= type=implication
     //# Initialization MUST fail if the [version number](#version-number) is not `1`.
@@ -242,10 +244,13 @@ module SearchConfigToInfo {
     requires ValidBeaconVersion(config)
     requires ValidSharedCache(config.keySource)
     modifies config.keyStore.Modifies
+    modifies if config.bucketSelector.Some? then config.bucketSelector.value.Modifies else {}
     ensures ValidSharedCache(config.keySource)
     ensures output.Success? ==>
               && output.value.ValidState()
               && fresh(output.value.keySource.client)
+              && fresh(output.value.bucketSelector)
+              && fresh (output.value.bucketSelector.Modifies)
 
     //= specification/searchable-encryption/search-config.md#beacon-version-initialization
     //= type=implication
@@ -264,7 +269,8 @@ module SearchConfigToInfo {
     var maybePrimitives := Primitives.AtomicPrimitives();
     var primitives :- maybePrimitives.MapFailure(e => AwsCryptographyPrimitives(e));
     var source :- MakeKeySource(outer, config.keyStore, config.keySource, primitives);
-    output := ConvertVersionWithSource(outer, config, source);
+    var version :- ConvertVersionWithSource(outer, config, source);
+    return Success(version);
   }
 
   class DefaultBucketSelector extends IBucketSelector
@@ -321,6 +327,8 @@ module SearchConfigToInfo {
     ensures output.Success? ==>
               && output.value.ValidState()
               && output.value.keySource == source
+              && fresh(output.value.bucketSelector)
+              && fresh(output.value.bucketSelector.Modifies)
   {
     var maxBuckets : BucketCount := config.maximumNumberOfBuckets.UnwrapOr(1);
     var defaultBuckets : BucketCount := config.defaultNumberOfBuckets.UnwrapOr(maxBuckets);
@@ -376,15 +384,17 @@ module SearchConfigToInfo {
       bucketSelector := new DefaultBucketSelector();
     }
 
-    return I.MakeBeaconVersion(
-        config.version as I.VersionNumber,
-        source,
-        beacons,
-        virtualFields,
-        outer.attributeActionsOnEncrypt,
-        bucketSelector,
-        maxBuckets
-      );
+    var ret :- I.MakeBeaconVersion(
+      config.version as I.VersionNumber,
+      source,
+      beacons,
+      virtualFields,
+      outer.attributeActionsOnEncrypt,
+      bucketSelector,
+      maxBuckets
+    );
+    assume {:axiom} fresh(ret.bucketSelector);
+    return Success(ret);
   }
 
   // convert configured VirtualFieldList to internal VirtualFieldMap

DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

@@ -215,6 +215,7 @@ module BeaconTestFixtures {
     ensures
       && output.keySource.multi?
       && output.keySource.multi.cache.None?
+      && output.bucketSelector.None?
   {
     var store := GetKeyStore();
     return BeaconVersion (

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy

@@ -32,6 +32,7 @@ module AttributeResolver {
         );
     } else {
       var tableConfig := config.tableEncryptionConfigs[input.TableName];
+      assume {:axiom} fresh(if tableConfig.search.Some? then tableConfig.search.value.curr().bucketSelector.Modifies else {});
       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);

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy

@@ -54,6 +54,7 @@ module BatchWriteItemTransform {
             //# The Item MUST be [writable](ddb-support.md#writable).
             var _ :- IsWriteable(tableConfig, req.PutRequest.value.Item);
 
+            assume {:axiom} fresh(if tableConfig.search.Some? then tableConfig.search.value.curr().bucketSelector.Modifies else {});
             var bucket :- GetRandomBucket(tableConfig, req.PutRequest.value.Item);
             var item :- AddSignedBeacons(tableConfig, req.PutRequest.value.Item, bucket);
 

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

@@ -161,6 +161,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
       assert SearchConfigToInfo.ValidSearchConfig(inputConfig.search);
       SearchInModifies(config, tableName);
       reveal SearchConfigToInfo.ValidSharedCache();
+      assume {:axiom} if inputConfig.search.Some? && inputConfig.search.value.versions[0].bucketSelector.Some? then fresh(inputConfig.search.value.versions[0].bucketSelector.value.Modifies) else true;
       var searchR := SearchConfigToInfo.Convert(inputConfig);
       var search :- searchR.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
       assert search.None? || search.value.ValidState();

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy

@@ -58,6 +58,7 @@ module PutItemTransform {
                                      input.sdkInput.ConditionExpression,
                                      input.sdkInput.ExpressionAttributeNames,
                                      input.sdkInput.ExpressionAttributeValues);
+    assume {:axiom} fresh(if tableConfig.search.Some? then tableConfig.search.value.curr().bucketSelector.Modifies else {});
     var bucket :- GetRandomBucket(tableConfig, input.sdkInput.Item);
     var item :- AddSignedBeacons(tableConfig, input.sdkInput.Item, bucket);
     var encryptRes := tableConfig.itemEncryptor.EncryptItem(

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy

@@ -89,6 +89,7 @@ module TransactWriteItemsTransform {
                                          item.Put.value.ExpressionAttributeNames,
                                          item.Put.value.ExpressionAttributeValues);
 
+        assume {:axiom} fresh(if tableConfig.search.Some? then tableConfig.search.value.curr().bucketSelector.Modifies else {});
         var bucket :- GetRandomBucket(tableConfig, item.Put.value.Item);
         var beaconItem :- AddSignedBeacons(tableConfig, item.Put.value.Item, bucket);