diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index ed3aa1f86..2712ba605 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy +++ b/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 := Option.None + nameonly cache: Option := Option.None , + nameonly partitionId: Option := 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: int32 , + nameonly cache: Option := Option.None , + nameonly partitionId: Option := Option.None ) datatype StandardBeacon = | StandardBeacon ( nameonly name: string , diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy index 5fe39b13d..87716dcc5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy @@ -708,6 +708,8 @@ structure KeyStoreReference {} //# On initialization of a Single Key Store, the caller MUST provide: //# - [Beacon Key Id](#beacon-key-id) //# - [cacheTTL](#cachettl) +//# - [cache](#key-store-cache) +//# - [partition-id](#partition-id) @javadoc("The configuration for using a single Beacon Key.") structure SingleKeyStore { @@ -717,6 +719,10 @@ structure SingleKeyStore { @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.") cacheTTL: Integer, + @documentation("Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore.") + cache : CacheType, + @documentation("Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.") + partitionId: String } //= specification/searchable-encryption/search-config.md#multi-key-store-initialization @@ -724,7 +730,8 @@ structure SingleKeyStore { //# On initialization of a Multi Key Store, the caller MUST provide: //# - [Beacon Key Field Name](#beacon-key-field-name) //# - [cacheTTL](#cachettl) -//# - [max cache size](#max-cache-size) +//# - [cache](#key-store-cache) +//# - [partition-id](#partition-id) @javadoc("The configuration for using multiple Beacon Keys.") structure MultiKeyStore { @@ -735,7 +742,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 distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.") + partitionId: String } //= specification/searchable-encryption/search-config.md#beacon-key-source diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 916005d6e..6e974d03c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -38,6 +38,9 @@ module SearchConfigToInfo { method Convert(outer : DynamoDbTableEncryptionConfig) returns (output : Result, 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 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 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)); } @@ -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) @@ -101,7 +118,10 @@ module SearchConfigToInfo { ) returns (output : Result) modifies client.Modifies + modifies keyStore.Modifies requires client.ValidState() + requires ValidSharedCache(config) + 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? - // Not in Spec, but for now, SE does not support the Shared Cache Type - ensures - && config.multi? - && config.multi.cache.Some? - && config.multi.cache.value.Shared? - ==> - && output.Failure? - // If the failure was NOT caused by booting up the MPL - && !output.error.AwsCryptographyMaterialProviders? - ==> - && output.error.DynamoDbEncryptionException? - && output.error.message == "Searchable Encryption does not support the Shared Cache type at this time." { // 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,35 @@ module SearchConfigToInfo { var mpl :- mplR.MapFailure(e => AwsCryptographyMaterialProviders(e)); //= specification/searchable-encryption/search-config.md#key-store-cache - //# For a [Single Key Store](#single-key-store-initialization) the [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) - //# MUST be 1 - //# For a [Multi Key Store](#multi-key-store-initialization) the [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) - //# MUST be key store's max cache size. + //# 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 has [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) + //# equal to 1. + //# For a [Multi Key Store](#multi-key-store-initialization), either the user provides a cache, or we create a cache that has [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? { - return Failure(DynamoDbEncryptionException(message:="Searchable Encryption does not support the Shared Cache type at this time.")); - // cache := 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,13 +188,49 @@ module SearchConfigToInfo { cache :- maybeCache.MapFailure(e => AwsCryptographyMaterialProviders(e)); } + var partitionIdBytes : seq; + + 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(); + } + var getKeyStoreInfoOutput? := keyStore.GetKeyStoreInfo(); + var getKeyStoreInfoOutput :- getKeyStoreInfoOutput?.MapFailure(e => Error.AwsCryptographyKeyStore(e)); + var logicalKeyStoreName : string := getKeyStoreInfoOutput.logicalKeyStoreName; + var logicalKeyStoreNameBytes : seq :- 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)); + 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)); + 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; } } @@ -182,6 +238,9 @@ module SearchConfigToInfo { method ConvertVersion(outer : DynamoDbTableEncryptionConfig, config : BeaconVersion) returns (output : Result) requires ValidBeaconVersion(config) + requires ValidSharedCache(config.keySource) + modifies config.keyStore.Modifies + ensures ValidSharedCache(config.keySource) 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 index 92a730fad..bedbe19c7 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy @@ -26,6 +26,9 @@ module SearchableEncryptionInfo { import MP = AwsCryptographyMaterialProvidersTypes import KeyStoreTypes = AwsCryptographyKeyStoreTypes import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes + import opened CacheConstants + import UUID + import Digest //= specification/searchable-encryption/search-config.md#version-number //= type=implication @@ -40,6 +43,7 @@ module SearchableEncryptionInfo { requires Seq.HasNoDuplicates(stdNames) modifies client.Modifies requires client.ValidState() + ensures client.History.Digest == old(client.History.Digest) ensures client.ValidState() { var newKeys :- GetHmacKeys(client, stdNames, stdNames, key); @@ -58,6 +62,7 @@ module SearchableEncryptionInfo { requires Seq.HasNoDuplicates(keysLeft) requires forall k <- allKeys :: k in keysLeft || k in acc requires forall k <- keysLeft :: k in allKeys + ensures client.History.Digest == old(client.History.Digest) ensures output.Success? ==> forall k <- allKeys :: k in output.value modifies client.Modifies requires client.ValidState() @@ -86,6 +91,7 @@ module SearchableEncryptionInfo { modifies client.Modifies requires client.ValidState() ensures client.ValidState() + ensures client.History.Digest == old(client.History.Digest) ensures output.Success? ==> && var fullName := "AWS_DBE_SCAN_BEACON" + name; @@ -127,6 +133,18 @@ module SearchableEncryptionInfo { return Success(newKey); } + // Generates a new random UUID converted to UTF8 bytes + method GenerateUuidBytes() returns (output : Result, Error>) + { + var uuid? := UUID.GenerateUUID(); + + var uuid :- uuid? + .MapFailure(e => Error.DynamoDbEncryptionException(message := e)); + + output := UUID.ToByteArray(uuid) + .MapFailure(e => Error.DynamoDbEncryptionException(message := e)); + } + datatype KeyLocation = | LiteralLoc (keys: HmacKeyMap) | SingleLoc (keyId: string) @@ -137,13 +155,18 @@ module SearchableEncryptionInfo { store : ValidStore, keyLoc : KeyLocation, cache : MP.ICryptographicMaterialsCache, - cacheTTL : uint32 + cacheTTL : uint32, + partitionIdBytes : seq, + logicalKeyStoreNameBytes : seq ) { function Modifies() : set { - client.Modifies + store.Modifies + client.Modifies + store.Modifies + cache.Modifies } predicate ValidState() { - client.ValidState() && store.ValidState() + && client.ValidState() + && store.ValidState() + && cache.ValidState() + && store.Modifies !! cache.Modifies } method getKeyMap(stdNames : seq, keyId : MaybeKeyId) returns (output : Result) requires Seq.HasNoDuplicates(stdNames) @@ -153,7 +176,16 @@ module SearchableEncryptionInfo { { if keyLoc.SingleLoc? { :- Need(keyId.DontUseKeyId?, E("KeyID should not be supplied with a SingleKeyStore")); - var theMap :- getKeysCache(stdNames, keyLoc.keyId); + var now := Time.GetCurrent(); + var theMap :- getKeysCache( + client, + 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")); @@ -161,9 +193,20 @@ module SearchableEncryptionInfo { return Success(Keys(theMap)); } else { match keyId { - case DontUseKeyId => return Failure(E("KeyID must not be supplied with a MultiKeyStore")); + case DontUseKeyId => return Failure(E("Fixed 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 now := Time.GetCurrent(); + var theMap :- getKeysCache( + client, + stdNames, + id, + cacheTTL as MP.PositiveLong, + partitionIdBytes, + logicalKeyStoreNameBytes, + now as MP.PositiveLong + ); + return Success(Keys(theMap)); } } } @@ -180,41 +223,76 @@ module SearchableEncryptionInfo { return Success(keyLoc.keys); } + // Checks if (time_now - cache creation time of the extracted cache entry) is less than the allowed + // TTL of the current Beacon Key Source calling the getEntry method from the cache. + // Mitigates risk if another Beacon Key Source wrote the entry with a longer TTL. + predicate method cacheEntryWithinLimits( + creationTime: MP.PositiveLong, + now: MP.PositiveLong, + ttlSeconds: MP.PositiveLong + ): (output: bool) + { + now - creationTime <= ttlSeconds as MP.PositiveLong + } + method getKeysCache( + client : Primitives.AtomicPrimitivesClient, stdNames : seq, - keyId : string + keyId : string, + cacheTTL : MP.PositiveLong, + partitionIdBytes : seq, + logicalKeyStoreNameBytes : seq, + now : MP.PositiveLong ) returns (output : Result) requires Seq.HasNoDuplicates(stdNames) requires ValidState() + requires client.ValidState() modifies Modifies() + modifies client.Modifies ensures ValidState() + ensures client.ValidState() //= specification/searchable-encryption/search-config.md#get-beacon-key-materials //= type=implication //# Get beacon key MUST Call the associated [Key Store Cache](#key-store-cache) //# [Get Cache Entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#get-cache-entry) - //# with the `beacon key id`. + //# with the cache identifier defined in the [Searchable Encryption Cache Identifier](#searchable-encryption-cache-identifier) section. ensures output.Success? ==> - && var oldHistory := old(cache.History.GetCacheEntry); - && var newHistory := cache.History.GetCacheEntry; - && |newHistory| == |oldHistory|+1 - && Seq.Last(newHistory).output.Success? - && var cacheInput := Seq.Last(newHistory).input; - && var cacheOutput := Seq.Last(newHistory).output; + && var oldGetCacheHistory := old(cache.History.GetCacheEntry); + && var newGetCacheHistory := cache.History.GetCacheEntry; + && |newGetCacheHistory| == |oldGetCacheHistory|+1 + && var getCacheInput := Seq.Last(newGetCacheHistory).input; + && var getCacheOutput := Seq.Last(newGetCacheHistory).output; && UTF8.Encode(keyId).Success? - && cacheInput.identifier == UTF8.Encode(keyId).value + + && var oldClientHistory := old(client.History.Digest); + && var newClientHistory := client.History.Digest; + && |newClientHistory| == |oldClientHistory|+1 + && var identifier := RESOURCE_ID_HIERARCHICAL_KEYRING + NULL_BYTE + SCOPE_ID_SEARCHABLE_ENCRYPTION + NULL_BYTE + partitionIdBytes + NULL_BYTE + logicalKeyStoreNameBytes + NULL_BYTE + UTF8.Encode(keyId).value; + && var digestInput := Seq.Last(newClientHistory).input; + && var digestOutput := Seq.Last(newClientHistory).output; + && digestInput.message == identifier + && (digestOutput.Success? ==> (getCacheInput.identifier == digestOutput.value)) //= specification/searchable-encryption/search-config.md#get-beacon-key-materials //= type=implication //# If a [cache entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#cache-entry) //# exists, get beacon key MUST return the [entry materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#materials). - && (cacheOutput.Success? ==> - && cacheOutput.value.materials.BeaconKey? - && cacheOutput.value.materials.BeaconKey.hmacKeys.Some? - && output.value == cacheOutput.value.materials.BeaconKey.hmacKeys.value) - - && (cacheOutput.Failure? ==> + && (getCacheOutput.Success? && cacheEntryWithinLimits( + creationTime := getCacheOutput.value.creationTime, + now := now, + ttlSeconds := cacheTTL + ) ==> + && getCacheOutput.value.materials.BeaconKey? + && getCacheOutput.value.materials.BeaconKey.hmacKeys.Some? + && output.value == getCacheOutput.value.materials.BeaconKey.hmacKeys.value) + + && (getCacheOutput.Failure? || !cacheEntryWithinLimits( + creationTime := getCacheOutput.value.creationTime, + now := now, + ttlSeconds := cacheTTL + ) ==> && var oldGetHistory := old(store.History.GetBeaconKey); && var newGetHistory := store.History.GetBeaconKey; && |newGetHistory| == |oldGetHistory|+1 @@ -228,32 +306,84 @@ module SearchableEncryptionInfo { //= type=implication //# The `beacon key id` MUST be passed to the configured `KeyStore`'s `GetBeaconKey` operation. && storeInput.branchKeyIdentifier == keyId - && var oldPutHistory := old(cache.History.PutCacheEntry); - && var newPutHistory := cache.History.PutCacheEntry; - && |newPutHistory| == |oldPutHistory|+1 - && Seq.Last(newPutHistory).output.Success? - && var storeInput := Seq.Last(newPutHistory).input; - && var storeOutput := Seq.Last(newPutHistory).output; + && var oldPutCacheHistory := old(cache.History.PutCacheEntry); + && var newPutCacheHistory := cache.History.PutCacheEntry; + && |newPutCacheHistory| == |oldPutCacheHistory|+1 + && ( + var putCacheOutput := Seq.Last(newPutCacheHistory).output; + || putCacheOutput.Success? + || putCacheOutput.error.EntryAlreadyExists? + ) + && var putCacheInput := Seq.Last(newPutCacheHistory).input; + && var putCacheOutput := Seq.Last(newPutCacheHistory).output; + + //= specification/searchable-encryption/search-config.md#get-beacon-key-materials + //# The Searchable Encryption cache identifier + //# used to [Put Cache Entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#put-cache-entry) + //# MUST be the same + //# as the identifier that was used to attempt [Get Cache Entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#get-cache-entry). + && putCacheInput.identifier == getCacheInput.identifier + //= specification/searchable-encryption/search-config.md#get-beacon-key-materials //= type=implication //# These cached materials MUST be returned. - && storeInput.materials.BeaconKey.hmacKeys == Some(output.value) - + && (putCacheInput.materials.BeaconKey? ==> putCacheInput.materials.BeaconKey.hmacKeys == Some(output.value)) ) { + + // Resource ID: Hierarchical Keyring [0x02] + var resourceId : seq := RESOURCE_ID_HIERARCHICAL_KEYRING; + + // Scope ID: Searchable Encryption [0x03] + var scopeId : seq := SCOPE_ID_SEARCHABLE_ENCRYPTION; + + // Create the Suffix var keyIdBytesR := UTF8.Encode(keyId); var keyIdBytes :- keyIdBytesR.MapFailure(e => E(e)); - var getCacheInput := MP.GetCacheEntryInput(identifier := keyIdBytes, bytesUsed := None); + var suffix : seq := 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; + + // Take a SHA384 of the cache identifier + var hashAlgorithm := Prim.DigestAlgorithm.SHA_384; + + var identifierDigestInput := Prim.DigestInput( + digestAlgorithm := hashAlgorithm, message := identifier + ); + var maybeCacheDigest := client.Digest(identifierDigestInput); + var cacheDigest :- maybeCacheDigest.MapFailure(e => AwsCryptographyPrimitives(e)); + + // Use the SHA384 of the identifier as the cache identifier + var getCacheInput := MP.GetCacheEntryInput(identifier := cacheDigest, bytesUsed := None); verifyValidStateCache(cache); - assume {:axiom} cache.Modifies == {}; var getCacheOutput := cache.GetCacheEntry(getCacheInput); - // If error is not EntryDoesNotExist, return failure if (getCacheOutput.Failure? && !getCacheOutput.error.EntryDoesNotExist?) { return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=getCacheOutput.error)); } - if getCacheOutput.Failure? { + assert + && |client.History.Digest| == |old(client.History.Digest)| + 1 + && Seq.Last(client.History.Digest).input.message == identifier + && Seq.Last(cache.History.GetCacheEntry).input.identifier == Seq.Last(client.History.Digest).output.value + by { + assume{:axiom} client.Modifies !! cache.Modifies; + } + + //= specification/searchable-encryption/search-config.md#get-beacon-key-materials + //# If using a `Shared` cache across multiple [Beacon Key Sources](#beacon-key-source), + //# different [Beacon Key Sources](#beacon-key-source) having the same `beaconKey` can have different TTLs. + //# In such a case, the expiry time in the cache is set according to the [Beacon Key Source](#beacon-key-source) that populated the cache. + //# There MUST be a check (cacheEntryWithinLimits) to make sure that for the cache entry found, who's TTL has NOT expired, + //# `time.now() - cacheEntryCreationTime <= ttlSeconds` is true and + //# valid for TTL of the [Beacon Key Source](#beacon-key-source) getting the cache entry. + //# If this is NOT true, then we MUST treat the cache entry as expired. + if getCacheOutput.Failure? || !cacheEntryWithinLimits( + creationTime := getCacheOutput.value.creationTime, + now := now, + ttlSeconds := cacheTTL + ) { //= specification/searchable-encryption/search-config.md#beacon-keys //# Beacon keys MUST be obtained from the configured [Beacon Key Source](#beacon-key-source). var maybeRawBeaconKeyMaterials := store.GetBeaconKey( @@ -261,6 +391,13 @@ module SearchableEncryptionInfo { branchKeyIdentifier := keyId ) ); + assert + && |client.History.Digest| == |old(client.History.Digest)| + 1 + && Seq.Last(client.History.Digest).input.message == identifier + && Seq.Last(cache.History.GetCacheEntry).input.identifier == Seq.Last(client.History.Digest).output.value + by { + assume{:axiom} client.Modifies !! store.Modifies; + } var rawBeaconKeyMaterials :- maybeRawBeaconKeyMaterials .MapFailure(e => AwsCryptographyKeyStore(AwsCryptographyKeyStore := e)); @@ -269,27 +406,33 @@ module SearchableEncryptionInfo { var keyMap :- getAllKeys(stdNames, key.value); var beaconKeyMaterials := rawBeaconKeyMaterials.beaconKeyMaterials.(beaconKey := None, hmacKeys := Some(keyMap)); + expect now < UInt.BoundedInts.INT64_MAX - cacheTTL; //= specification/searchable-encryption/search-config.md#get-beacon-key-materials //# These materials MUST be put into the associated [Key Store Cache](#key-store-cache) //# with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time) //# equal to now + configured [cacheTTL](#cachettl). - var now := Time.GetCurrent(); var putCacheEntryInput:= MP.PutCacheEntryInput( - identifier := keyIdBytes, + identifier := cacheDigest, materials := MP.Materials.BeaconKey(beaconKeyMaterials), creationTime := now, - expiryTime := now+cacheTTL as MP.PositiveLong, + expiryTime := now + cacheTTL, messagesUsed := None, bytesUsed := None ); verifyValidStateCache(cache); - assume {:axiom} cache.Modifies == {}; var putResult := cache.PutCacheEntry(putCacheEntryInput); if (putResult.Failure? && !putResult.error.EntryAlreadyExists?) { return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=putResult.error)); } + assert + && |client.History.Digest| == |old(client.History.Digest)| + 1 + && Seq.Last(client.History.Digest).input.message == identifier + && Seq.Last(cache.History.GetCacheEntry).input.identifier == Seq.Last(client.History.Digest).output.value + by { + assume{:axiom} client.Modifies !! cache.Modifies; + } return Success(keyMap); } else { :- Need( @@ -307,6 +450,7 @@ module SearchableEncryptionInfo { requires Seq.HasNoDuplicates(stdNames) modifies client.Modifies requires client.ValidState() + ensures client.History.Digest == old(client.History.Digest) ensures client.ValidState() { output := GetAllKeys(client, stdNames, key); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy index f839c551d..b0ec519f3 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy +++ b/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 = diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index 7c4391d40..a812cdc0e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -105,6 +105,231 @@ module TestBaseBeacon { expect goodAttrs["aws_dbe_b_std2"] == newAttrs["aws_dbe_b_std2"]; } + method {:test} TestSharedCacheBeaconsSingleKeyStoreWithSamePartitionId() + { + var partitionId : string := "partitionId"; + var sharedCache : MPT.CacheType := GetSharedCache(); + var primitives :- expect Primitives.AtomicPrimitives(); + + // Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes + // Dafny is working on a fix. Update this test when Dafny releases `4.9.2`. + // Using `assume{:axiom} false;` for this test for now. + // var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by { + // assume {:axiom} C.ValidSharedCache(version.keySource); + // } + // var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + // var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by { + // assume{:axiom} false; + // } + assume{:axiom} false; + + // This call is expected to fail because we are providing a Bad KeyStore which does NOT exist + var badVersion := GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionId)); + var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); + var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + expect badAttrs.Failure?; + + // This is expected to pass because we pass a valid KeyStore + var version := GetLotsaBeaconsSingleWithSharedCache(cache := sharedCache, partitionId := Some(partitionId)); + var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); + var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + + // This is expected to pass now because the cache already has cached material for this Branch Key ID. + // This is a hack to test that the correct material is cached. + var badAttrsNowCached :- expect badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + } + + method {:test} TestSharedCacheBeaconsSingleKeyStoreWithDifferentPartitionId() + { + var sharedCache : MPT.CacheType := GetSharedCache(); + var primitives :- expect Primitives.AtomicPrimitives(); + + // Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes + // Dafny is working on a fix. Update this test when Dafny releases `4.9.2`. + // Using `assume{:axiom} false;` for this test for now. + // var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by { + // assume {:axiom} C.ValidSharedCache(version.keySource); + // } + // var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + // var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by { + // assume{:axiom} false; + // } + assume{:axiom} false; + + // This call is expected to fail because we are providing a Bad KeyStore which does NOT exist + var partitionIdBadVersion : string := "partitionIdBadVersion"; + var badVersion := GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionIdBadVersion)); + var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); + var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + expect badAttrs.Failure?; + + // This is expected to pass because we pass a valid KeyStore + var partitionIdGoodVersion : string := "partitionIdGoodVersion"; + var version := GetLotsaBeaconsSingleWithSharedCache(cache := sharedCache, partitionId := Some(partitionIdGoodVersion)); + var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); + var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + + // This is still expected to fail because the partitionId for the cached material is different. + var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + expect badAttrsNowCached.Failure?; + } + + method {:test} TestSharedCacheBeaconsSingleKeyStoreWithUnspecifiedPartitionId() + { + var sharedCache : MPT.CacheType := GetSharedCache(); + var primitives :- expect Primitives.AtomicPrimitives(); + + // Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes + // Dafny is working on a fix. Update this test when Dafny releases `4.9.2`. + // Using `assume{:axiom} false;` for this test for now. + // var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by { + // assume {:axiom} C.ValidSharedCache(version.keySource); + // } + // var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + // var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by { + // assume{:axiom} false; + // } + assume{:axiom} false; + + // This call is expected to fail because we are providing a Bad KeyStore which does NOT exist + var badVersion := GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := None); + var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); + var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + expect badAttrs.Failure?; + + // This is expected to pass because we pass a valid KeyStore + var version := GetLotsaBeaconsSingleWithSharedCache(cache := sharedCache, partitionId := None); + var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); + var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + + // This is still expected to fail because the partitionId for the cached material is different. + // If the user does NOT specify the partitionId, it is set to a random UUID + var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + expect badAttrsNowCached.Failure?; + } + + method {:test} TestSharedCacheBeaconsMultiKeyStoreWithSamePartitionId() + { + var partitionId : string := "partitionId"; + var sharedCache : MPT.CacheType := GetSharedCache(); + var primitives :- expect Primitives.AtomicPrimitives(); + + // Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes + // Dafny is working on a fix. Update this test when Dafny releases `4.9.2`. + // Using `assume{:axiom} false;` for this test for now. + // var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by { + // assume {:axiom} C.ValidSharedCache(version.keySource); + // } + // var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + // var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by { + // assume{:axiom} false; + // } + assume{:axiom} false; + + // This call is expected to fail because we are providing a Bad KeyStore which does NOT exist + var badVersion := GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionId)); + var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); + var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + expect badAttrs.Failure?; + + // This is expected to pass because we pass a valid KeyStore + var version := GetLotsaBeaconsMultiWithSharedCache(cache := sharedCache, partitionId := Some(partitionId)); + var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); + var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + + // This is expected to pass now because the cache already has cached material for this Branch Key ID. + // This is a hack to test that the correct material is cached. + var badAttrsNowCached :- expect badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + } + + + method {:test} TestSharedCacheBeaconsMultiKeyStoreWithDifferentPartitionId() + { + var sharedCache : MPT.CacheType := GetSharedCache(); + var primitives :- expect Primitives.AtomicPrimitives(); + + // Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes + // Dafny is working on a fix. Update this test when Dafny releases `4.9.2`. + // Using `assume{:axiom} false;` for this test for now. + // var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by { + // assume {:axiom} C.ValidSharedCache(version.keySource); + // } + // var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + // var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by { + // assume{:axiom} false; + // } + assume{:axiom} false; + + // This call is expected to fail because we are providing a Bad KeyStore which does NOT exist + var partitionIdBadVersion : string := "partitionIdBadVersion"; + var badVersion := GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionIdBadVersion)); + var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); + var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); + // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable. + // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy, + // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource. + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + expect badAttrs.Failure?; + + // This is expected to pass because we pass a valid KeyStore + var partitionIdGoodVersion : string := "partitionIdGoodVersion"; + var version := GetLotsaBeaconsMultiWithSharedCache(cache := sharedCache, partitionId := Some(partitionIdGoodVersion)); + var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); + var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + + // This is still expected to fail because the partitionId for the cached material is different. + var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + expect badAttrsNowCached.Failure?; + } + + method {:test} TestSharedCacheBeaconsMultiKeyStoreWithUnspecifiedPartitionId() + { + var sharedCache : MPT.CacheType := GetSharedCache(); + var primitives :- expect Primitives.AtomicPrimitives(); + + // Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes + // Dafny is working on a fix. Update this test when Dafny releases `4.9.2`. + // Using `assume{:axiom} false;` for this test for now. + // var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by { + // assume {:axiom} C.ValidSharedCache(version.keySource); + // } + // var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + // var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by { + // assume{:axiom} false; + // } + assume{:axiom} false; + + // This call is expected to fail because we are providing a Bad KeyStore which does NOT exist + var badVersion := GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := None); + var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); + var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); + // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable. + // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy, + // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource. + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + expect badAttrs.Failure?; + + // This is expected to pass because we pass a valid KeyStore + var version := GetLotsaBeaconsMultiWithSharedCache(cache := sharedCache, partitionId := None); + var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); + var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + + // This is still expected to fail because the partitionId for the cached material is different. + // If the user does NOT specify the partitionId, it is set to a random UUID + var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + expect badAttrsNowCached.Failure?; + } + method {:test} TestBeaconValues() { var version := GetLotsaBeacons(); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index bbf448e00..2b16f9c8b 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy @@ -141,6 +141,37 @@ module BeaconTestFixtures { return store; } + // Method to create a bad keyStore with the same LogicalKeyStoreName as + // the keyStore generated by the GetKeyStore method + // Used in the Shared Cache to verify cache hits + // If the bv.GenerateEncryptedBeacons() method succeeds in Beacon.dfy + // with even the bad keyStore, that verifies that there's a cache hit. + method GetBadKeyStore() returns (output : SI.ValidStore) + ensures fresh(output.Modifies) + { + var kmsClient :- expect KMS.KMSClient(); + var ddbClient :- expect DDBC.DynamoDBClient(); + // This is the bad-arn key which does NOT exist. + var kmsConfig := KTypes.KMSConfiguration.kmsKeyArn( + "arn:aws:kms:us-west-2:370957321024:key/bad-arn" + ); + var keyStoreConfig := KTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + // This needs to be the same as logicalKeyStoreName of KeyStore + // generated by GetKeyStore to have the same cache identifier. + logicalKeyStoreName := "KeyStoreDdbTable", + grantTokens := None, + // This is the bad-table-name which does NOT exist. + ddbTableName := "bad-table-name", + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClient) + ); + + var store :- expect KeyStore.KeyStore(keyStoreConfig); + return store; + } + method GetEmptyBeacons() returns (output : BeaconVersion) ensures output.keyStore.ValidState() ensures fresh(output.keyStore.Modifies) @@ -198,6 +229,122 @@ module BeaconTestFixtures { ); } + method GetLotsaBeaconsSingleWithSharedCache(cache: MPT.CacheType, partitionId: Option) returns (output : BeaconVersion) + ensures output.keyStore.ValidState() + ensures fresh(output.keyStore.Modifies) + ensures output.version == 1 + ensures + && output.keySource.single? + && output.keySource.single.cache.Some? + && output.keySource.single.cache.value == cache + { + var store := GetKeyStore(); + return BeaconVersion ( + version := 1, + keyStore := store, + // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable. + // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy, + // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource. + keySource := single(SingleKeyStore(keyId := "040a32a8-3737-4f16-a3ba-bd4449556d73", cacheTTL := 42, cache := Some(cache), partitionId := partitionId)), + standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB], + compoundBeacons := Some([NameTitle, YearName, Mixed, JustSigned]), + virtualFields := Some([NameTitleField]), + encryptedParts := None, + signedParts := None + ); + } + + method GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache: MPT.CacheType, partitionId: Option) returns (output : BeaconVersion) + ensures output.keyStore.ValidState() + ensures fresh(output.keyStore.Modifies) + ensures output.version == 1 + ensures + && output.keySource.single? + && output.keySource.single.cache.Some? + { + var store := GetBadKeyStore(); + return BeaconVersion ( + version := 1, + keyStore := store, + // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable. + // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy, + // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource. + // Even though this method creates a BeaconVersion with a Bad Key Store which does NOT exist, + // we need the keyId to be valid for the cache to pick up the correct material to confirm a cache hit in + // the test TestSharedCacheBeaconsSingleKeyStore in Beacon.dfy + keySource := single(SingleKeyStore(keyId := "040a32a8-3737-4f16-a3ba-bd4449556d73", cacheTTL := 42, cache := Some(cache), partitionId := partitionId)), + standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB], + compoundBeacons := Some([NameTitle, YearName, Mixed, JustSigned]), + virtualFields := Some([NameTitleField]), + encryptedParts := None, + signedParts := None + ); + } + + method GetLotsaBeaconsMultiWithSharedCache(cache: MPT.CacheType, partitionId: Option) returns (output : BeaconVersion) + ensures output.keyStore.ValidState() + ensures fresh(output.keyStore.Modifies) + ensures output.version == 1 + ensures + && output.keySource.multi? + && output.keySource.multi.cache.Some? + { + var store := GetKeyStore(); + return BeaconVersion ( + version := 1, + keyStore := store, + keySource := multi(MultiKeyStore(keyFieldName := "TheKeyField", cacheTTL := 42, cache := Some(cache), partitionId := partitionId)), + standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB], + compoundBeacons := Some([NameTitle, YearName, Mixed, JustSigned]), + virtualFields := Some([NameTitleField]), + encryptedParts := None, + signedParts := None + ); + } + + method GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache: MPT.CacheType, partitionId: Option) returns (output : BeaconVersion) + ensures output.keyStore.ValidState() + ensures fresh(output.keyStore.Modifies) + ensures output.version == 1 + ensures + && output.keySource.multi? + && output.keySource.multi.cache.Some? + { + var store := GetBadKeyStore(); + return BeaconVersion ( + version := 1, + keyStore := store, + keySource := multi(MultiKeyStore(keyFieldName := "TheKeyField", cacheTTL := 42, cache := Some(cache), partitionId := partitionId)), + standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB], + compoundBeacons := Some([NameTitle, YearName, Mixed, JustSigned]), + virtualFields := Some([NameTitleField]), + encryptedParts := None, + signedParts := None + ); + } + + method GetSharedCache() + returns (cache: MPT.CacheType) + ensures cache.Shared? && fresh(cache.Shared.Modifies) + { + var mpl :- expect MaterialProviders.MaterialProviders(); + // Initialize the shared Cryptographic Materials Cache + var sharedCache :- expect mpl.CreateCryptographicMaterialsCache( + MPT.CreateCryptographicMaterialsCacheInput( + cache := MPT.CacheType.Default( + MPT.DefaultCache( + entryCapacity := 100 + ) + ) + ) + ); + + // Wrap the initialized shared Cryptographic Materials Cache as a `Shared` CacheType object + cache := MPT.CacheType.Shared( + sharedCache + ); + } + const EmptyTableConfig := DynamoDbTableEncryptionConfig ( logicalTableName := "Foo", partitionKeyName := "foo", @@ -231,6 +378,9 @@ module BeaconTestFixtures { ensures output.ValidState() ensures version.keyStore == output.store ensures fresh(output.client.Modifies) + ensures + && fresh(output.cache) + && fresh(output.cache.Modifies) { var client :- expect Primitives.AtomicPrimitives(); @@ -242,7 +392,21 @@ module BeaconTestFixtures { cache := MPT.Default(Default := MPT.DefaultCache(entryCapacity := 3)) ); var cache :- expect mpl.CreateCryptographicMaterialsCache(input); - return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0); + // Create a test partitionIdBytes + var partitionIdBytes : seq :- 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 :- 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) @@ -250,6 +414,9 @@ module BeaconTestFixtures { ensures output.ValidState() ensures version.keyStore == output.store ensures fresh(output.client.Modifies) + ensures + && fresh(output.cache) + && fresh(output.cache.Modifies) { var client :- expect Primitives.AtomicPrimitives(); var mpl :- expect MaterialProviders.MaterialProviders(); @@ -257,7 +424,21 @@ module BeaconTestFixtures { cache := MPT.Default(Default := MPT.DefaultCache(entryCapacity := 3)) ); var cache :- expect mpl.CreateCryptographicMaterialsCache(input); - return SI.KeySource(client, version.keyStore, SI.MultiLoc(keyName, false), cache, 0); + // Create a test partitionIdBytes + var partitionIdBytes : seq :- 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 :- 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/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy index 123b5917e..de056cf74 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy @@ -773,93 +773,127 @@ 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() - modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true - && t7.keyring.Some? - :: t7.keyring.value, - obj <- tmps7.Modifies | obj in tmps7.Modifies :: obj - modifies set tmps8 <- set t8 <- config.tableEncryptionConfigs.Values | true - && t8.cmm.Some? - :: t8.cmm.value, - obj <- tmps8.Modifies | obj in tmps8.Modifies :: obj + tmp6.keySource.single? ==> + tmp6.keySource.single.cache.Some? ==> + tmp6.keySource.single.cache.value.Shared? ==> + tmp6.keySource.single.cache.value.Shared.ValidState() + requires var tmps7 := set t7 | t7 in config.tableEncryptionConfigs.Values; + forall tmp7 :: tmp7 in tmps7 ==> + tmp7.search.Some? ==> + var tmps8 := set t8 | t8 in tmp7.search.value.versions; + forall tmp8 :: tmp8 in tmps8 ==> + tmp8.keySource.multi? ==> + tmp8.keySource.multi.cache.Some? ==> + tmp8.keySource.multi.cache.value.Shared? ==> + tmp8.keySource.multi.cache.value.Shared.ValidState() modifies set tmps9 <- set t9 <- config.tableEncryptionConfigs.Values | true - && t9.legacyOverride.Some? - :: t9.legacyOverride.value.encryptor, + && t9.keyring.Some? + :: t9.keyring.value, obj <- tmps9.Modifies | obj in tmps9.Modifies :: obj modifies set tmps10 <- set t10 <- config.tableEncryptionConfigs.Values | true - && t10.search.Some? - , t11 <- t10.search.value.versions | true - :: t11.keyStore, + && t10.cmm.Some? + :: t10.cmm.value, obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj + modifies set tmps11 <- set t11 <- config.tableEncryptionConfigs.Values | true + && t11.legacyOverride.Some? + :: t11.legacyOverride.value.encryptor, + obj <- tmps11.Modifies | obj in tmps11.Modifies :: obj 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.keyStore, obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj + modifies set tmps14 <- set t14 <- config.tableEncryptionConfigs.Values | true + && t14.search.Some? + , t15 <- t14.search.value.versions | true + && t15.keySource.single? + && t15.keySource.single.cache.Some? + && t15.keySource.single.cache.value.Shared? + :: t15.keySource.single.cache.value.Shared, + obj <- tmps14.Modifies | obj in tmps14.Modifies :: obj + modifies set tmps16 <- set t16 <- config.tableEncryptionConfigs.Values | true + && t16.search.Some? + , t17 <- t16.search.value.versions | true + && t17.keySource.multi? + && t17.keySource.multi.cache.Some? + && t17.keySource.multi.cache.value.Shared? + :: t17.keySource.multi.cache.value.Shared, + obj <- tmps16.Modifies | obj in tmps16.Modifies :: obj ensures res.Success? ==> && fresh(res.value) && fresh(res.value.Modifies - - ( set tmps14 <- set t14 <- config.tableEncryptionConfigs.Values | true - && t14.keyring.Some? - :: t14.keyring.value, - obj <- tmps14.Modifies | obj in tmps14.Modifies :: obj - ) - ( set tmps15 <- set t15 <- config.tableEncryptionConfigs.Values | true - && t15.cmm.Some? - :: t15.cmm.value, - obj <- tmps15.Modifies | obj in tmps15.Modifies :: obj - ) - ( set tmps16 <- set t16 <- config.tableEncryptionConfigs.Values | true - && t16.legacyOverride.Some? - :: t16.legacyOverride.value.encryptor, - obj <- tmps16.Modifies | obj in tmps16.Modifies :: obj - ) - ( set tmps17 <- set t17 <- config.tableEncryptionConfigs.Values | true - && t17.search.Some? - , t18 <- t17.search.value.versions | true - :: t18.keyStore, - obj <- tmps17.Modifies | obj in tmps17.Modifies :: obj + - ( set tmps18 <- set t18 <- config.tableEncryptionConfigs.Values | true + && t18.keyring.Some? + :: t18.keyring.value, + obj <- tmps18.Modifies | obj in tmps18.Modifies :: obj ) - ( 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, + && t19.cmm.Some? + :: t19.cmm.value, obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj + ) - ( set tmps20 <- set t20 <- config.tableEncryptionConfigs.Values | true + && t20.legacyOverride.Some? + :: t20.legacyOverride.value.encryptor, + obj <- tmps20.Modifies | obj in tmps20.Modifies :: obj + ) - ( set tmps21 <- set t21 <- config.tableEncryptionConfigs.Values | true + && t21.search.Some? + , t22 <- t21.search.value.versions | true + :: t22.keyStore, + obj <- tmps21.Modifies | obj in tmps21.Modifies :: obj + ) - ( set tmps23 <- set t23 <- config.tableEncryptionConfigs.Values | true + && t23.search.Some? + , t24 <- t23.search.value.versions | true + && t24.keySource.single? + && t24.keySource.single.cache.Some? + && t24.keySource.single.cache.value.Shared? + :: t24.keySource.single.cache.value.Shared, + obj <- tmps23.Modifies | obj in tmps23.Modifies :: obj + ) - ( set tmps25 <- set t25 <- config.tableEncryptionConfigs.Values | true + && t25.search.Some? + , t26 <- t25.search.value.versions | true + && t26.keySource.multi? + && t26.keySource.multi.cache.Some? + && t26.keySource.multi.cache.value.Shared? + :: t26.keySource.multi.cache.value.Shared, + obj <- tmps25.Modifies | obj in tmps25.Modifies :: obj ) ) && fresh(res.value.History) && res.value.ValidState() - ensures var tmps21 := set t21 | t21 in config.tableEncryptionConfigs.Values; - forall tmp21 :: tmp21 in tmps21 ==> - tmp21.keyring.Some? ==> - tmp21.keyring.value.ValidState() - ensures var tmps22 := set t22 | t22 in config.tableEncryptionConfigs.Values; - forall tmp22 :: tmp22 in tmps22 ==> - tmp22.cmm.Some? ==> - tmp22.cmm.value.ValidState() - ensures var tmps23 := set t23 | t23 in config.tableEncryptionConfigs.Values; - forall tmp23 :: tmp23 in tmps23 ==> - tmp23.legacyOverride.Some? ==> - tmp23.legacyOverride.value.encryptor.ValidState() - ensures var tmps24 := set t24 | t24 in config.tableEncryptionConfigs.Values; - forall tmp24 :: tmp24 in tmps24 ==> - tmp24.search.Some? ==> - var tmps25 := set t25 | t25 in tmp24.search.value.versions; - forall tmp25 :: tmp25 in tmps25 ==> - tmp25.keyStore.ValidState() - ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values; - forall tmp26 :: tmp26 in tmps26 ==> - 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() + ensures var tmps27 := set t27 | t27 in config.tableEncryptionConfigs.Values; + forall tmp27 :: tmp27 in tmps27 ==> + tmp27.keyring.Some? ==> + tmp27.keyring.value.ValidState() + ensures var tmps28 := set t28 | t28 in config.tableEncryptionConfigs.Values; + forall tmp28 :: tmp28 in tmps28 ==> + tmp28.cmm.Some? ==> + tmp28.cmm.value.ValidState() + ensures var tmps29 := set t29 | t29 in config.tableEncryptionConfigs.Values; + forall tmp29 :: tmp29 in tmps29 ==> + tmp29.legacyOverride.Some? ==> + tmp29.legacyOverride.value.encryptor.ValidState() + ensures var tmps30 := set t30 | t30 in config.tableEncryptionConfigs.Values; + forall tmp30 :: tmp30 in tmps30 ==> + tmp30.search.Some? ==> + var tmps31 := set t31 | t31 in tmp30.search.value.versions; + forall tmp31 :: tmp31 in tmps31 ==> + tmp31.keyStore.ValidState() + ensures var tmps32 := set t32 | t32 in config.tableEncryptionConfigs.Values; + forall tmp32 :: tmp32 in tmps32 ==> + tmp32.search.Some? ==> + var tmps33 := set t33 | t33 in tmp32.search.value.versions; + forall tmp33 :: tmp33 in tmps33 ==> + tmp33.keySource.single? ==> + tmp33.keySource.single.cache.Some? ==> + tmp33.keySource.single.cache.value.Shared? ==> + tmp33.keySource.single.cache.value.Shared.ValidState() + ensures var tmps34 := set t34 | t34 in config.tableEncryptionConfigs.Values; + forall tmp34 :: tmp34 in tmps34 ==> + tmp34.search.Some? ==> + var tmps35 := set t35 | t35 in tmp34.search.value.versions; + forall tmp35 :: tmp35 in tmps35 ==> + tmp35.keySource.multi? ==> + tmp35.keySource.multi.cache.Some? ==> + tmp35.keySource.multi.cache.value.Shared? ==> + tmp35.keySource.multi.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 { diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index f44f59b6c..77f3b7aab 100644 --- 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; @@ -150,10 +151,11 @@ 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); + reveal SearchConfigToInfo.ValidSharedCache(); var searchR := SearchConfigToInfo.Convert(inputConfig); var search :- searchR.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); assert search.None? || search.value.ValidState(); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy index 467ef6c87..8ee8feebf 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy @@ -32,7 +32,7 @@ module PutItemTransformTest { method TestPutItemInputMultiFail(plaintextOverride : Option) { assume {:axiom} false; - var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(plaintextOverride); + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMulti(plaintextOverride); var tableName := GetTableName("foo"); var input := DDB.PutItemInput( TableName := tableName, @@ -57,7 +57,7 @@ module PutItemTransformTest { method {:test} TestPutItemInputMultiForceAllow() { assume {:axiom} false; - var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli( + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMulti( Some(PlaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ) ); var tableName := GetTableName("foo"); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy index 6a6a1ef7b..f287a4c47 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy @@ -279,7 +279,7 @@ module TestFixtures { "TheKeyField" := SE.SIGN_ONLY ] - method GetDynamoDbEncryptionTransformsMutli(plaintextOverride : Option) + method GetDynamoDbEncryptionTransformsMulti(plaintextOverride : Option) returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient) ensures encryption.ValidState() ensures fresh(encryption) diff --git a/DynamoDbEncryption/runtimes/java/.gitignore b/DynamoDbEncryption/runtimes/java/.gitignore index fe5c7a5ac..58db26ec3 100644 --- a/DynamoDbEncryption/runtimes/java/.gitignore +++ b/DynamoDbEncryption/runtimes/java/.gitignore @@ -4,6 +4,9 @@ # Ignore Gradle build output directory build +# Ignore bin +bin + # JetBrains .idea/* *.iml diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java index 7a7f45a7e..def56ee72 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java @@ -679,7 +679,19 @@ public static MultiKeyStore MultiKeyStore( ) ) : Option.create_None(CacheType._typeDescriptor()); - return new MultiKeyStore(keyFieldName, cacheTTL, cache); + Option> partitionId; + partitionId = + Objects.nonNull(nativeValue.partitionId()) + ? Option.create_Some( + DafnySequence._typeDescriptor(TypeDescriptor.CHAR), + software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( + nativeValue.partitionId() + ) + ) + : Option.create_None( + DafnySequence._typeDescriptor(TypeDescriptor.CHAR) + ); + return new MultiKeyStore(keyFieldName, cacheTTL, cache, partitionId); } public static PartOnly PartOnly( @@ -758,7 +770,29 @@ public static SingleKeyStore SingleKeyStore( ); Integer cacheTTL; cacheTTL = (nativeValue.cacheTTL()); - return new SingleKeyStore(keyId, cacheTTL); + Option cache; + cache = + Objects.nonNull(nativeValue.cache()) + ? Option.create_Some( + CacheType._typeDescriptor(), + software.amazon.cryptography.materialproviders.ToDafny.CacheType( + nativeValue.cache() + ) + ) + : Option.create_None(CacheType._typeDescriptor()); + Option> partitionId; + partitionId = + Objects.nonNull(nativeValue.partitionId()) + ? Option.create_Some( + DafnySequence._typeDescriptor(TypeDescriptor.CHAR), + software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( + nativeValue.partitionId() + ) + ) + : Option.create_None( + DafnySequence._typeDescriptor(TypeDescriptor.CHAR) + ); + return new SingleKeyStore(keyId, cacheTTL, cache, partitionId); } public static StandardBeacon StandardBeacon( diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java index efbdce285..c953e7bf9 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java @@ -595,6 +595,13 @@ public static MultiKeyStore MultiKeyStore( ) ); } + if (dafnyValue.dtor_partitionId().is_Some()) { + nativeBuilder.partitionId( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_partitionId().dtor_value() + ) + ); + } return nativeBuilder.build(); } @@ -674,6 +681,20 @@ public static SingleKeyStore SingleKeyStore( ) ); nativeBuilder.cacheTTL((dafnyValue.dtor_cacheTTL())); + if (dafnyValue.dtor_cache().is_Some()) { + nativeBuilder.cache( + software.amazon.cryptography.materialproviders.ToNative.CacheType( + dafnyValue.dtor_cache().dtor_value() + ) + ); + } + if (dafnyValue.dtor_partitionId().is_Some()) { + nativeBuilder.partitionId( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_partitionId().dtor_value() + ) + ); + } return nativeBuilder.build(); } diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/MultiKeyStore.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/MultiKeyStore.java index 0f1420eaa..77ad60629 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/MultiKeyStore.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/MultiKeyStore.java @@ -26,10 +26,16 @@ public class MultiKeyStore { */ private final CacheType cache; + /** + * Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache. + */ + private final String partitionId; + protected MultiKeyStore(BuilderImpl builder) { this.keyFieldName = builder.keyFieldName(); this.cacheTTL = builder.cacheTTL(); this.cache = builder.cache(); + this.partitionId = builder.partitionId(); } /** @@ -53,6 +59,13 @@ public CacheType cache() { return this.cache; } + /** + * @return Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache. + */ + public String partitionId() { + return this.partitionId; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -92,6 +105,16 @@ public interface Builder { */ CacheType cache(); + /** + * @param partitionId Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache. + */ + Builder partitionId(String partitionId); + + /** + * @return Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache. + */ + String partitionId(); + MultiKeyStore build(); } @@ -103,12 +126,15 @@ static class BuilderImpl implements Builder { protected CacheType cache; + protected String partitionId; + protected BuilderImpl() {} protected BuilderImpl(MultiKeyStore model) { this.keyFieldName = model.keyFieldName(); this.cacheTTL = model.cacheTTL(); this.cache = model.cache(); + this.partitionId = model.partitionId(); } public Builder keyFieldName(String keyFieldName) { @@ -138,6 +164,15 @@ public CacheType cache() { return this.cache; } + public Builder partitionId(String partitionId) { + this.partitionId = partitionId; + return this; + } + + public String partitionId() { + return this.partitionId; + } + public MultiKeyStore build() { if (Objects.isNull(this.keyFieldName())) { throw new IllegalArgumentException( diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/SingleKeyStore.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/SingleKeyStore.java index 9ece5763f..0c16361bf 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/SingleKeyStore.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/SingleKeyStore.java @@ -4,6 +4,7 @@ package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; import java.util.Objects; +import software.amazon.cryptography.materialproviders.model.CacheType; /** * The configuration for using a single Beacon Key. @@ -20,9 +21,21 @@ public class SingleKeyStore { */ private final Integer cacheTTL; + /** + * Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore. + */ + private final CacheType cache; + + /** + * Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache. + */ + private final String partitionId; + protected SingleKeyStore(BuilderImpl builder) { this.keyId = builder.keyId(); this.cacheTTL = builder.cacheTTL(); + this.cache = builder.cache(); + this.partitionId = builder.partitionId(); } /** @@ -39,6 +52,20 @@ public Integer cacheTTL() { return this.cacheTTL; } + /** + * @return Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore. + */ + public CacheType cache() { + return this.cache; + } + + /** + * @return Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache. + */ + public String partitionId() { + return this.partitionId; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -68,6 +95,26 @@ public interface Builder { */ Integer cacheTTL(); + /** + * @param cache Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore. + */ + Builder cache(CacheType cache); + + /** + * @return Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore. + */ + CacheType cache(); + + /** + * @param partitionId Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache. + */ + Builder partitionId(String partitionId); + + /** + * @return Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache. + */ + String partitionId(); + SingleKeyStore build(); } @@ -77,11 +124,17 @@ static class BuilderImpl implements Builder { protected Integer cacheTTL; + protected CacheType cache; + + protected String partitionId; + protected BuilderImpl() {} protected BuilderImpl(SingleKeyStore model) { this.keyId = model.keyId(); this.cacheTTL = model.cacheTTL(); + this.cache = model.cache(); + this.partitionId = model.partitionId(); } public Builder keyId(String keyId) { @@ -102,6 +155,24 @@ public Integer cacheTTL() { return this.cacheTTL; } + public Builder cache(CacheType cache) { + this.cache = cache; + return this; + } + + public CacheType cache() { + return this.cache; + } + + public Builder partitionId(String partitionId) { + this.partitionId = partitionId; + return this; + } + + public String partitionId() { + return this.partitionId; + } + public SingleKeyStore build() { if (Objects.isNull(this.keyId())) { throw new IllegalArgumentException( diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/MultiKeyStore.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/MultiKeyStore.cs index 82fc3f519..ad6541b51 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/MultiKeyStore.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/MultiKeyStore.cs @@ -10,6 +10,7 @@ public class MultiKeyStore private string _keyFieldName; private int? _cacheTTL; private AWS.Cryptography.MaterialProviders.CacheType _cache; + private string _partitionId; public string KeyFieldName { get { return this._keyFieldName; } @@ -37,6 +38,15 @@ public bool IsSetCache() { return this._cache != null; } + public string PartitionId + { + get { return this._partitionId; } + set { this._partitionId = value; } + } + public bool IsSetPartitionId() + { + return this._partitionId != null; + } public void Validate() { if (!IsSetKeyFieldName()) throw new System.ArgumentException("Missing value for required property 'KeyFieldName'"); diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/SingleKeyStore.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/SingleKeyStore.cs index c0e76e378..891baa636 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/SingleKeyStore.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/SingleKeyStore.cs @@ -9,6 +9,8 @@ public class SingleKeyStore { private string _keyId; private int? _cacheTTL; + private AWS.Cryptography.MaterialProviders.CacheType _cache; + private string _partitionId; public string KeyId { get { return this._keyId; } @@ -27,6 +29,24 @@ public bool IsSetCacheTTL() { return this._cacheTTL.HasValue; } + public AWS.Cryptography.MaterialProviders.CacheType Cache + { + get { return this._cache; } + set { this._cache = value; } + } + public bool IsSetCache() + { + return this._cache != null; + } + public string PartitionId + { + get { return this._partitionId; } + set { this._partitionId = value; } + } + public bool IsSetPartitionId() + { + return this._partitionId != null; + } public void Validate() { if (!IsSetKeyId()) throw new System.ArgumentException("Missing value for required property 'KeyId'"); diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs index b0542873a..5ae8d0198 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs @@ -522,25 +522,30 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ISingleKeyStore value) { software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore(); converted.KeyId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(concrete._keyId); - converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(concrete._cacheTTL); return converted; + converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(concrete._cacheTTL); + if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(concrete._cache); + if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(concrete._partitionId); return converted; } public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ISingleKeyStore ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore(AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore value) { value.Validate(); - - return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(value.KeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(value.CacheTTL)); + AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null; + string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(value.KeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(var_partitionId)); } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IMultiKeyStore value) { software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore(); converted.KeyFieldName = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(concrete._keyFieldName); converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(concrete._cacheTTL); - if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(concrete._cache); return converted; + if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(concrete._cache); + if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(concrete._partitionId); return converted; } public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IMultiKeyStore ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore(AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore value) { value.Validate(); AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null; - return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(value.KeyFieldName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(var_cache)); + string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(value.KeyFieldName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(var_partitionId)); } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.PartOnly FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S8_PartOnly(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IPartOnly value) { @@ -762,6 +767,22 @@ public static int ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dyna { return ToDafny_N6_smithy__N3_api__S7_Integer(value); } + public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.MaterialProviders.CacheType)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(AWS.Cryptography.MaterialProviders.CacheType value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType((AWS.Cryptography.MaterialProviders.CacheType)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S6_String(value); @@ -786,6 +807,14 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12 { return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType((AWS.Cryptography.MaterialProviders.CacheType)value)); } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S6_Shared__M5_other(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S6_String(value); diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs index 95841aee6..e252e07d5 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs @@ -5494,25 +5494,30 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ISingleKeyStore value) { software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore(); converted.KeyId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(concrete._keyId); - converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(concrete._cacheTTL); return converted; + converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(concrete._cacheTTL); + if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(concrete._cache); + if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(concrete._partitionId); return converted; } public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ISingleKeyStore ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore(AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore value) { value.Validate(); - - return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(value.KeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(value.CacheTTL)); + AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null; + string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(value.KeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(var_partitionId)); } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IMultiKeyStore value) { software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore(); converted.KeyFieldName = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(concrete._keyFieldName); converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(concrete._cacheTTL); - if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(concrete._cache); return converted; + if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(concrete._cache); + if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(concrete._partitionId); return converted; } public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IMultiKeyStore ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore(AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore value) { value.Validate(); AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null; - return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(value.KeyFieldName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(var_cache)); + string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(value.KeyFieldName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(var_partitionId)); } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.StandardBeacon FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_StandardBeacon(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IStandardBeacon value) { @@ -5594,6 +5599,22 @@ public static int ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dyna { return ToDafny_N6_smithy__N3_api__S7_Integer(value); } + public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.MaterialProviders.CacheType)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(AWS.Cryptography.MaterialProviders.CacheType value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType((AWS.Cryptography.MaterialProviders.CacheType)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S6_String(value); @@ -5618,6 +5639,14 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12 { return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType((AWS.Cryptography.MaterialProviders.CacheType)value)); } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_StandardBeacon__M4_name(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S6_String(value); diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index d4eb1f144..46605a425 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -524,7 +524,22 @@ module {:options "-functionSyntax:4"} JsonConfig { var cache :- expect mpl.CreateCryptographicMaterialsCache(input); var client :- expect Primitives.AtomicPrimitives(); - var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32); + + // Create a test partitionIdBytes + var partitionIdBytes : seq :- 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 :- 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); diff --git a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs index 346af372e..35d5c504e 100644 --- a/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs +++ b/TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs @@ -489,25 +489,30 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ISingleKeyStore value) { software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore(); converted.KeyId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(concrete._keyId); - converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(concrete._cacheTTL); return converted; + converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(concrete._cacheTTL); + if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(concrete._cache); + if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(concrete._partitionId); return converted; } public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ISingleKeyStore ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore(AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore value) { value.Validate(); - - return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(value.KeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(value.CacheTTL)); + AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null; + string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(value.KeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(var_partitionId)); } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IMultiKeyStore value) { software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore(); converted.KeyFieldName = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(concrete._keyFieldName); converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(concrete._cacheTTL); - if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(concrete._cache); return converted; + if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(concrete._cache); + if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(concrete._partitionId); return converted; } public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IMultiKeyStore ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore(AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore value) { value.Validate(); AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null; - return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(value.KeyFieldName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(var_cache)); + string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(value.KeyFieldName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(var_partitionId)); } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.PartOnly FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S8_PartOnly(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IPartOnly value) { @@ -722,6 +727,22 @@ public static int ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dyna { return ToDafny_N6_smithy__N3_api__S7_Integer(value); } + public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(Wrappers_Compile._IOption value) + { + return value.is_None ? (AWS.Cryptography.MaterialProviders.CacheType)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(AWS.Cryptography.MaterialProviders.CacheType value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType((AWS.Cryptography.MaterialProviders.CacheType)value)); + } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S6_String(value); @@ -746,6 +767,14 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12 { return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType((AWS.Cryptography.MaterialProviders.CacheType)value)); } + public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(Wrappers_Compile._IOption> value) + { + return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract()); + } + public static Wrappers_Compile._IOption> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(string value) + { + return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value)); + } public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S6_Shared__M5_other(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S6_String(value); diff --git a/specification/searchable-encryption/search-config.md b/specification/searchable-encryption/search-config.md index 9c70d99cb..e12aefea4 100644 --- a/specification/searchable-encryption/search-config.md +++ b/specification/searchable-encryption/search-config.md @@ -5,7 +5,12 @@ ## Version -1.0.0 +- 1.1.0 + - [Update Cache Entry Identifier Formulas to shared cache across multiple Beacon Key Sources](../../changes/2024-09-13_cache-across-hierarchical-keyrings/change.md) + - New optional parameter `Partition ID` used to distinguish Cryptographic Material Providers (i.e: Beacon Key Sources) writing to a cache + - New optional parameter `cache` allowed while creating a `SingleKeyStore` +- 1.0.0 + - Initial record ### Changelog @@ -166,6 +171,8 @@ On initialization of a Single Key Store, the caller MUST provide: - [Beacon Key Id](#beacon-key-id) - [cacheTTL](#cachettl) +- [cache](#key-store-cache) +- [partition-id](#partition-id) ### Multi Key Store Initialization @@ -177,7 +184,8 @@ On initialization of a Multi Key Store, the caller MUST provide: - [Beacon Key Field Name](#beacon-key-field-name) - [cacheTTL](#cachettl) -- [max cache size](#max-cache-size) +- [cache](#key-store-cache) +- [partition-id](#partition-id) ### Field descriptions @@ -208,24 +216,32 @@ and used to extract a beacon key id from a query. The [cacheTTL](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#time-to-live-ttl) for how long a beacon key should exist locally before reauthorization. -#### max cache size - -The [max cache size](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#entry-capacity) -that the [Key Store Cache](#key-store-cache) will be configured to. - ### 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) the [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) -MUST be 1 -For a [Multi Key Store](#multi-key-store-initialization) the [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) -MUST be key store's max cache size. +For a [Single Key Store](#single-key-store-initialization), either the user provides a cache, or we create a cache that has [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) +equal to 1. +For a [Multi Key Store](#multi-key-store-initialization), either the user provides a cache, or we create a cache that has [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) +equal to 1000. + +The Key Store Cache is shared across different [Beacon Key Sources](#beacon-key-source) if and only if a `Shared` cache is used. +In all other cases, the Key Store Cache is bound to the [Beacon Key Source](#beacon-key-source). +In either case, Cache Identifiers MUST be unique across all key sources. +Cache Identifiers for Searchable Encryption MUST be set as per the section [Searchable Encryption Cache Identifier](#searchable-encryption-cache-identifier). + +### Partition ID + +An optional string that uniquely identifies the respective [Beacon Key Source](#beacon-key-source) +and is used to avoid collisions with other [Beacon Key Sources](#beacon-key-source). + +PartitionId can be a string provided by the user. If provided, it MUST be interpreted as UTF8 bytes. +If the PartitionId is NOT provided by the user, it MUST be set to the 16 byte representation of a v4 UUID. -The Key Store Cache MUST be bound to the Beacon Key Source. -This is currently invariant because we construct the cache for each search config -It is easy for beacon key ids to be unique within a single key source, -this may not be true across all key sources. +The Partition ID MUST NOT be changed after initialization. + +Please see [Shared Cache Considerations](#shared-cache-considerations) on how to provide the +Partition ID and Logical Key Store Name while providing a Shared Cache to the [Beacon Key Source](#beacon-key-source). ## Beacon Keys @@ -296,11 +312,11 @@ and the result returned for Get beacon key for query. ### Get Beacon Key Materials -Takes a `beacon key id`, [Key Store Cache](#key-store-cache), and a `KeyStore` +Takes a `beacon key id`, [Key Store Cache](#key-store-cache), and a `KeyStore`. Get beacon key MUST Call the associated [Key Store Cache](#key-store-cache) [Get Cache Entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#get-cache-entry) -with the `beacon key id`. +with the cache identifier defined in the [Searchable Encryption Cache Identifier](#searchable-encryption-cache-identifier) section. If a [cache entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#cache-entry) exists, get beacon key MUST return the [entry materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#materials). @@ -308,7 +324,15 @@ exists, get beacon key MUST return the [entry materials](../../submodules/Materi The `beacon key id` MUST be passed to the configured `KeyStore`'s `GetBeaconKey` operation. If `GetBeaconKey` fails get beacon key MUST fail. -For every [standard beacons](beacons.md#standard-beacon-initialization) an HMAC key +If using a `Shared` cache across multiple [Beacon Key Sources](#beacon-key-source), +different [Beacon Key Sources](#beacon-key-source) having the same `beaconKey` can have different TTLs. +In such a case, the expiry time in the cache is set according to the [Beacon Key Source](#beacon-key-source) that populated the cache. +There MUST be a check (cacheEntryWithinLimits) to make sure that for the cache entry found, who's TTL has NOT expired, +`time.now() - cacheEntryCreationTime <= ttlSeconds` is true and +valid for TTL of the [Beacon Key Source](#beacon-key-source) getting the cache entry. +If this is NOT true, then we MUST treat the cache entry as expired. + +For every [standard beacons](beacons.md#standard-beacon-initialization), an HMAC key MUST be generated in accordance with [HMAC Key Generation](#hmac-key-generation). [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated @@ -320,6 +344,11 @@ These materials MUST be put into the associated [Key Store Cache](#key-store-cac with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time) equal to now + configured [cacheTTL](#cachettl). +The Searchable Encryption cache identifier +used to [Put Cache Entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#put-cache-entry) +MUST be the same +as the identifier that was used to attempt [Get Cache Entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#get-cache-entry). + These cached materials MUST be returned. ### HMAC Key Generation @@ -332,3 +361,155 @@ using the beacon key retrieved above as the initial key material with no salt. The `info` MUST be the concatenation of "AWS_DBE_SCAN_BEACON" encoded as UTF8 and the beacon name. The `expectedLength` MUST be 64 bytes. + +## Searchable Encryption Cache Identifier + +This section is consistent with the Cache Entry Identifier formulas for the [Hierarchical Keyring](https://github.com/awslabs/aws-encryption-sdk-specification/blob/master/framework/aws-kms/aws-kms-hierarchical-keyring.md#appendix-a-cache-entry-identifier-formulas) +and [Caching CMM](https://github.com/awslabs/aws-encryption-sdk-specification/blob/master/framework/caching-cmm.md#appendix-a-cache-entry-identifier-formulas) in the Material Providers spec. These cache identifier formulas should +not be changed independently. + +When accessing the underlying cryptographic materials cache, +Searchable Encryption MUST use the formulas specified in this section +in order to compute the [cache entry identifier](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#cache-identifier). + +### Preliminaries + +Each of the cache entry identifier formulas includes serialized information related to the branch key, +as defined in the [Key Provider Info](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#key-provider-information). + +We establish the following definitions for the Cache Entry Identifier formula: + +#### Resource Identifier + +Resource Identifier is defined in the [Material Providers specification](https://github.com/awslabs/aws-encryption-sdk-specification/blob/master/framework/aws-kms/aws-kms-hierarchical-keyring.md#resource-identifier). + +#### Scope Identifier + +Scope Identifier is defined in the [Material Providers specification](https://github.com/awslabs/aws-encryption-sdk-specification/blob/master/framework/aws-kms/aws-kms-hierarchical-keyring.md#scope-identifier). + +#### Partition ID + +Partition ID is an optional parameter provided to the [Beacon Key Source](#beacon-key-source) input, which distinguishes +Cryptographic Material Providers (i.e: [Beacon Key Sources](#beacon-key-source)) writing to a cache. +It can either be a String provided by the user, which MUST be interpreted as the bytes of +UTF-8 Encoding of the String, or a v4 UUID, which SHOULD be interpreted as the 16 byte representation of the UUID. + +Note: The cache will not know if the Partition ID is a String set by the user or the UUID. +The constructor of the [Beacon Key Source](#beacon-key-source) MUST record these bytes at construction time. + +Please see [Shared Cache Considerations](#shared-cache-considerations) on how to provide the +Partition ID and Logical Key Store Name of the [beacon versions](#beacon-version-initialization) +while providing a Shared Cache to the [Beacon Key Source](#beacon-key-source). + +#### Resource Suffix + +The resource suffixes for the Searchable Encryption is as follows: + +``` +logicalKeyStoreName + NULL_BYTE + UTF8Encode(branchKeyId) +``` + +The aforementioned 4 definitions ([Resource Identifier](#resource-identifier), +[Scope Identifier](#scope-identifier), [Partition ID](#partition-id-1), and +[Resource Suffix](#resource-suffix)) MUST be appended together with the null byte, 0x00, +and the SHA384 of the result should be taken as the final cache identifier. + +When the [Beacon Key Source](#beacon-key-source) receives a `getKeyMap` request, +the cache entry identifier MUST be calculated as the +SHA-384 hash of the following byte strings, in the order listed: + +- MUST be the Resource ID for the Hierarchical Keyring (0x02) +- MUST be the Scope ID for Searchable Encryption (0x03) +- MUST be the Partition ID for the [Beacon Key Source](#beacon-key-source) +- Resource Suffix + - MUST be the UTF8 encoded Logical Key Store Name of the keystore for the [beacon versions](#beacon-version-initialization) + - MUST be the UTF8 encoded branch-key-id + +All the above fields must be separated by a single NULL_BYTE `0x00`. + +| Field | Length (bytes) | Interpreted as | +| ---------------------- | -------------- | ------------------- | +| Resource ID | 1 | bytes | +| Null Byte | 1 | `0x00` | +| Scope ID | 1 | bytes | +| Null Byte | 1 | `0x00` | +| Partition ID | Variable | bytes | +| Null Byte | 1 | `0x00` | +| Logical Key Store Name | Variable | UTF-8 Encoded Bytes | +| Null Byte | 1 | `0x00` | +| Branch Key ID | Variable | UTF-8 Encoded Bytes | + +As a formula: + +``` +resource-id = [0x02] +scope-id = [0x03] +logical-key-store-name = UTF8Encode(beaconVersion.keystore.LogicalKeyStoreName) +branch-key-id = UTF8Encode(BranchKeyIdentifier) +NULL_BYTE = [0x00] + +ENTRY_ID = SHA384( + resource-id + + NULL_BYTE + + scope-id + + NULL_BYTE + + partition-id + + NULL_BYTE + + logical-key-store-name + + NULL_BYTE + + branch-key-id +) +``` + +## Shared Cache Considerations + +If a user has two or more [beacon versions](#beacon-version-initialization) with: + +- Same Partition ID +- Same Logical Key Store Name of the Key Store +- Same Branch Key ID + +then they WILL share the cache entries in the `Shared` Cache. + +Any keyring that has access to the `Shared` cache may be able to use materials +that it may or may not have direct access to. + +Users should make sure that all of Partition ID, Logical Key Store Name of the Key Store +and Branch Key ID are set to be the same for two [beacon versions](#beacon-version-initialization) +if and only they want the keyrings to share cache entries. + +Therefore, there are two important parameters that users need to carefully set while providing the shared cache: + +### Partition ID + +Partition ID is an optional parameter provided to the [Beacon Key Source](#beacon-key-source) input, +which distinguishes Cryptographic Material Providers (i.e: [Beacon Key Sources](#beacon-key-source)) writing to a cache. + +- (Default) A a random 16-byte UUID, which makes + it unique for every [Beacon Key Source](#beacon-key-source). + In this case, two [Beacon Key Sources](#beacon-key-source) (or another Material Provider) + WILL NOT share the same cache entries in the cache. +- If the Partition ID is set by the user and is the same for two [Beacon Key Sources](#beacon-key-source) (or another Material Provider), + they MAY share the same cache entries in the cache. +- If the Partition ID is set by the user and is different for two [Beacon Key Sources](#beacon-key-source) (or another Material Provider), + they WILL NOT share the same cache entries in the cache. + +### Logical Key Store Name + +> Note: Users should not have two different physical Key Stores with the same Logical Key Store Name. + +Logical Key Store Name is set by the user when configuring the Key Store for +the [beacon versions](#beacon-version-initialization). +This is a logical name for the key store. +Logical Key Store Name MUST be converted to UTF8 Bytes to be used in +the cache identifiers. + +Suppose there's a physical Key Store on DynamoDB (K). Two Key Store clients of K (K1 and K2) are created. +Now, two [beacon versions](#beacon-version-initialization) (BV1 and BV2) are created with these Key Store clients (K1 and K2 respectively). + +- If we want to share cache entries across these two BeaconVersions BV1 and BV2, the Logical Key Store Names + for both the Key Store clients (K1 and K2) should be set to be the same. +- If we set the Logical Key Store Names for K1 and K2 to be different, BV1 (which uses Key Store client K1) + and BV2 (which uses Key Store client K2) will NOT be able to share cache entries. + +Notice that both K1 and K2 are clients for the same physical Key Store (K). diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 1915a11bb..9c80544bb 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 1915a11bb84d3d9135b89d2a46ec9d6dff27b493 +Subproject commit 9c80544bbfeac5547915aa93795f9b79eac7db6b diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny index f67c21075..84523f4cb 160000 --- a/submodules/smithy-dafny +++ b/submodules/smithy-dafny @@ -1 +1 @@ -Subproject commit f67c21075ebac40e052204b6827a4db641e65862 +Subproject commit 84523f4cb6e76503c7f2cd4ac9e67adea709d013