add logicalKeyStoreName

aws · Dec 23, 2024 · be3e77c · be3e77c
1 parent 59862ee
commit be3e77c
Show file tree

Hide file tree

Showing 5 changed files with 72 additions and 19 deletions.
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
@@ -39,6 +39,7 @@ module SearchConfigToInfo {
     returns (output : Result<Option<I.ValidSearchInfo>, Error>)
     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 {}
     ensures output.Success? && output.value.Some? ==>
               && output.value.value.ValidState()
               && fresh(output.value.value.versions[0].keySource.client)
@@ -57,7 +58,8 @@ module SearchConfigToInfo {
     } else {
       :- Need(outer.search.value.writeVersion == 1, E("writeVersion must be '1'."));
       :- Need(|outer.search.value.versions| == 1, E("search config must be have exactly one version."));
-      var version :- ConvertVersion(outer, outer.search.value.versions[0]);
+      var beaconVersionConfig := outer.search.value.versions[0];
+      var version :- ConvertVersion(outer, beaconVersionConfig);
       var info := I.MakeSearchInfo(version);
       return Success(Some(info));
     }
@@ -115,6 +117,7 @@ module SearchConfigToInfo {
   )
     returns (output : Result<I.KeySource, Error>)
     modifies client.Modifies
+    modifies keyStore.Modifies
     requires client.ValidState()
     requires ValidSharedCache(config)
     ensures client.ValidState()
@@ -203,16 +206,25 @@ module SearchConfigToInfo {
       );
     }
     else {
-      partitionIdBytes :- I.GeneratePartitionId();
+      partitionIdBytes :- I.GenerateUuidBytes();
     }
+    var getKeyStoreInfoOutput? := keyStore.GetKeyStoreInfo();
+    var getKeyStoreInfoOutput :- getKeyStoreInfoOutput?.MapFailure(e => Error.AwsCryptographyKeyStore(e));
+    var logicalKeyStoreName : string := getKeyStoreInfoOutput.logicalKeyStoreName;
+    var logicalKeyStoreNameBytes : seq<uint8> :- UTF8.Encode(logicalKeyStoreName)
+      .MapFailure(
+        e => Error.DynamoDbEncryptionException(
+            message := "Could not UTF-8 Encode Logical Key Store Name: " + 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, partitionIdBytes));
+      output := Success(I.KeySource(client, keyStore, I.MultiLoc(config.multi.keyFieldName, deleteKey), cache, config.multi.cacheTTL as uint32, partitionIdBytes, logicalKeyStoreNameBytes));
     } 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, partitionIdBytes));
+      output := Success(I.KeySource(client, keyStore, I.SingleLoc(config.single.keyId), cache, config.single.cacheTTL as uint32, partitionIdBytes, logicalKeyStoreNameBytes));
     }
   }
 
@@ -221,6 +233,7 @@ module SearchConfigToInfo {
     returns (output : Result<I.ValidBeaconVersion, Error>)
     requires ValidBeaconVersion(config)
     requires ValidSharedCache(config.keySource)
+    modifies config.keyStore.Modifies
     ensures output.Success? ==>
               && output.value.ValidState()
               && fresh(output.value.keySource.client)

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
@@ -129,18 +129,18 @@ module SearchableEncryptionInfo {
     return Success(newKey);
   }
 
-  // Generates a new partitionId, which is a random UUID
-  method GeneratePartitionId() returns (output : Result<seq<uint8>, Error>)
+  // Generates a new random UUID converted to UTF8 bytes
+  method GenerateUuidBytes() returns (output : Result<seq<uint8>, Error>)
   {
     var uuid? := UUID.GenerateUUID();
 
     var uuid :- uuid?
     .MapFailure(e => Error.DynamoDbEncryptionException(message := e));
 
-    var partitionIdBytes: seq<uint8> :- UUID.ToByteArray(uuid)
+    var uuidBytes: seq<uint8> :- UUID.ToByteArray(uuid)
     .MapFailure(e => Error.DynamoDbEncryptionException(message := e));
 
-    output := Success(partitionIdBytes);
+    output := Success(uuidBytes);
   }
 
   datatype KeyLocation =
@@ -154,7 +154,8 @@ module SearchableEncryptionInfo {
     keyLoc : KeyLocation,
     cache : MP.ICryptographicMaterialsCache,
     cacheTTL : uint32,
-    partitionIdBytes : seq<uint8>
+    partitionIdBytes : seq<uint8>,
+    logicalKeyStoreNameBytes : seq<uint8>
   ) {
     function Modifies() : set<object> {
       client.Modifies + store.Modifies + cache.Modifies
@@ -174,7 +175,7 @@ module SearchableEncryptionInfo {
       if keyLoc.SingleLoc? {
         :- Need(keyId.DontUseKeyId?, E("KeyID should not be supplied with a SingleKeyStore"));
         var now := Time.GetCurrent();
-        var theMap :- getKeysCache(stdNames, keyLoc.keyId, cacheTTL as MP.PositiveLong, partitionIdBytes, now as MP.PositiveLong);
+        var theMap :- getKeysCache(stdNames, keyLoc.keyId, cacheTTL as MP.PositiveLong, partitionIdBytes, logicalKeyStoreNameBytes, now as MP.PositiveLong);
         return Success(Keys(theMap));
       } else if keyLoc.LiteralLoc? {
         :- Need(keyId.DontUseKeyId?, E("KeyID should not be supplied with a LiteralKeyStore"));
@@ -184,7 +185,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 now := Time.GetCurrent(); var theMap :- getKeysCache(stdNames, id, cacheTTL as MP.PositiveLong, partitionIdBytes, now as MP.PositiveLong); return Success(Keys(theMap));
+          case KeyId(id) => var now := Time.GetCurrent(); var theMap :- getKeysCache(stdNames, id, cacheTTL as MP.PositiveLong, partitionIdBytes, logicalKeyStoreNameBytes, now as MP.PositiveLong); return Success(Keys(theMap));
         }
       }
     }
@@ -218,6 +219,7 @@ module SearchableEncryptionInfo {
       keyId : string,
       cacheTTL : MP.PositiveLong,
       partitionIdBytes : seq<uint8>,
+      logicalKeyStoreNameBytes : seq<uint8>,
       now : MP.PositiveLong
     )
       returns (output : Result<HmacKeyMap, Error>)
@@ -238,7 +240,7 @@ module SearchableEncryptionInfo {
                 && var cacheInput := Seq.Last(newHistory).input;
                 && var cacheOutput := Seq.Last(newHistory).output;
                 && UTF8.Encode(keyId).Success?
-                && cacheInput.identifier == RESOURCE_ID_HIERARCHICAL_KEYRING + NULL_BYTE + SCOPE_ID_SEARCHABLE_ENCRYPTION + NULL_BYTE + partitionIdBytes + NULL_BYTE + UTF8.Encode(keyId).value
+                && cacheInput.identifier == RESOURCE_ID_HIERARCHICAL_KEYRING + NULL_BYTE + SCOPE_ID_SEARCHABLE_ENCRYPTION + NULL_BYTE + partitionIdBytes + NULL_BYTE + logicalKeyStoreNameBytes + NULL_BYTE + UTF8.Encode(keyId).value
 
                 //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
                 //= type=implication
@@ -297,7 +299,7 @@ module SearchableEncryptionInfo {
       // Create the Suffix
       var keyIdBytesR := UTF8.Encode(keyId);
       var keyIdBytes :- keyIdBytesR.MapFailure(e => E(e));
-      var suffix : seq<uint8> := keyIdBytes;
+      var suffix : seq<uint8> := logicalKeyStoreNameBytes + NULL_BYTE + 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;

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy
@@ -246,8 +246,20 @@ module BeaconTestFixtures {
     );
     var cache :- expect mpl.CreateCryptographicMaterialsCache(input);
     // Create a test partitionIdBytes
-    var partitionIdBytes : seq<uint8> :- expect SI.GeneratePartitionId();
-    return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0, partitionIdBytes);
+    var partitionIdBytes : seq<uint8> :- expect SI.GenerateUuidBytes();
+
+    // Create a random logicalKeyStoreNameBytes
+    // Ideally, this should be taken from the KeyStore version.keyStore,
+    // but logicalKeyStoreName variable doesn't exist in the
+    // trait AwsCryptographyKeyStoreTypes.IKeyStoreClient
+    // Therefore, the only way to get logicalKeyStoreName is
+    // to call GetKeyStoreInfo, which we don't need to do here
+    // since this method does NOT test the shared cache
+    // which is the only place logicalKeyStoreName is used
+    // (in the cache identifier)
+    var logicalKeyStoreNameBytes : seq<uint8> :- expect SI.GenerateUuidBytes();
+
+    return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0, partitionIdBytes, logicalKeyStoreNameBytes);
   }
 
   method GetMultiSource(keyName : string, version : BeaconVersion) returns (output : SI.KeySource)
@@ -266,8 +278,20 @@ module BeaconTestFixtures {
     );
     var cache :- expect mpl.CreateCryptographicMaterialsCache(input);
     // Create a test partitionIdBytes
-    var partitionIdBytes : seq<uint8> :- expect SI.GeneratePartitionId();
-    return SI.KeySource(client, version.keyStore, SI.MultiLoc(keyName, false), cache, 0, partitionIdBytes);
+    var partitionIdBytes : seq<uint8> :- expect SI.GenerateUuidBytes();
+
+    // Create a random logicalKeyStoreNameBytes
+    // Ideally, this should be taken from the KeyStore version.keyStore,
+    // but logicalKeyStoreName variable doesn't exist in the
+    // trait AwsCryptographyKeyStoreTypes.IKeyStoreClient
+    // Therefore, the only way to get logicalKeyStoreName is
+    // to call GetKeyStoreInfo, which we don't need to do here
+    // since this method does NOT test the shared cache
+    // which is the only place logicalKeyStoreName is used
+    // (in the cache identifier)
+    var logicalKeyStoreNameBytes : seq<uint8> :- expect SI.GenerateUuidBytes();
+
+    return SI.KeySource(client, version.keyStore, SI.MultiLoc(keyName, false), cache, 0, partitionIdBytes, logicalKeyStoreNameBytes);
   }
 
   const SimpleItem : DDB.AttributeMap := map[

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
@@ -130,6 +130,7 @@ module
              (if tableConfig.keyring.Some? then tableConfig.keyring.value.Modifies else {})
              + (if tableConfig.cmm.Some? then tableConfig.cmm.value.Modifies else {})
              + (if tableConfig.legacyOverride.Some? then tableConfig.legacyOverride.value.encryptor.Modifies else {})
+             + (if tableConfig.search.Some? then tableConfig.search.value.versions[0].keyStore.Modifies else {})
            )
       :: o;
 
@@ -155,6 +156,7 @@ module
       assert SearchConfigToInfo.ValidSearchConfig(inputConfig.search);
       SearchInModifies(config, tableName);
       reveal SearchConfigToInfo.ValidSharedCache();
+      // TODO: remove assume axiom; this should be generated by smithy-dafny
       assume {:axiom} inputConfig.search.Some? ==> SearchConfigToInfo.ValidSharedCache(inputConfig.search.value.versions[0].keySource);
       var searchR := SearchConfigToInfo.Convert(inputConfig);
       var search :- searchR.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));

diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
@@ -526,8 +526,20 @@ module {:options "-functionSyntax:4"} JsonConfig {
     var client :- expect Primitives.AtomicPrimitives();
 
     // Create a test partitionIdBytes
-    var partitionIdBytes : seq<uint8> :- expect SI.GeneratePartitionId();
-    var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32, partitionIdBytes);
+    var partitionIdBytes : seq<uint8> :- expect SI.GenerateUuidBytes();
+
+    // Create a random logicalKeyStoreNameBytes
+    // Ideally, this should be taken from the KeyStore store,
+    // but logicalKeyStoreName variable doesn't exist in the
+    // trait AwsCryptographyKeyStoreTypes.IKeyStoreClient
+    // Therefore, the only way to get logicalKeyStoreName is
+    // to call GetKeyStoreInfo, which we don't need to do here
+    // since this method does NOT test the shared cache
+    // which is the only place logicalKeyStoreName is used
+    // (in the cache identifier)
+    var logicalKeyStoreNameBytes : seq<uint8> :- expect SI.GenerateUuidBytes();
+
+    var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32, partitionIdBytes, logicalKeyStoreNameBytes);
 
     var bv :- expect SI.MakeBeaconVersion(1, src, map[], map[], map[]);
     return Success(bv);