feat(SharedCache): Shared Cache for Searchable Encryption

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -354,7 +354,8 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
   datatype MultiKeyStore = | MultiKeyStore (
     nameonly keyFieldName: string ,
     nameonly cacheTTL: int32 ,
-    nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType> := Option.None
+    nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType> := Option.None ,
+    nameonly partitionId: Option<string> := Option.None
   )
   datatype PartOnly = | PartOnly (
 
@@ -388,7 +389,9 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
   }
   datatype SingleKeyStore = | SingleKeyStore (
     nameonly keyId: string ,
-    nameonly cacheTTL: int32
+    nameonly cacheTTL: Option<int32> := Option.None ,
+    nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType> := Option.None ,
+    nameonly partitionId: Option<string> := Option.None
   )
   datatype StandardBeacon = | StandardBeacon (
     nameonly name: string ,

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -713,9 +713,12 @@ structure SingleKeyStore {
   @required
   @javadoc("The Beacon Key ID.")
   keyId : String,
-  @required
-  @javadoc("How long (in seconds) the beacon key material is cached locally before it is re-retrieved from DynamoDB and re-authed with AWS KMS.")
+  @javadoc("How long (in seconds) the beacon key material is cached locally before it is re-retrieved from DynamoDB and re-authed with AWS KMS. Provide only one of cacheTTL or cache.")
   cacheTTL: Integer,
+  @documentation("Provide the Shared Cache for Searchable Encryption. Provide only one of cacheTTL or cache.")
+  cache : CacheType,
+  @documentation("Partition ID to share DynamoDB Interceptors. TODO: Update description")
+  partitionId: String
 }
 
 //= specification/searchable-encryption/search-config.md#multi-key-store-initialization
@@ -734,7 +737,9 @@ structure MultiKeyStore {
   @javadoc("How long (in seconds) the beacon key material is cached locally before it is re-retrieved from DynamoDB and re-authed with AWS KMS.")
   cacheTTL: Integer,
   @javadoc("Which type of local cache to use.")
-  cache : CacheType
+  cache : CacheType,
+  @documentation("Partition ID to share DynamoDB Interceptors. TODO: Update description")
+  partitionId: String
 }
 
 //= specification/searchable-encryption/search-config.md#beacon-key-source

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -33,6 +33,7 @@ module SearchConfigToInfo {
   import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import MPT = AwsCryptographyMaterialProvidersTypes
   import Primitives = AtomicPrimitives
+  import UUID
 
   // convert configured SearchConfig to internal SearchInfo
   method Convert(outer : DynamoDbTableEncryptionConfig)
@@ -137,6 +138,7 @@ module SearchConfigToInfo {
       else
         MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1));
 
+    // TODO : Add check that customers only provide either cacheTTL or cache in case of SingleKeyStore
     var cache;
     if cacheType.Shared? {
       cache := cacheType.Shared;
@@ -151,13 +153,35 @@ module SearchConfigToInfo {
       cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e));
     }
 
+    var partitionIdBytes : seq<uint8>;
+
+    if outer.keyring.Some? {
+      if outer.keyring.value.partitionId.Some? {
+        partitionIdBytes :- UTF8.Encode(outer.keyring.value.partitionId.value)
+        .MapFailure(
+          e => Error.DynamoDbEncryptionException(
+              message := "Could not UTF-8 Encode Partition ID: " + e
+            )
+        );
+      }
+    }
+    else {
+      var uuid? := UUID.GenerateUUID();
+
+      var uuid :- uuid?
+      .MapFailure(e => Error.DynamoDbEncryptionException(message := e));
+
+      partitionIdBytes :- UUID.ToByteArray(uuid)
+      .MapFailure(e => Error.DynamoDbEncryptionException(message := e));
+    }
+
     if config.multi? {
       :- Need(0 < config.multi.cacheTTL, E("Beacon Cache TTL must be at least 1."));
       var deleteKey :- ShouldDeleteKeyField(outer, config.multi.keyFieldName);
-      output := Success(I.KeySource(client, keyStore, I.MultiLoc(config.multi.keyFieldName, deleteKey), cache, config.multi.cacheTTL as uint32));
+      output := Success(I.KeySource(client, keyStore, I.MultiLoc(config.multi.keyFieldName, deleteKey), cache, config.multi.cacheTTL as uint32, partitionIdBytes));
     } else {
       :- Need(0 < config.single.cacheTTL, E("Beacon Cache TTL must be at least 1."));
-      output := Success(I.KeySource(client, keyStore, I.SingleLoc(config.single.keyId), cache, config.single.cacheTTL as uint32));
+      output := Success(I.KeySource(client, keyStore, I.SingleLoc(config.single.keyId), cache, config.single.cacheTTL as uint32, partitionIdBytes));
     }
   }
 

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -26,6 +26,7 @@ module SearchableEncryptionInfo {
   import MP = AwsCryptographyMaterialProvidersTypes
   import KeyStoreTypes = AwsCryptographyKeyStoreTypes
   import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
+  import opened CacheConstants
 
   //= specification/searchable-encryption/search-config.md#version-number
   //= type=implication
@@ -137,7 +138,8 @@ module SearchableEncryptionInfo {
     store : ValidStore,
     keyLoc : KeyLocation,
     cache : MP.ICryptographicMaterialsCache,
-    cacheTTL : uint32
+    cacheTTL : uint32,
+    partitionIdBytes : seq<uint8>
   ) {
     function Modifies() : set<object> {
       client.Modifies + store.Modifies
@@ -153,7 +155,7 @@ module SearchableEncryptionInfo {
     {
       if keyLoc.SingleLoc? {
         :- Need(keyId.DontUseKeyId?, E("KeyID should not be supplied with a SingleKeyStore"));
-        var theMap :- getKeysCache(stdNames, keyLoc.keyId);
+        var theMap :- getKeysCache(stdNames, keyLoc.keyId, partitionIdBytes);
         return Success(Keys(theMap));
       } else if keyLoc.LiteralLoc? {
         :- Need(keyId.DontUseKeyId?, E("KeyID should not be supplied with a LiteralKeyStore"));
@@ -163,7 +165,7 @@ module SearchableEncryptionInfo {
         match keyId {
           case DontUseKeyId => return Failure(E("KeyID must not be supplied with a MultiKeyStore"));
           case ShouldHaveKeyId => return Success(ShouldHaveKeys);
-          case KeyId(id) => var theMap :- getKeysCache(stdNames, id); return Success(Keys(theMap));
+          case KeyId(id) => var theMap :- getKeysCache(stdNames, id, partitionIdBytes); return Success(Keys(theMap));
         }
       }
     }
@@ -182,7 +184,8 @@ module SearchableEncryptionInfo {
 
     method getKeysCache(
       stdNames : seq<string>,
-      keyId : string
+      keyId : string,
+      partitionIdBytes : seq<uint8>
     )
       returns (output : Result<HmacKeyMap, Error>)
       requires Seq.HasNoDuplicates(stdNames)
@@ -241,8 +244,21 @@ module SearchableEncryptionInfo {
 
                    )
     {
+
+      // Resource ID: Searchable Encryption [0x02]
+      var resourceId : seq<uint8> := RESOURCE_ID_HIERARCHICAL_KEYRING;
+
+      // Scope ID: Searchable Encryption [0x03]
+      var scopeId : seq<uint8> := SCOPE_ID_SEARCHABLE_ENCRYPTION;
+
+      // Create the Suffix
       var keyIdBytesR := UTF8.Encode(keyId);
       var keyIdBytes :- keyIdBytesR.MapFailure(e => E(e));
+      var suffix : seq<uint8> := keyIdBytes;
+
+      // Append Resource Id, Scope Id, Partition Id, and Suffix to create the cache identifier
+      var identifier := resourceId + NULL_BYTE + scopeId + NULL_BYTE + partitionIdBytes + NULL_BYTE + suffix;
+
       var getCacheInput := MP.GetCacheEntryInput(identifier := keyIdBytes, bytesUsed := None);
       verifyValidStateCache(cache);
       assume {:axiom} cache.Modifies == {};
@@ -253,6 +269,7 @@ module SearchableEncryptionInfo {
         return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=getCacheOutput.error));
       }
 
+      // TODO: Add cacheEntryWithinLimits
       if getCacheOutput.Failure? {
         //= specification/searchable-encryption/search-config.md#beacon-keys
         //# Beacon keys MUST be obtained from the configured [Beacon Key Source](#beacon-key-source).

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy

@@ -26,7 +26,7 @@ module DynamoDbEncryptionUtil {
   //
   // Counterintuitively, DontUseKeys and DontUseKeyId are very different things.
   // DontUseKeyId is the usual thing for single tenant, meaning to use the pre-configured
-  // KeyId, rather than fnd a new one from somewhere.
+  // KeyId, rather than find a new one from somewhere.
   // DontUseKeys means to not hash the values into beacons,
   // but to leave them plaintext, which is necessary for the post-query filtering.
   datatype MaybeKeyMap =

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

@@ -764,10 +764,10 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
                               tmp5.search.Some? ==>
                                 var tmps6 := set t6 | t6 in tmp5.search.value.versions;
                                 forall tmp6 :: tmp6 in tmps6 ==>
-                                                 tmp6.keySource.multi? ==>
-                                                   tmp6.keySource.multi.cache.Some? ==>
-                                                     tmp6.keySource.multi.cache.value.Shared? ==>
-                                                       tmp6.keySource.multi.cache.value.Shared.ValidState()
+                                                 tmp6.keySource.single? ==>
+                                                   tmp6.keySource.single.cache.Some? ==>
+                                                     tmp6.keySource.single.cache.value.Shared? ==>
+                                                       tmp6.keySource.single.cache.value.Shared.ValidState()
     modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true
                                                                            && t7.keyring.Some?
                             :: t7.keyring.value,
@@ -788,10 +788,10 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
     modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
                                                                              && t12.search.Some?
                              , t13 <- t12.search.value.versions | true
-                                                                  && t13.keySource.multi?
-                                                                  && t13.keySource.multi.cache.Some?
-                                                                  && t13.keySource.multi.cache.value.Shared?
-                             :: t13.keySource.multi.cache.value.Shared,
+                                                                  && t13.keySource.single?
+                                                                  && t13.keySource.single.cache.Some?
+                                                                  && t13.keySource.single.cache.value.Shared?
+                             :: t13.keySource.single.cache.value.Shared,
                obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
     ensures res.Success? ==>
               && fresh(res.value)
@@ -816,10 +816,10 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
                        ) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true
                                                                                              && t19.search.Some?
                                              , t20 <- t19.search.value.versions | true
-                                                                                  && t20.keySource.multi?
-                                                                                  && t20.keySource.multi.cache.Some?
-                                                                                  && t20.keySource.multi.cache.value.Shared?
-                                             :: t20.keySource.multi.cache.value.Shared,
+                                                                                  && t20.keySource.single?
+                                                                                  && t20.keySource.single.cache.Some?
+                                                                                  && t20.keySource.single.cache.value.Shared?
+                                             :: t20.keySource.single.cache.value.Shared,
                                obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj
                        ) )
               && fresh(res.value.History)
@@ -847,10 +847,10 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
                               tmp26.search.Some? ==>
                                 var tmps27 := set t27 | t27 in tmp26.search.value.versions;
                                 forall tmp27 :: tmp27 in tmps27 ==>
-                                                  tmp27.keySource.multi? ==>
-                                                    tmp27.keySource.multi.cache.Some? ==>
-                                                      tmp27.keySource.multi.cache.value.Shared? ==>
-                                                        tmp27.keySource.multi.cache.value.Shared.ValidState()
+                                                  tmp27.keySource.single? ==>
+                                                    tmp27.keySource.single.cache.Some? ==>
+                                                      tmp27.keySource.single.cache.value.Shared? ==>
+                                                        tmp27.keySource.single.cache.value.Shared.ValidState()
 
   // Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
   function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result<IDynamoDbEncryptionTransformsClient, Error> {

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

@@ -150,7 +150,7 @@ module
       var tableName: string := tableNamesSeq[i];
 
       var inputConfig := config.tableEncryptionConfigs[tableName];
-      :- Need(inputConfig.logicalTableName !in allLogicalTableNames,  E("Duplicate logical table maped to multipule physical tables: " + inputConfig.logicalTableName));
+      :- Need(inputConfig.logicalTableName !in allLogicalTableNames,  E("Duplicate logical table mapped to multiple physical tables: " + inputConfig.logicalTableName));
 
       assert SearchConfigToInfo.ValidSearchConfig(inputConfig.search);
       SearchInModifies(config, tableName);