feat(SharedCache): Shared Cache for Searchable Encryption #1476
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -38,6 +38,9 @@ module SearchConfigToInfo { | |
| method Convert(outer : DynamoDbTableEncryptionConfig) | ||
| 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 {} | ||
|
Comment on lines
+41
to
+42
There was a problem hiding this comment. These are 0, is there any requirement that There was a problem hiding this comment. Yes, that is specified in a |
||
| 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) | ||
|
|
@@ -56,7 +59,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 beaconVersionConfig := outer.search.value.versions[0]; | ||
| var version :- ConvertVersion(outer, beaconVersionConfig); | ||
| var info := I.MakeSearchInfo(version); | ||
| return Success(Some(info)); | ||
| } | ||
|
|
@@ -74,6 +78,19 @@ module SearchConfigToInfo { | |
| forall b <- config.value.versions :: ValidBeaconVersion(b) | ||
| } | ||
|
|
||
| // Valid state of the provided shared cache, if it exists | ||
| predicate {:opaque} ValidSharedCache(config: BeaconKeySource) | ||
| { | ||
| && (&& config.single? | ||
| && config.single.cache.Some? | ||
| && config.single.cache.value.Shared? | ||
| ==> && config.single.cache.value.Shared.ValidState()) | ||
| && (&& config.multi? | ||
| && config.multi.cache.Some? | ||
| && config.multi.cache.value.Shared? | ||
| ==> && config.multi.cache.value.Shared.ValidState()) | ||
| } | ||
|
|
||
| // return true if, `keyFieldName` should be deleted from an item before writing | ||
| function method ShouldDeleteKeyField(outer : DynamoDbTableEncryptionConfig, keyFieldName : string) | ||
| : (ret : Result<bool, Error>) | ||
|
|
@@ -101,7 +118,10 @@ module SearchConfigToInfo { | |
| ) | ||
| returns (output : Result<I.KeySource, Error>) | ||
| modifies client.Modifies | ||
| modifies keyStore.Modifies | ||
| requires client.ValidState() | ||
| requires ValidSharedCache(config) | ||
RitvikKapila marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| ensures ValidSharedCache(config) | ||
| ensures client.ValidState() | ||
| ensures output.Success? ==> | ||
| && output.value.ValidState() | ||
|
|
@@ -119,18 +139,6 @@ module SearchConfigToInfo { | |
| && config.multi.keyFieldName in outer.attributeActionsOnEncrypt | ||
| && outer.attributeActionsOnEncrypt[config.multi.keyFieldName] == SE.ENCRYPT_AND_SIGN | ||
| ==> output.Failure? | ||
| { | ||
| // TODO-FutureCleanUp : https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1510 | ||
| // It is not-good that the MPL is initialized here; | ||
|
|
@@ -140,23 +148,36 @@ module SearchConfigToInfo { | |
| var mpl :- mplR.MapFailure(e => AwsCryptographyMaterialProviders(e)); | ||
|
|
||
| //= specification/searchable-encryption/search-config.md#key-store-cache | ||
| //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md) | ||
| //# MUST be created. | ||
| //# For a [Single Key Store](#single-key-store-initialization), either the user provides a cache, or we create a cache that MUST have [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) | ||
| //# equal to 1. If the user provides a cache which is not `Shared`, they SHOULD set the [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) | ||
| //# of the provided `CacheType` to 1, because the [Single Key Store](#single-key-store-initialization) only ever caches one entry. Even if the user provides an entryCapacity > 1, the [Single Key Store](#single-key-store-initialization) will only cache one entry. | ||
| //# For a [Multi Key Store](#multi-key-store-initialization), either the user provides a cache, or we create a cache that MUST have [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) | ||
| //# equal to 1000. | ||
| var cacheType : MPT.CacheType := | ||
| if config.multi? then | ||
| if config.multi.cache.Some? then | ||
| config.multi.cache.value | ||
| else | ||
| MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1000)) | ||
| else | ||
| if config.single.cache.Some? then | ||
| // If the user provides a CacheType, and it is NOT Shared, | ||
| // we SHOULD only allow an entryCapacity = 1 | ||
| // because the SingleKeyStore only ever caches one value. | ||
| // That is, we SHOULD add a check here for entryCapacity = 1. | ||
| // However, that requires us to write an if block for each CacheType. | ||
| // Also, it does NOT matter what the entryCapacity is, because the cache | ||
| // can only hold one element at a time. | ||
| config.single.cache.value | ||
| else | ||
| MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1)); | ||
|
|
||
| var cache; | ||
| if cacheType.Shared? { | ||
| cache := cacheType.Shared; | ||
| reveal ValidSharedCache(config); | ||
| } else { | ||
| //= specification/searchable-encryption/search-config.md#key-store-cache | ||
| //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md) | ||
|
|
@@ -168,20 +189,59 @@ module SearchConfigToInfo { | |
| cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e)); | ||
| } | ||
|
|
||
| var partitionIdBytes : seq<uint8>; | ||
|
|
||
| if config.multi? && config.multi.partitionId.Some? { | ||
| partitionIdBytes :- UTF8.Encode(config.multi.partitionId.value) | ||
| .MapFailure( | ||
| e => Error.DynamoDbEncryptionException( | ||
| message := "Could not UTF-8 Encode Partition ID from MultiKeyStore: " + e | ||
| ) | ||
| ); | ||
| } | ||
| else if config.single? && config.single.partitionId.Some? { | ||
| partitionIdBytes :- UTF8.Encode(config.single.partitionId.value) | ||
| .MapFailure( | ||
| e => Error.DynamoDbEncryptionException( | ||
| message := "Could not UTF-8 Encode Partition ID from SingleKeyStore: " + e | ||
| ) | ||
| ); | ||
| } | ||
| else { | ||
| partitionIdBytes :- I.GenerateUuidBytes(); | ||
| } | ||
RitvikKapila marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| var getKeyStoreInfoOutput? := keyStore.GetKeyStoreInfo(); | ||
| var getKeyStoreInfoOutput :- getKeyStoreInfoOutput?.MapFailure(e => Error.AwsCryptographyKeyStore(e)); | ||
| var logicalKeyStoreName : string := getKeyStoreInfoOutput.logicalKeyStoreName; | ||
RitvikKapila marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| 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, 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, logicalKeyStoreNameBytes)); | ||
| } | ||
| assert output.value.ValidState() by { | ||
| // This axiom is important because it is not easy to prove | ||
| // keyStore.Modifies !! cache.Modifies for a shared cache. | ||
| assume {:axiom} keyStore.Modifies !! cache.Modifies; | ||
| } | ||
| } | ||
|
|
||
| // convert configured BeaconVersion to internal BeaconVersion | ||
| method ConvertVersion(outer : DynamoDbTableEncryptionConfig, config : BeaconVersion) | ||
| returns (output : Result<I.ValidBeaconVersion, Error>) | ||
| requires ValidBeaconVersion(config) | ||
| requires ValidSharedCache(config.keySource) | ||
RitvikKapila marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| modifies config.keyStore.Modifies | ||
RitvikKapila marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| ensures ValidSharedCache(config.keySource) | ||
| ensures output.Success? ==> | ||
| && output.value.ValidState() | ||
| && fresh(output.value.keySource.client) | ||
|
|
||
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.