From d4709e91fe05180ea13712cf657373515493a3f1 Mon Sep 17 00:00:00 2001 From: Ritvik Kapila <61410899+RitvikKapila@users.noreply.github.com> Date: Mon, 23 Sep 2024 14:15:42 -0700 Subject: [PATCH] feat(HierarchyKeyring; CMC): Shared cache across Hierarchy Keyrings (#747) --- .../AwsCryptographyMaterialProvidersTypes.dfy | 4 +- .../cryptographic-materials-cache.smithy | 4 +- .../Model/keyrings.smithy | 5 +- ...ryptographyMaterialProvidersOperations.dfy | 87 ++- .../src/CMCs/CacheConstants.dfy | 23 + .../AwsKms/AwsKmsHierarchicalKeyring.dfy | 173 ++++-- .../TestAwsKmsHierarchicalKeyring.dfy | 516 +++++++++++++++++- .../materialproviders/ToDafny.java | 20 +- .../materialproviders/ToNative.java | 12 + .../materialproviders/model/CacheType.java | 38 ++ .../CreateAwsKmsHierarchicalKeyringInput.java | 43 +- .../CacheType.cs | 13 +- .../CreateAwsKmsHierarchicalKeyringInput.cs | 10 + .../TypeConversion.cs | 69 ++- .../KeyVectors/src/CreateStaticKeyStores.dfy | 14 +- .../src/KeyringFromKeyDescription.dfy | 3 +- .../TypeConversion.cs | 55 +- 17 files changed, 993 insertions(+), 96 deletions(-) create mode 100644 AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/CacheConstants.dfy diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy index f5b262f67..b23ccbeb0 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy @@ -719,6 +719,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty | SingleThreaded(SingleThreaded: SingleThreadedCache) | MultiThreaded(MultiThreaded: MultiThreadedCache) | StormTracking(StormTracking: StormTrackingCache) + | Shared(Shared: ICryptographicMaterialsCache) class IClientSupplierCallHistory { ghost constructor() { GetClient := []; @@ -823,7 +824,8 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty nameonly branchKeyIdSupplier: Option := Option.None , nameonly keyStore: AwsCryptographyKeyStoreTypes.IKeyStoreClient , nameonly ttlSeconds: PositiveLong , - nameonly cache: Option := Option.None + nameonly cache: Option := Option.None , + nameonly partitionId: Option := Option.None ) datatype CreateAwsKmsKeyringInput = | CreateAwsKmsKeyringInput ( nameonly kmsKeyId: KmsKeyId , diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/cryptographic-materials-cache.smithy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/cryptographic-materials-cache.smithy index 244411a49..d5d1c06fd 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/cryptographic-materials-cache.smithy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/cryptographic-materials-cache.smithy @@ -215,7 +215,9 @@ union CacheType { No: NoCache, SingleThreaded: SingleThreadedCache, MultiThreaded: MultiThreadedCache, - StormTracking: StormTrackingCache + StormTracking: StormTrackingCache, + @documentation("Shared cache across multiple Hierarchical Keyrings. For this cache type, the user should provide an already constructed CryptographicMaterialsCache to the Hierarchical Keyring at initialization.") + Shared: CryptographicMaterialsCacheReference } structure CreateCryptographicMaterialsCacheInput { diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/keyrings.smithy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/keyrings.smithy index 1bec34677..5b8d11900 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/keyrings.smithy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/keyrings.smithy @@ -339,8 +339,11 @@ structure CreateAwsKmsHierarchicalKeyringInput { @javadoc("How many seconds the Branch Key material is allowed to be reused within the local cache before it is re-retrieved from Amazon DynamoDB and re-authenticated with AWS KMS.") ttlSeconds: PositiveLong, - @javadoc("Which type of local cache to use.") + @documentation("Sets the type of cache for this Hierarchical Keyring. By providing an already initialized 'Shared' cache, users can determine the scope of the cache. That is, if the cache is shared across other Cryptographic Material Providers, for instance other Hierarchical Keyrings or Caching Cryptographic Materials Managers (Caching CMMs). If any other type of cache in the CacheType union is provided, the Hierarchical Keyring will initialize a cache of that type, to be used with only this Hierarchical Keyring. If not set, a DefaultCache is initialized to be used with only this Hierarchical Keyring with entryCapacity = 1000.") cache : CacheType + + @documentation("Partition ID to distinguish Cryptographic Material Providers (i.e: Keyrings) writing to a cache. If the Partition ID is the same for two Hierarchical Keyrings (or another Material Provider), they can share the same cache entries in the cache.") + partitionId : String } // Raw diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy index b37808f78..8f1193b2a 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy @@ -66,6 +66,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph import Kms = Com.Amazonaws.Kms import Ddb = ComAmazonawsDynamodbTypes import RequiredEncryptionContextCMM + import UUID datatype Config = Config( nameonly crypto: Primitives.AtomicPrimitivesClient @@ -260,16 +261,76 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph method CreateAwsKmsHierarchicalKeyring (config: InternalConfig, input: CreateAwsKmsHierarchicalKeyringInput) returns (output: Result) { - var maxCacheSize : int32; + // //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#initialization + // //= type=implication + //# If the Hierarchical Keyring does NOT get a `Shared` cache on initialization, + //# it MUST initialize a [cryptographic-materials-cache](../local-cryptographic-materials-cache.md) + //# with the user provided cache limit TTL and the entry capacity. + //# If no `cache` is provided, a `DefaultCache` MUST be configured with entry capacity of 1000. + var cmc; + + if input.cache.Some? { + match input.cache.value { + case Shared(c) => + cmc := c; + case _ => + cmc :- CreateCryptographicMaterialsCache( + config, + CreateCryptographicMaterialsCacheInput(cache := input.cache.value) + ); + } + } + else { + cmc :- CreateCryptographicMaterialsCache( + config, + CreateCryptographicMaterialsCacheInput( + cache := Types.Default( + Types.DefaultCache(entryCapacity := 1000) + ) + ) + ); + } - //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#initialization - //= type=implication - //# If no max cache size is provided, the crypotgraphic materials cache MUST be configured to a - //# max cache size of 1000. - var cache := if input.cache.Some? then - input.cache.value - else - Types.Default(Types.DefaultCache(entryCapacity := 1000)); + // //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#partition-id + // //= type=implication + //# 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. + var partitionIdBytes : seq; + + if input.partitionId.Some? { + partitionIdBytes :- UTF8.Encode(input.partitionId.value) + .MapFailure( + e => Types.AwsCryptographicMaterialProvidersException( + message := "Could not UTF-8 Encode Partition ID: " + e + ) + ); + } else { + var uuid? := UUID.GenerateUUID(); + + var uuid :- uuid? + .MapFailure(e => Types.AwsCryptographicMaterialProvidersException(message := e)); + + partitionIdBytes :- UUID.ToByteArray(uuid) + .MapFailure(e => Types.AwsCryptographicMaterialProvidersException(message := e)); + } + + // //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#logical-key-store-name + // //= type=implication + //# Logical Key Store Name is set by the user when configuring the Key Store for + //# the Hierarchical Keyring. 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. + var getKeyStoreInfoOutput? := input.keyStore.GetKeyStoreInfo(); + var getKeyStoreInfoOutput :- getKeyStoreInfoOutput? + .MapFailure(e => Types.AwsCryptographyKeyStore(AwsCryptographyKeyStore := e)); + var logicalKeyStoreName := getKeyStoreInfoOutput.logicalKeyStoreName; + + var logicalKeyStoreNameBytes : seq :- UTF8.Encode(logicalKeyStoreName) + .MapFailure( + e => Types.AwsCryptographicMaterialProvidersException( + message := "Could not UTF-8 Encode Logical Key Store Name: " + e + ) + ); :- Need(input.branchKeyId.None? || input.branchKeyIdSupplier.None?, Types.AwsCryptographicMaterialProvidersException( @@ -279,14 +340,14 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph Types.AwsCryptographicMaterialProvidersException( message := "Must initialize keyring with either branchKeyId or BranchKeyIdSupplier.")); - var cmc :- CreateCryptographicMaterialsCache(config, CreateCryptographicMaterialsCacheInput(cache := cache)); var keyring := new AwsKmsHierarchicalKeyring.AwsKmsHierarchicalKeyring( keyStore := input.keyStore, branchKeyId := input.branchKeyId, branchKeyIdSupplier := input.branchKeyIdSupplier, ttlSeconds := input.ttlSeconds, - // maxCacheSize := maxCacheSize, cmc := cmc, + partitionIdBytes := partitionIdBytes, + logicalKeyStoreNameBytes := logicalKeyStoreNameBytes, cryptoPrimitives := config.crypto ); return Success(keyring); @@ -735,6 +796,10 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph ); var synCmc := new StormTrackingCMC.StormTrackingCMC(cmc); return Success(synCmc); + case Shared(c) => + var exception := Types.AwsCryptographicMaterialProvidersException( + message := "CreateCryptographicMaterialsCache should never be called with Shared CacheType."); + return Failure(exception); } } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/CacheConstants.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/CacheConstants.dfy new file mode 100644 index 000000000..e93356f68 --- /dev/null +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/CacheConstants.dfy @@ -0,0 +1,23 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "../../Model/AwsCryptographyMaterialProvidersTypes.dfy" + +module CacheConstants { + import opened StandardLibrary.UInt + import Seq + + // Constants defined for cache identifier formulae + + // Null Byte + const NULL_BYTE : seq := [0x00] + + // Resource Id + const RESOURCE_ID_CACHING_CMM: seq := [0x01] + const RESOURCE_ID_HIERARCHICAL_KEYRING: seq := [0x02] + + // Scope Id + const SCOPE_ID_ENCRYPT: seq := [0x01] + const SCOPE_ID_DECRYPT: seq := [0x02] + const SCOPE_ID_SEARCHABLE_ENCRYPTION: seq := [0x03] +} \ No newline at end of file diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy index f87125982..4900d544e 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy @@ -14,6 +14,7 @@ include "../../CMCs/StormTracker.dfy" include "../../CMCs/StormTrackingCMC.dfy" include "../../CMCs/LocalCMC.dfy" include "../../CMCs/SynchronizedLocalCMC.dfy" +include "../../CMCs/CacheConstants.dfy" include "../../../Model/AwsCryptographyMaterialProvidersTypes.dfy" include "../../ErrorMessages.dfy" @@ -31,6 +32,7 @@ module AwsKmsHierarchicalKeyring { import SynchronizedLocalCMC import StormTracker import StormTrackingCMC + import opened CacheConstants import opened AlgorithmSuites import EdkWrapping import MaterialWrapping @@ -117,6 +119,18 @@ module AwsKmsHierarchicalKeyring { res := cmc.PutCacheEntry(input); } + // Checks if (time_now - cache creation time of the extracted cache entry) is less than the allowed + // TTL of the current Hierarchical Keyring calling the getEntry method from the cache. + // Mitigates risk if another Material Provider wrote the entry with a longer TTL. + predicate method cacheEntryWithinLimits( + creationTime: Types.PositiveLong, + now: Types.PositiveLong, + ttlSeconds: Types.PositiveLong + ): (output: bool) + { + now - creationTime <= ttlSeconds as Types.PositiveLong + } + //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#interface //= type=implication //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface) @@ -129,6 +143,8 @@ module AwsKmsHierarchicalKeyring { const ttlSeconds: Types.PositiveLong const cryptoPrimitives: Primitives.AtomicPrimitivesClient const cache: Types.ICryptographicMaterialsCache + const partitionIdBytes: seq + const logicalKeyStoreNameBytes: seq predicate ValidState() ensures ValidState() ==> History in Modifies @@ -163,6 +179,8 @@ module AwsKmsHierarchicalKeyring { ttlSeconds: Types.PositiveLong, cmc: Types.ICryptographicMaterialsCache, + partitionIdBytes: seq, + logicalKeyStoreNameBytes: seq, cryptoPrimitives : Primitives.AtomicPrimitivesClient ) requires ttlSeconds >= 0 @@ -174,6 +192,8 @@ module AwsKmsHierarchicalKeyring { && this.keyStore == keyStore && this.branchKeyIdSupplier == branchKeyIdSupplier && this.ttlSeconds == ttlSeconds + && this.partitionIdBytes == partitionIdBytes + && this.logicalKeyStoreNameBytes == logicalKeyStoreNameBytes ensures && ValidState() && fresh(this) @@ -181,12 +201,14 @@ module AwsKmsHierarchicalKeyring { && var maybeSupplierModifies := if branchKeyIdSupplier.Some? then branchKeyIdSupplier.value.Modifies else {}; && fresh(Modifies - keyStore.Modifies - cryptoPrimitives.Modifies - maybeSupplierModifies) { - this.keyStore := keyStore; - this.branchKeyId := branchKeyId; - this.branchKeyIdSupplier := branchKeyIdSupplier; - this.ttlSeconds := ttlSeconds; - this.cryptoPrimitives := cryptoPrimitives; - this.cache := cmc; + this.keyStore := keyStore; + this.branchKeyId := branchKeyId; + this.branchKeyIdSupplier := branchKeyIdSupplier; + this.ttlSeconds := ttlSeconds; + this.cryptoPrimitives := cryptoPrimitives; + this.cache := cmc; + this.partitionIdBytes := partitionIdBytes; + this.logicalKeyStoreNameBytes := logicalKeyStoreNameBytes; History := new Types.IKeyringCallHistory(); var maybeSupplierModifies := if branchKeyIdSupplier.Some? then branchKeyIdSupplier.value.Modifies else {}; @@ -351,12 +373,14 @@ module AwsKmsHierarchicalKeyring { } var decryptClosure := new DecryptSingleEncryptedDataKey( - materials, - keyStore, - cryptoPrimitives, - branchKeyIdForDecrypt, - ttlSeconds, - cache + materials := materials, + keyStore := keyStore, + cryptoPrimitives := cryptoPrimitives, + branchKeyId := branchKeyIdForDecrypt, + ttlSeconds := ttlSeconds, + cache := cache, + partitionIdBytes := partitionIdBytes, + logicalKeyStoreNameBytes := logicalKeyStoreNameBytes ); var outcome, attempts := ReduceToSuccess( @@ -391,7 +415,7 @@ module AwsKmsHierarchicalKeyring { requires cryptoPrimitives.ValidState() modifies cryptoPrimitives.Modifies ensures cryptoPrimitives.ValidState() - ensures cacheId.Success? ==> |cacheId.value| == 32 + ensures cacheId.Success? ==> |cacheId.value| == 48 { :- Need( && UTF8.Decode(branchKeyIdUtf8).MapFailure(WrapStringToError).Success? @@ -399,20 +423,33 @@ module AwsKmsHierarchicalKeyring { && 0 <= |branchKeyId| < UINT32_LIMIT, E("Invalid Branch Key ID Length") ); + // //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#encryption-materials + //# When the hierarchical keyring receives an OnEncrypt request, + //# the cache entry identifier MUST be calculated as the + //# SHA-384 hash of the following byte strings, in the order listed: + // (blank line for duvet) + //# - MUST be the Resource ID for the Hierarchical Keyring (0x02) + //# - MUST be the Scope ID for Encrypt (0x01) + //# - MUST be the Partition ID for the Hierarchical Keyring + //# - Resource Suffix + //# - MUST be the UTF8 encoded Logical Key Store Name of the keystore for the Hierarchical Keyring + //# - MUST be the UTF8 encoded branch-key-id + // (blank line for duvet) + //# All the above fields must be separated by a single NULL_BYTE `0x00`. - var branchKeyId := UTF8.Decode(branchKeyIdUtf8).value; - var lenBranchKey := UInt.UInt32ToSeq(|branchKeyId| as uint32); + var hashAlgorithm := Crypto.DigestAlgorithm.SHA_384; - var hashAlgorithm := Crypto.DigestAlgorithm.SHA_512; + // Resource ID: Hierarchical Keyring [0x02] + var resourceId : seq := RESOURCE_ID_HIERARCHICAL_KEYRING; - var maybeBranchKeyDigest := cryptoPrimitives - .Digest(Crypto.DigestInput(digestAlgorithm := hashAlgorithm, message := branchKeyIdUtf8)); - var branchKeyDigest :- maybeBranchKeyDigest - .MapFailure(e => Types.AwsCryptographyPrimitives(AwsCryptographyPrimitives := e)); + // Scope ID: Encryption [0x01] + var scopeId : seq := SCOPE_ID_ENCRYPT; - var activeUtf8 :- UTF8.Encode(EXPRESSION_ATTRIBUTE_VALUE_STATUS_VALUE) - .MapFailure(WrapStringToError); - var identifier := lenBranchKey + branchKeyDigest + [0x00] + activeUtf8; + // Create the Suffix + var suffix : seq := logicalKeyStoreNameBytes + NULL_BYTE + branchKeyIdUtf8; + + // Append Resource Id, Scope Id, Partition Id, and Suffix to create the cache identifier + var identifier := resourceId + NULL_BYTE + scopeId + NULL_BYTE + partitionIdBytes + NULL_BYTE + suffix; var maybeCacheIdDigest := cryptoPrimitives .Digest(Crypto.DigestInput(digestAlgorithm := hashAlgorithm, message := identifier)); @@ -425,7 +462,7 @@ module AwsKmsHierarchicalKeyring { message := "Digest generated a message not equal to the expected length.") ); - return Success(cacheDigest[0..32]); + return Success(cacheDigest); } method GetActiveHierarchicalMaterials( @@ -445,7 +482,22 @@ module AwsKmsHierarchicalKeyring { verifyValidStateCache(cache); var getCacheOutput := getEntry(cache, getCacheInput); - if getCacheOutput.Failure? { + var now := Time.GetCurrent(); + + // //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#onencrypt + //# If using a `Shared` cache across multiple Hierarchical Keyrings, + //# different keyrings having the same `branchKey` can have different TTLs. + //# In such a case, the expiry time in the cache is set according to the Keyring 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 Hierarchical Keyring 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 := ttlSeconds + ) + { var maybeGetActiveBranchKeyOutput := keyStore.GetActiveBranchKey( KeyStore.GetActiveBranchKeyInput( branchKeyIdentifier := branchKeyId @@ -609,6 +661,8 @@ module AwsKmsHierarchicalKeyring { const branchKeyId: string const ttlSeconds: Types.PositiveLong const cache: Types.ICryptographicMaterialsCache + const partitionIdBytes: seq + const logicalKeyStoreNameBytes: seq constructor( materials: Materials.DecryptionMaterialsPendingPlaintextDataKey, @@ -616,7 +670,9 @@ module AwsKmsHierarchicalKeyring { cryptoPrimitives: Primitives.AtomicPrimitivesClient, branchKeyId: string, ttlSeconds: Types.PositiveLong, - cache: Types.ICryptographicMaterialsCache + cache: Types.ICryptographicMaterialsCache, + partitionIdBytes: seq, + logicalKeyStoreNameBytes: seq ) requires keyStore.ValidState() && cryptoPrimitives.ValidState() ensures @@ -626,6 +682,8 @@ module AwsKmsHierarchicalKeyring { && this.branchKeyId == branchKeyId && this.ttlSeconds == ttlSeconds && this.cache == cache + && this.partitionIdBytes == partitionIdBytes + && this.logicalKeyStoreNameBytes == logicalKeyStoreNameBytes ensures Invariant() { this.materials := materials; @@ -634,6 +692,8 @@ module AwsKmsHierarchicalKeyring { this.branchKeyId := branchKeyId; this.ttlSeconds := ttlSeconds; this.cache := cache; + this.partitionIdBytes := partitionIdBytes; + this.logicalKeyStoreNameBytes := logicalKeyStoreNameBytes; Modifies := keyStore.Modifies + cryptoPrimitives.Modifies; } @@ -728,7 +788,7 @@ module AwsKmsHierarchicalKeyring { cryptoPrimitives: Primitives.AtomicPrimitivesClient ) returns (cacheId: Result, Types.Error>) - ensures cacheId.Success? ==> |cacheId.value| == 32 + ensures cacheId.Success? ==> |cacheId.value| == 48 { :- Need( && UTF8.Decode(branchKeyIdUtf8).MapFailure(WrapStringToError).Success? @@ -736,23 +796,55 @@ module AwsKmsHierarchicalKeyring { && 0 <= |branchKeyId| < UINT32_LIMIT, E("Invalid Branch Key ID Length") ); + // //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#decryption-materials + //# When the hierarchical keyring receives an OnDecrypt request, + //# it MUST calculate the cache entry identifier as the + //# SHA-384 hash of the following byte strings, in the order listed: + // (blank line for duvet) + //# - MUST be the Resource ID for the Hierarchical Keyring (0x02) + //# - MUST be the Scope ID for Decrypt (0x02) + //# - MUST be the Partition ID for the Hierarchical Keyring + //# - Resource Suffix + //# - MUST be the UTF8 encoded Logical Key Store Name of the keystore for the Hierarchical Keyring + //# - MUST be the UTF8 encoded branch-key-id + //# - MUST be the UTF8 encoded branch-key-version + // (blank line for duvet) + //# All the above fields must be separated by a single NULL_BYTE `0x00`. - var branchKeyId := UTF8.Decode(branchKeyIdUtf8).value; - var lenBranchKey := UInt.UInt32ToSeq(|branchKeyId| as uint32); + var hashAlgorithm := Crypto.DigestAlgorithm.SHA_384; + + // Resource ID: Hierarchical Keyring [0x02] + var resourceId : seq := RESOURCE_ID_HIERARCHICAL_KEYRING; + + // Scope ID: Decryption [0x02] + var scopeId : seq := SCOPE_ID_DECRYPT; + + // Convert branch key version into UTF8 bytes :- Need( UTF8.IsASCIIString(branchKeyVersion), E("Unable to represent as an ASCII string.") ); var versionBytes := UTF8.EncodeAscii(branchKeyVersion); - var identifier := lenBranchKey + branchKeyIdUtf8 + [0x00 as uint8] + versionBytes; + // Create the suffix + var suffix : seq := logicalKeyStoreNameBytes + NULL_BYTE + branchKeyIdUtf8 + NULL_BYTE + versionBytes; + + // Append Resource Id, Scope Id, Partition Id, and Suffix to create the cache identifier + var identifier := resourceId + NULL_BYTE + scopeId + NULL_BYTE + partitionIdBytes + NULL_BYTE + suffix; + var identifierDigestInput := Crypto.DigestInput( - digestAlgorithm := Crypto.DigestAlgorithm.SHA_512, message := identifier + digestAlgorithm := hashAlgorithm, message := identifier ); var maybeCacheDigest := Digest.Digest(identifierDigestInput); var cacheDigest :- maybeCacheDigest.MapFailure(e => Types.AwsCryptographyPrimitives(e)); - return Success(cacheDigest[0..32]); + :- Need( + |cacheDigest| == Digest.Length(hashAlgorithm), + Types.AwsCryptographicMaterialProvidersException( + message := "Digest generated a message not equal to the expected length.") + ); + + return Success(cacheDigest); } method GetHierarchicalMaterialsVersion( @@ -772,7 +864,22 @@ module AwsKmsHierarchicalKeyring { verifyValidStateCache(cache); var getCacheOutput := getEntry(cache, getCacheInput); - if getCacheOutput.Failure? { + var now := Time.GetCurrent(); + + // //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-hierarchical-keyring.md#ondecrypt + //# If using a `Shared` cache across multiple Hierarchical Keyrings, + //# different keyrings having the same `branchKey` can have different TTLs. + //# In such a case, the expiry time in the cache is set according to the Keyring 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 Hierarchical Keyring 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 := ttlSeconds + ) + { var maybeGetBranchKeyVersionOutput := keyStore.GetBranchKeyVersion( KeyStore.GetBranchKeyVersionInput( branchKeyIdentifier := branchKeyId, diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsHierarchicalKeyring/TestAwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsHierarchicalKeyring/TestAwsKmsHierarchicalKeyring.dfy index 772bc3af9..5cbdb03d9 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsHierarchicalKeyring/TestAwsKmsHierarchicalKeyring.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/AwsKms/AwsKmsHierarchicalKeyring/TestAwsKmsHierarchicalKeyring.dfy @@ -72,6 +72,7 @@ module TestAwsKmsHierarchicalKeyring { method {:test} TestHierarchyClientESDKSuite() { var branchKeyId := BRANCH_KEY_ID; + // TTL = 166.67 hours var ttl : Types.PositiveLong := (1 * 60000) * 10; var mpl :- expect MaterialProviders.MaterialProviders(); @@ -97,7 +98,8 @@ module TestAwsKmsHierarchicalKeyring { branchKeyIdSupplier := None, keyStore := keyStore, ttlSeconds := ttl, - cache := None + cache := None, + partitionId := None ) ); @@ -113,6 +115,7 @@ module TestAwsKmsHierarchicalKeyring { method {:test} TestHierarchyClientDBESuite() { var branchKeyId := BRANCH_KEY_ID; + // TTL = 166.67 hours var ttl : Types.PositiveLong := (1 * 60000) * 10; var mpl :- expect MaterialProviders.MaterialProviders(); @@ -138,7 +141,8 @@ module TestAwsKmsHierarchicalKeyring { branchKeyIdSupplier := None, keyStore := keyStore, ttlSeconds := ttl, - cache := None + cache := None, + partitionId := None ) ); @@ -155,6 +159,7 @@ module TestAwsKmsHierarchicalKeyring { method {:test} TestBranchKeyIdSupplier() { var branchKeyIdSupplier: Types.IBranchKeyIdSupplier := new DummyBranchKeyIdSupplier(); + // TTL = 166.67 hours var ttl : int64 := (1 * 60000) * 10; var mpl :- expect MaterialProviders.MaterialProviders(); @@ -180,7 +185,8 @@ module TestAwsKmsHierarchicalKeyring { branchKeyIdSupplier := Some(branchKeyIdSupplier), keyStore := keyStore, ttlSeconds := ttl, - cache := None + cache := None, + partitionId := None ) ); @@ -199,6 +205,7 @@ module TestAwsKmsHierarchicalKeyring { method {:test} TestInvalidDataKeyError() { var branchKeyIdSupplier: Types.IBranchKeyIdSupplier := new DummyBranchKeyIdSupplier(); + // TTL = 166.67 hours var ttl : int64 := (1 * 60000) * 10; var mpl :- expect MaterialProviders.MaterialProviders(); var kmsClient :- expect KMS.KMSClient(); @@ -220,7 +227,8 @@ module TestAwsKmsHierarchicalKeyring { branchKeyIdSupplier := Some(branchKeyIdSupplier), keyStore := keyStore, ttlSeconds := ttl, - cache := None + cache := None, + partitionId := None ) ); var materials := GetTestMaterials(TEST_DBE_ALG_SUITE_ID); @@ -320,6 +328,506 @@ module TestAwsKmsHierarchicalKeyring { == decryptionMaterialsOut.materials.plaintextDataKey; } + method {:test} TestSharedCacheWithSamePartitionIdAndSameLogicalKeyStoreName() + { + var branchKeyIdWest := BRANCH_KEY_ID; + // TTL = 166.67 hours + var ttl : Types.PositiveLong := (1 * 60000) * 10; + var mpl :- expect MaterialProviders.MaterialProviders(); + + var regionWest := "us-west-2"; + var regionEast := "us-east-2"; + + var kmsClientWest :- expect KMS.KMSClientForRegion(regionWest); + var kmsClientEast :- expect KMS.KMSClientForRegion(regionEast); + var ddbClient :- expect DDB.DynamoDBClient(); + var kmsConfig := KeyStoreTypes.KMSConfiguration.kmsKeyArn(keyArn); + + // Create a Key Store with the a KMS configuration and + // KMS client for a particular region (us-west-2 in this case) + // with a logicalKeyStoreName + var keyStoreConfigClientRegionWest := KeyStoreTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + logicalKeyStoreName := logicalKeyStoreName, + grantTokens := None, + ddbTableName := branchKeyStoreName, + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClientWest) + ); + + var keyStoreClientRegionWest :- expect KeyStore.KeyStore(keyStoreConfigClientRegionWest); + + // Create a key store with the same branch key store and + // KMS key configuration but with different client region + // (us-east-2 in this case) + // with the same logicalKeyStoreName as keyStoreConfigClientRegionWest + var keyStoreConfigClientRegionEast := KeyStoreTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + logicalKeyStoreName := logicalKeyStoreName, + grantTokens := None, + ddbTableName := branchKeyStoreName, + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClientEast) + ); + + var keyStoreClientRegionEast :- expect KeyStore.KeyStore(keyStoreConfigClientRegionEast); + + // Initialize the shared Cryptographic Materials Cache + var sharedCacheInput :- expect mpl.CreateCryptographicMaterialsCache( + Types.CreateCryptographicMaterialsCacheInput( + cache := Types.CacheType.Default( + Types.DefaultCache( + entryCapacity := 100 + ) + ) + ) + ); + + // Wrap the initialized shared Cryptographic Materials Cache as a `Shared` CacheType object + var sharedCache := Types.CacheType.Shared( + sharedCacheInput + ); + + // Create a Hierarchy Keyring HK1 with branchKeyIdWest, + // keyStoreClientRegionWest and the shared cache `sharedCache` + // with a partitionId + var hierarchyKeyring1 :- expect mpl.CreateAwsKmsHierarchicalKeyring( + Types.CreateAwsKmsHierarchicalKeyringInput( + branchKeyId := Some(branchKeyIdWest), + branchKeyIdSupplier := None, + keyStore := keyStoreClientRegionWest, + ttlSeconds := ttl, + cache := Some(sharedCache), + partitionId := Some("partitionId") + ) + ); + + // Create a Hierarchy Keyring HK2 with branchKeyIdWest, + // keyStoreClientRegionEast and the shared cache `sharedCache` + // with the same partitionId as hierarchyKeyring1 + var hierarchyKeyring2 :- expect mpl.CreateAwsKmsHierarchicalKeyring( + Types.CreateAwsKmsHierarchicalKeyringInput( + branchKeyId := Some(branchKeyIdWest), + branchKeyIdSupplier := None, + keyStore := keyStoreClientRegionEast, + ttlSeconds := ttl, + cache := Some(sharedCache), + partitionId := Some("partitionId") + ) + ); + + // Get test materials + var materials := GetTestMaterials(TEST_ESDK_ALG_SUITE_ID); + + // Commenting these tests out because these are ghost fields and cannot be added for now + // Ensure that there are 0 KMS Decrypt and 0 DynamoDB GetItem calls until now + // expect |kmsClientEast.History.Decrypt| == 0; + // expect |kmsClientWest.History.Decrypt| == 0; + // expect |ddbClient.History.GetItem| == 0; + + // Try encrypting the test materials with HK2, which has branchKeyIdWest + // but its keystore is keyStoreClientRegionEast + var encryptionMaterialsOutMismatchedRegion := hierarchyKeyring2.OnEncrypt( + Types.OnEncryptInput(materials:=materials) + ); + + // This encryption should fail because of region mismatch + expect encryptionMaterialsOutMismatchedRegion.IsFailure(); + + // Commenting these tests out because these are ghost fields and cannot be added for now + // Ensure that there are 1 KMS Decrypt calls for kmsClientEast, 0 for KMSClientWest and + // 1 DynamoDB GetItem calls until now + // expect |kmsClientEast.History.Decrypt| == 1; + // expect |kmsClientWest.History.Decrypt| == 0; + // expect |ddbClient.History.GetItem| == 1; + + // Encrypt and Decrypt round trip for the test materials with HK1, + // which has branchKeyIdWest and its keystore is keyStoreClientRegionWest + // This should pass + TestRoundtrip(hierarchyKeyring1, materials, TEST_ESDK_ALG_SUITE_ID, branchKeyIdWest); + + // Commenting these tests out because these are ghost fields and cannot be added for now + // Ensure that there are 1 KMS Decrypt calls for kmsClientEast, 2 for KMSClientWest and + // 3 DynamoDB GetItem calls until now + // expect |kmsClientEast.History.Decrypt| == 1; + // expect |kmsClientWest.History.Decrypt| == 2; + // expect |ddbClient.History.GetItem| == 3; + + // This should now pass because the material exists inside the cache. + // This proves the cache entry from HK1 was hit by HK2. + TestRoundtrip(hierarchyKeyring2, materials, TEST_ESDK_ALG_SUITE_ID, branchKeyIdWest); + + // Commenting these tests out because these are ghost fields and cannot be added for now + // Ensure that the count doesn't change after the last round trip because the cached + // entries are being used. That is, there are 1 KMS Decrypt calls for kmsClientEast, + // 2 for KMSClientWest and 3 DynamoDB GetItem calls until now + // expect |kmsClientEast.History.Decrypt| == 1; + // expect |kmsClientWest.History.Decrypt| == 2; + // expect |ddbClient.History.GetItem| == 3; + } + + method {:test} TestSharedCacheWithDifferentUnspecifiedPartitionIdAndSameLogicalKeyStoreName() + { + var branchKeyIdWest := BRANCH_KEY_ID; + // TTL = 166.67 hours + var ttl : Types.PositiveLong := (1 * 60000) * 10; + var mpl :- expect MaterialProviders.MaterialProviders(); + + var regionWest := "us-west-2"; + var regionEast := "us-east-2"; + + var kmsClientWest :- expect KMS.KMSClientForRegion(regionWest); + var kmsClientEast :- expect KMS.KMSClientForRegion(regionEast); + var ddbClient :- expect DDB.DynamoDBClient(); + var kmsConfig := KeyStoreTypes.KMSConfiguration.kmsKeyArn(keyArn); + + // Create a Key Store with the a KMS configuration and + // KMS client for a particular region (us-west-2 in this case) + // with a logicalKeyStoreName + var keyStoreConfigClientRegionWest := KeyStoreTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + logicalKeyStoreName := logicalKeyStoreName, + grantTokens := None, + ddbTableName := branchKeyStoreName, + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClientWest) + ); + + var keyStoreClientRegionWest :- expect KeyStore.KeyStore(keyStoreConfigClientRegionWest); + + // Create a key store with the same branch key store and + // KMS key configuration but with different client region + // (us-east-2 in this case) + // with the same logicalKeyStoreName as keyStoreConfigClientRegionWest + var keyStoreConfigClientRegionEast := KeyStoreTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + logicalKeyStoreName := logicalKeyStoreName, + grantTokens := None, + ddbTableName := branchKeyStoreName, + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClientEast) + ); + + var keyStoreClientRegionEast :- expect KeyStore.KeyStore(keyStoreConfigClientRegionEast); + + // Initialize the shared Cryptographic Materials Cache + var sharedCacheInput :- expect mpl.CreateCryptographicMaterialsCache( + Types.CreateCryptographicMaterialsCacheInput( + cache := Types.CacheType.Default( + Types.DefaultCache( + entryCapacity := 100 + ) + ) + ) + ); + + // Wrap the initialized shared Cryptographic Materials Cache as a `Shared` CacheType object + var sharedCache := Types.CacheType.Shared( + sharedCacheInput + ); + + // Create a Hierarchy Keyring HK1 with branchKeyIdWest, + // keyStoreClientRegionWest and the shared cache `sharedCache` + // without specifying the partitionId, so that it is initialized to a random UUID + var hierarchyKeyring1 :- expect mpl.CreateAwsKmsHierarchicalKeyring( + Types.CreateAwsKmsHierarchicalKeyringInput( + branchKeyId := Some(branchKeyIdWest), + branchKeyIdSupplier := None, + keyStore := keyStoreClientRegionWest, + ttlSeconds := ttl, + cache := Some(sharedCache), + partitionId := None + ) + ); + + // Create a Hierarchy Keyring HK2 with branchKeyIdWest, + // keyStoreClientRegionEast and the shared cache `sharedCache` + // without specifying the partitionId, so that it is initialized to a random UUID + var hierarchyKeyring2 :- expect mpl.CreateAwsKmsHierarchicalKeyring( + Types.CreateAwsKmsHierarchicalKeyringInput( + branchKeyId := Some(branchKeyIdWest), + branchKeyIdSupplier := None, + keyStore := keyStoreClientRegionEast, + ttlSeconds := ttl, + cache := Some(sharedCache), + partitionId := None + ) + ); + + // Get test materials + var materials := GetTestMaterials(TEST_ESDK_ALG_SUITE_ID); + + // Try encrypting the test materials with HK2, which has branchKeyIdWest + // but its keystore is keyStoreClientRegionEast + var encryptionMaterialsOutMismatchedRegion := hierarchyKeyring2.OnEncrypt( + Types.OnEncryptInput(materials:=materials) + ); + + // This encryption should fail because of region mismatch + expect encryptionMaterialsOutMismatchedRegion.IsFailure(); + + // Encrypt and Decrypt round trip for the test materials with HK1, + // which has branchKeyIdWest and its keystore is keyStoreClientRegionWest + // This should pass + TestRoundtrip(hierarchyKeyring1, materials, TEST_ESDK_ALG_SUITE_ID, branchKeyIdWest); + + // Again, try encrypting the test materials with HK2, which has branchKeyIdWest + // but its keystore is keyStoreClientRegionEast + var encryptionMaterialsOutMismatchedRegionFromCache := hierarchyKeyring2.OnEncrypt( + Types.OnEncryptInput(materials:=materials) + ); + + // This encryption should fail because the partition IDs for HK1 and HK2 are different + // even though the partition IDs are unspecified. In such a case, partition IDs are + // initialized as UUIDs which have negligible probability of collision. + // This proves the cache was missed. + expect encryptionMaterialsOutMismatchedRegionFromCache.IsFailure(); + } + + method {:test} TestSharedCacheWithDifferentSpecifiedPartitionIdAndSameLogicalKeyStoreName() + { + var branchKeyIdWest := BRANCH_KEY_ID; + // TTL = 166.67 hours + var ttl : Types.PositiveLong := (1 * 60000) * 10; + var mpl :- expect MaterialProviders.MaterialProviders(); + + var regionWest := "us-west-2"; + var regionEast := "us-east-2"; + + var kmsClientWest :- expect KMS.KMSClientForRegion(regionWest); + var kmsClientEast :- expect KMS.KMSClientForRegion(regionEast); + var ddbClient :- expect DDB.DynamoDBClient(); + var kmsConfig := KeyStoreTypes.KMSConfiguration.kmsKeyArn(keyArn); + + // Create a Key Store with the a KMS configuration and + // KMS client for a particular region (us-west-2 in this case) + // with a logicalKeyStoreName + var keyStoreConfigClientRegionWest := KeyStoreTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + logicalKeyStoreName := logicalKeyStoreName, + grantTokens := None, + ddbTableName := branchKeyStoreName, + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClientWest) + ); + + var keyStoreClientRegionWest :- expect KeyStore.KeyStore(keyStoreConfigClientRegionWest); + + // Create a key store with the same branch key store and + // KMS key configuration but with different client region + // (us-east-2 in this case) + // with the same logicalKeyStoreName as keyStoreConfigClientRegionWest + var keyStoreConfigClientRegionEast := KeyStoreTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + logicalKeyStoreName := logicalKeyStoreName, + grantTokens := None, + ddbTableName := branchKeyStoreName, + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClientEast) + ); + + var keyStoreClientRegionEast :- expect KeyStore.KeyStore(keyStoreConfigClientRegionEast); + + // Initialize the shared Cryptographic Materials Cache + var sharedCacheInput :- expect mpl.CreateCryptographicMaterialsCache( + Types.CreateCryptographicMaterialsCacheInput( + cache := Types.CacheType.Default( + Types.DefaultCache( + entryCapacity := 100 + ) + ) + ) + ); + + // Wrap the shared Cryptographic Materials Cache as a `Shared` CacheType object + var sharedCache := Types.CacheType.Shared( + sharedCacheInput + ); + + // Create a Hierarchy Keyring HK1 with branchKeyIdWest, + // keyStoreClientRegionWest and the shared cache `sharedCache` + // with a partitionId "partitionIdHK1" + var hierarchyKeyring1 :- expect mpl.CreateAwsKmsHierarchicalKeyring( + Types.CreateAwsKmsHierarchicalKeyringInput( + branchKeyId := Some(branchKeyIdWest), + branchKeyIdSupplier := None, + keyStore := keyStoreClientRegionWest, + ttlSeconds := ttl, + cache := Some(sharedCache), + partitionId := Some("partitionIdHK1") + ) + ); + + // Create a Hierarchy Keyring HK2 with branchKeyIdWest, + // keyStoreClientRegionEast and the shared cache `sharedCache` + // with a partitionId different than hierarchyKeyring1, which + // in this case is "partitionIdHK2" + var hierarchyKeyring2 :- expect mpl.CreateAwsKmsHierarchicalKeyring( + Types.CreateAwsKmsHierarchicalKeyringInput( + branchKeyId := Some(branchKeyIdWest), + branchKeyIdSupplier := None, + keyStore := keyStoreClientRegionEast, + ttlSeconds := ttl, + cache := Some(sharedCache), + partitionId := Some("partitionIdHK2") + ) + ); + + // Get test materials + var materials := GetTestMaterials(TEST_ESDK_ALG_SUITE_ID); + + // Try encrypting the test materials with HK2, which has branchKeyIdWest + // but its keystore is keyStoreClientRegionEast + var encryptionMaterialsOutMismatchedRegion := hierarchyKeyring2.OnEncrypt( + Types.OnEncryptInput(materials:=materials) + ); + + // This encryption should fail because of region mismatch + expect encryptionMaterialsOutMismatchedRegion.IsFailure(); + + // Encrypt and Decrypt round trip for the test materials with HK1, + // which has branchKeyIdWest and its keystore is keyStoreClientRegionWest + // This should pass + TestRoundtrip(hierarchyKeyring1, materials, TEST_ESDK_ALG_SUITE_ID, branchKeyIdWest); + + // Again, try encrypting the test materials with HK2, which has branchKeyIdWest + // but its keystore is keyStoreClientRegionEast + var encryptionMaterialsOutMismatchedRegionFromCache := hierarchyKeyring2.OnEncrypt( + Types.OnEncryptInput(materials:=materials) + ); + + // This encryption should fail because the partition IDs for HK1 and HK2 are different + expect encryptionMaterialsOutMismatchedRegionFromCache.IsFailure(); + } + + method {:test} TestSharedCacheWithSamePartitionIdAndDifferentLogicalKeyStoreName() + { + var branchKeyIdWest := BRANCH_KEY_ID; + // TTL = 166.67 hours + var ttl : Types.PositiveLong := (1 * 60000) * 10; + var mpl :- expect MaterialProviders.MaterialProviders(); + + var regionWest := "us-west-2"; + var regionEast := "us-east-2"; + + var kmsClientWest :- expect KMS.KMSClientForRegion(regionWest); + var kmsClientEast :- expect KMS.KMSClientForRegion(regionEast); + var ddbClient :- expect DDB.DynamoDBClient(); + var kmsConfig := KeyStoreTypes.KMSConfiguration.kmsKeyArn(keyArn); + + // Different logical key store names for both Key Stores + var logicalKeyStoreName : DDBTypes.TableName := logicalKeyStoreName; + var logicalKeyStoreNameNew : DDBTypes.TableName := logicalKeyStoreName + "New"; + + // Create a Key Store with the a KMS configuration and + // KMS client for a particular region (us-west-2 in this case) + // with a logicalKeyStoreName + var keyStoreConfigClientRegionWest := KeyStoreTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + logicalKeyStoreName := logicalKeyStoreName, + grantTokens := None, + ddbTableName := branchKeyStoreName, + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClientWest) + ); + + var keyStoreClientRegionWest :- expect KeyStore.KeyStore(keyStoreConfigClientRegionWest); + + // Create a key store with the same branch key store and + // KMS key configuration but with different client region + // (us-east-2 in this case) + // with a different logicalKeyStoreName as compared to keyStoreConfigClientRegionWest + // which is logicalKeyStoreNameNew in this case + var keyStoreConfigClientRegionEast := KeyStoreTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + logicalKeyStoreName := logicalKeyStoreNameNew, + grantTokens := None, + ddbTableName := branchKeyStoreName, + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClientEast) + ); + + var keyStoreClientRegionEast :- expect KeyStore.KeyStore(keyStoreConfigClientRegionEast); + + // Initialize the shared Cryptographic Materials Cache + var sharedCacheInput :- expect mpl.CreateCryptographicMaterialsCache( + Types.CreateCryptographicMaterialsCacheInput( + cache := Types.CacheType.Default( + Types.DefaultCache( + entryCapacity := 100 + ) + ) + ) + ); + + // Wrap the initialized shared Cryptographic Materials Cache as a `Shared` CacheType object + var sharedCache := Types.CacheType.Shared( + sharedCacheInput + ); + + // Create a Hierarchy Keyring HK1 with branchKeyIdWest, + // keyStoreClientRegionWest and the shared cache `sharedCache` + // with a partitionId + var hierarchyKeyring1 :- expect mpl.CreateAwsKmsHierarchicalKeyring( + Types.CreateAwsKmsHierarchicalKeyringInput( + branchKeyId := Some(branchKeyIdWest), + branchKeyIdSupplier := None, + keyStore := keyStoreClientRegionWest, + ttlSeconds := ttl, + cache := Some(sharedCache), + partitionId := Some("partitionId") + ) + ); + + // Create a Hierarchy Keyring HK2 with branchKeyIdWest, + // keyStoreClientRegionEast and the shared cache `sharedCache` + // with the same partitionId as hierarchyKeyring1 + var hierarchyKeyring2 :- expect mpl.CreateAwsKmsHierarchicalKeyring( + Types.CreateAwsKmsHierarchicalKeyringInput( + branchKeyId := Some(branchKeyIdWest), + branchKeyIdSupplier := None, + keyStore := keyStoreClientRegionEast, + ttlSeconds := ttl, + cache := Some(sharedCache), + partitionId := Some("partitionId") + ) + ); + + // Get test materials + var materials := GetTestMaterials(TEST_ESDK_ALG_SUITE_ID); + + // Try encrypting the test materials with HK2, which has branchKeyIdWest + // but its keystore is keyStoreClientRegionEast + var encryptionMaterialsOutMismatchedRegion := hierarchyKeyring2.OnEncrypt( + Types.OnEncryptInput(materials:=materials) + ); + + // This encryption should fail because of region mismatch + expect encryptionMaterialsOutMismatchedRegion.IsFailure(); + + // Encrypt and Decrypt round trip for the test materials with HK1, + // which has branchKeyIdWest and its keystore is keyStoreClientRegionWest + // This should pass + TestRoundtrip(hierarchyKeyring1, materials, TEST_ESDK_ALG_SUITE_ID, branchKeyIdWest); + + // Again, try encrypting the test materials with HK2, which has branchKeyIdWest + // but its keystore is keyStoreClientRegionEast + var encryptionMaterialsOutMismatchedRegionFromCache := hierarchyKeyring2.OnEncrypt( + Types.OnEncryptInput(materials:=materials) + ); + + // This encryption should fail because the logicalKeyStoreName for HK1 and HK2 are different + expect encryptionMaterialsOutMismatchedRegionFromCache.IsFailure(); + } + // Returns "hierarchy-test-v1" when EC contains kv pair "branchKey":"caseA" // Returns "hierarchy-test-active-active" when EC contains kv pair "branchKey":"caseB" // Otherwise returns a Failure diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToDafny.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToDafny.java index ed78a1e59..d2efbf511 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToDafny.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToDafny.java @@ -413,12 +413,25 @@ public static CreateAwsKmsHierarchicalKeyringInput CreateAwsKmsHierarchicalKeyri 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 CreateAwsKmsHierarchicalKeyringInput( branchKeyId, branchKeyIdSupplier, keyStore, ttlSeconds, - cache + cache, + partitionId ); } @@ -2132,6 +2145,11 @@ public static CacheType CacheType( ToDafny.StormTrackingCache(nativeValue.StormTracking()) ); } + if (Objects.nonNull(nativeValue.Shared())) { + return CacheType.create_Shared( + ToDafny.CryptographicMaterialsCache(nativeValue.Shared()) + ); + } throw new IllegalArgumentException( "Cannot convert " + nativeValue + diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToNative.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToNative.java index 790d62cc6..9bd2cbf7c 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToNative.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToNative.java @@ -474,6 +474,13 @@ public static CreateAwsKmsHierarchicalKeyringInput CreateAwsKmsHierarchicalKeyri 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(); } @@ -1669,6 +1676,11 @@ public static CacheType CacheType( ToNative.StormTrackingCache(dafnyValue.dtor_StormTracking()) ); } + if (dafnyValue.is_Shared()) { + nativeBuilder.Shared( + ToNative.CryptographicMaterialsCache(dafnyValue.dtor_Shared()) + ); + } return nativeBuilder.build(); } diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/CacheType.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/CacheType.java index 408cc6d78..edb10b961 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/CacheType.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/CacheType.java @@ -4,6 +4,8 @@ package software.amazon.cryptography.materialproviders.model; import java.util.Objects; +import software.amazon.cryptography.materialproviders.CryptographicMaterialsCache; +import software.amazon.cryptography.materialproviders.ICryptographicMaterialsCache; public class CacheType { @@ -33,12 +35,18 @@ public class CacheType { */ private final StormTrackingCache StormTracking; + /** + * Shared cache across multiple Hierarchical Keyrings. For this cache type, the user should provide an already constructed CryptographicMaterialsCache to the Hierarchical Keyring at initialization. + */ + private final ICryptographicMaterialsCache Shared; + protected CacheType(BuilderImpl builder) { this.Default = builder.Default(); this.No = builder.No(); this.SingleThreaded = builder.SingleThreaded(); this.MultiThreaded = builder.MultiThreaded(); this.StormTracking = builder.StormTracking(); + this.Shared = builder.Shared(); } /** @@ -77,6 +85,13 @@ public StormTrackingCache StormTracking() { return this.StormTracking; } + /** + * @return Shared cache across multiple Hierarchical Keyrings. For this cache type, the user should provide an already constructed CryptographicMaterialsCache to the Hierarchical Keyring at initialization. + */ + public ICryptographicMaterialsCache Shared() { + return this.Shared; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -138,6 +153,16 @@ public interface Builder { */ StormTrackingCache StormTracking(); + /** + * @param Shared Shared cache across multiple Hierarchical Keyrings. For this cache type, the user should provide an already constructed CryptographicMaterialsCache to the Hierarchical Keyring at initialization. + */ + Builder Shared(ICryptographicMaterialsCache Shared); + + /** + * @return Shared cache across multiple Hierarchical Keyrings. For this cache type, the user should provide an already constructed CryptographicMaterialsCache to the Hierarchical Keyring at initialization. + */ + ICryptographicMaterialsCache Shared(); + CacheType build(); } @@ -153,6 +178,8 @@ static class BuilderImpl implements Builder { protected StormTrackingCache StormTracking; + protected ICryptographicMaterialsCache Shared; + protected BuilderImpl() {} protected BuilderImpl(CacheType model) { @@ -161,6 +188,7 @@ protected BuilderImpl(CacheType model) { this.SingleThreaded = model.SingleThreaded(); this.MultiThreaded = model.MultiThreaded(); this.StormTracking = model.StormTracking(); + this.Shared = model.Shared(); } public Builder Default(DefaultCache Default) { @@ -208,6 +236,15 @@ public StormTrackingCache StormTracking() { return this.StormTracking; } + public Builder Shared(ICryptographicMaterialsCache Shared) { + this.Shared = CryptographicMaterialsCache.wrap(Shared); + return this; + } + + public ICryptographicMaterialsCache Shared() { + return this.Shared; + } + public CacheType build() { if (!onlyOneNonNull()) { throw new IllegalArgumentException( @@ -224,6 +261,7 @@ private boolean onlyOneNonNull() { this.SingleThreaded, this.MultiThreaded, this.StormTracking, + this.Shared, }; boolean haveOneNonNull = false; for (Object o : allValues) { diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/CreateAwsKmsHierarchicalKeyringInput.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/CreateAwsKmsHierarchicalKeyringInput.java index 120bd769c..da972fa97 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/CreateAwsKmsHierarchicalKeyringInput.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/CreateAwsKmsHierarchicalKeyringInput.java @@ -34,16 +34,22 @@ public class CreateAwsKmsHierarchicalKeyringInput { private final long ttlSeconds; /** - * Which type of local cache to use. + * Sets the type of cache for this Hierarchical Keyring. By providing an already initialized 'Shared' cache, users can determine the scope of the cache. That is, if the cache is shared across other Cryptographic Material Providers, for instance other Hierarchical Keyrings or Caching Cryptographic Materials Managers (Caching CMMs). If any other type of cache in the CacheType union is provided, the Hierarchical Keyring will initialize a cache of that type, to be used with only this Hierarchical Keyring. If not set, a DefaultCache is initialized to be used with only this Hierarchical Keyring with entryCapacity = 1000. */ private final CacheType cache; + /** + * Partition ID to distinguish Cryptographic Material Providers (i.e: Keyrings) writing to a cache. If the Partition ID is the same for two Hierarchical Keyrings (or another Material Provider), they can share the same cache entries in the cache. + */ + private final String partitionId; + protected CreateAwsKmsHierarchicalKeyringInput(BuilderImpl builder) { this.branchKeyId = builder.branchKeyId(); this.branchKeyIdSupplier = builder.branchKeyIdSupplier(); this.keyStore = builder.keyStore(); this.ttlSeconds = builder.ttlSeconds(); this.cache = builder.cache(); + this.partitionId = builder.partitionId(); } /** @@ -75,12 +81,19 @@ public long ttlSeconds() { } /** - * @return Which type of local cache to use. + * @return Sets the type of cache for this Hierarchical Keyring. By providing an already initialized 'Shared' cache, users can determine the scope of the cache. That is, if the cache is shared across other Cryptographic Material Providers, for instance other Hierarchical Keyrings or Caching Cryptographic Materials Managers (Caching CMMs). If any other type of cache in the CacheType union is provided, the Hierarchical Keyring will initialize a cache of that type, to be used with only this Hierarchical Keyring. If not set, a DefaultCache is initialized to be used with only this Hierarchical Keyring with entryCapacity = 1000. */ public CacheType cache() { return this.cache; } + /** + * @return Partition ID to distinguish Cryptographic Material Providers (i.e: Keyrings) writing to a cache. If the Partition ID is the same for two Hierarchical Keyrings (or another Material Provider), they can share the same cache entries in the cache. + */ + public String partitionId() { + return this.partitionId; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -131,15 +144,25 @@ public interface Builder { long ttlSeconds(); /** - * @param cache Which type of local cache to use. + * @param cache Sets the type of cache for this Hierarchical Keyring. By providing an already initialized 'Shared' cache, users can determine the scope of the cache. That is, if the cache is shared across other Cryptographic Material Providers, for instance other Hierarchical Keyrings or Caching Cryptographic Materials Managers (Caching CMMs). If any other type of cache in the CacheType union is provided, the Hierarchical Keyring will initialize a cache of that type, to be used with only this Hierarchical Keyring. If not set, a DefaultCache is initialized to be used with only this Hierarchical Keyring with entryCapacity = 1000. */ Builder cache(CacheType cache); /** - * @return Which type of local cache to use. + * @return Sets the type of cache for this Hierarchical Keyring. By providing an already initialized 'Shared' cache, users can determine the scope of the cache. That is, if the cache is shared across other Cryptographic Material Providers, for instance other Hierarchical Keyrings or Caching Cryptographic Materials Managers (Caching CMMs). If any other type of cache in the CacheType union is provided, the Hierarchical Keyring will initialize a cache of that type, to be used with only this Hierarchical Keyring. If not set, a DefaultCache is initialized to be used with only this Hierarchical Keyring with entryCapacity = 1000. */ CacheType cache(); + /** + * @param partitionId Partition ID to distinguish Cryptographic Material Providers (i.e: Keyrings) writing to a cache. If the Partition ID is the same for two Hierarchical Keyrings (or another Material Provider), they can share the same cache entries in the cache. + */ + Builder partitionId(String partitionId); + + /** + * @return Partition ID to distinguish Cryptographic Material Providers (i.e: Keyrings) writing to a cache. If the Partition ID is the same for two Hierarchical Keyrings (or another Material Provider), they can share the same cache entries in the cache. + */ + String partitionId(); + CreateAwsKmsHierarchicalKeyringInput build(); } @@ -157,6 +180,8 @@ static class BuilderImpl implements Builder { protected CacheType cache; + protected String partitionId; + protected BuilderImpl() {} protected BuilderImpl(CreateAwsKmsHierarchicalKeyringInput model) { @@ -166,6 +191,7 @@ protected BuilderImpl(CreateAwsKmsHierarchicalKeyringInput model) { this.ttlSeconds = model.ttlSeconds(); this._ttlSecondsSet = true; this.cache = model.cache(); + this.partitionId = model.partitionId(); } public Builder branchKeyId(String branchKeyId) { @@ -216,6 +242,15 @@ public CacheType cache() { return this.cache; } + public Builder partitionId(String partitionId) { + this.partitionId = partitionId; + return this; + } + + public String partitionId() { + return this.partitionId; + } + public CreateAwsKmsHierarchicalKeyringInput build() { if (Objects.isNull(this.keyStore())) { throw new IllegalArgumentException( diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/CacheType.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/CacheType.cs index adf4c8b69..647e263c3 100644 --- a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/CacheType.cs +++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/CacheType.cs @@ -12,6 +12,7 @@ public class CacheType private AWS.Cryptography.MaterialProviders.SingleThreadedCache _singleThreaded; private AWS.Cryptography.MaterialProviders.MultiThreadedCache _multiThreaded; private AWS.Cryptography.MaterialProviders.StormTrackingCache _stormTracking; + private AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache _shared; public AWS.Cryptography.MaterialProviders.DefaultCache Default { get { return this._default; } @@ -57,13 +58,23 @@ public bool IsSetStormTracking() { return this._stormTracking != null; } + public AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache Shared + { + get { return this._shared; } + set { this._shared = value; } + } + public bool IsSetShared() + { + return this._shared != null; + } public void Validate() { var numberOfPropertiesSet = Convert.ToUInt16(IsSetDefault()) + Convert.ToUInt16(IsSetNo()) + Convert.ToUInt16(IsSetSingleThreaded()) + Convert.ToUInt16(IsSetMultiThreaded()) + - Convert.ToUInt16(IsSetStormTracking()); + Convert.ToUInt16(IsSetStormTracking()) + + Convert.ToUInt16(IsSetShared()); if (numberOfPropertiesSet == 0) throw new System.ArgumentException("No union value set"); if (numberOfPropertiesSet > 1) throw new System.ArgumentException("Multiple union values set"); diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/CreateAwsKmsHierarchicalKeyringInput.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/CreateAwsKmsHierarchicalKeyringInput.cs index 41dfa398e..542702bc5 100644 --- a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/CreateAwsKmsHierarchicalKeyringInput.cs +++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/CreateAwsKmsHierarchicalKeyringInput.cs @@ -12,6 +12,7 @@ public class CreateAwsKmsHierarchicalKeyringInput private AWS.Cryptography.KeyStore.KeyStore _keyStore; private long? _ttlSeconds; private AWS.Cryptography.MaterialProviders.CacheType _cache; + private string _partitionId; public string BranchKeyId { get { return this._branchKeyId; } @@ -57,6 +58,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 (!IsSetKeyStore()) throw new System.ArgumentException("Missing value for required property 'KeyStore'"); diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs index 3f953819b..56aef9ec6 100644 --- a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs +++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs @@ -111,6 +111,11 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12 converted.StormTracking = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(concrete.dtor_StormTracking); return converted; } + if (value.is_Shared) + { + converted.Shared = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(concrete.dtor_Shared); + return converted; + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(AWS.Cryptography.MaterialProviders.CacheType value) @@ -135,6 +140,10 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_StormTracking(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(value.StormTracking)); } + if (value.IsSetShared()) + { + return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_Shared(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(value.Shared)); + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static AWS.Cryptography.MaterialProviders.CommitmentPolicy FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_CommitmentPolicy(software.amazon.cryptography.materialproviders.internaldafny.types._ICommitmentPolicy value) @@ -211,7 +220,8 @@ public static AWS.Cryptography.MaterialProviders.CreateAwsKmsHierarchicalKeyring if (concrete._branchKeyIdSupplier.is_Some) converted.BranchKeyIdSupplier = (AWS.Cryptography.MaterialProviders.IBranchKeyIdSupplier)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M19_branchKeyIdSupplier(concrete._branchKeyIdSupplier); converted.KeyStore = (AWS.Cryptography.KeyStore.KeyStore)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M8_keyStore(concrete._keyStore); converted.TtlSeconds = (long)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M10_ttlSeconds(concrete._ttlSeconds); - if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M5_cache(concrete._cache); return converted; + if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M5_cache(concrete._cache); + if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M11_partitionId(concrete._partitionId); return converted; } public static software.amazon.cryptography.materialproviders.internaldafny.types._ICreateAwsKmsHierarchicalKeyringInput ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput(AWS.Cryptography.MaterialProviders.CreateAwsKmsHierarchicalKeyringInput value) { @@ -219,7 +229,8 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types string var_branchKeyId = value.IsSetBranchKeyId() ? value.BranchKeyId : (string)null; AWS.Cryptography.MaterialProviders.IBranchKeyIdSupplier var_branchKeyIdSupplier = value.IsSetBranchKeyIdSupplier() ? value.BranchKeyIdSupplier : (AWS.Cryptography.MaterialProviders.IBranchKeyIdSupplier)null; AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null; - return new software.amazon.cryptography.materialproviders.internaldafny.types.CreateAwsKmsHierarchicalKeyringInput(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M11_branchKeyId(var_branchKeyId), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M19_branchKeyIdSupplier(var_branchKeyIdSupplier), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M8_keyStore(value.KeyStore), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M10_ttlSeconds(value.TtlSeconds), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M5_cache(var_cache)); + string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null; + return new software.amazon.cryptography.materialproviders.internaldafny.types.CreateAwsKmsHierarchicalKeyringInput(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M11_branchKeyId(var_branchKeyId), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M19_branchKeyIdSupplier(var_branchKeyIdSupplier), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M8_keyStore(value.KeyStore), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M10_ttlSeconds(value.TtlSeconds), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M11_partitionId(var_partitionId)); } public static AWS.Cryptography.MaterialProviders.CreateAwsKmsKeyringInput FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S24_CreateAwsKmsKeyringInput(software.amazon.cryptography.materialproviders.internaldafny.types._ICreateAwsKmsKeyringInput value) { @@ -1395,6 +1406,14 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache(value); } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_CommitmentPolicy__M4_ESDK(software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(value); @@ -1539,6 +1558,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__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__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__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__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__N17_materialProviders__S24_CreateAwsKmsKeyringInput__M8_kmsKeyId(Dafny.ISequence value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S8_KmsKeyId(value); @@ -2810,6 +2837,25 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types int? var_entryPruningTailSize = value.IsSetEntryPruningTailSize() ? value.EntryPruningTailSize : (int?)null; return new software.amazon.cryptography.materialproviders.internaldafny.types.StormTrackingCache(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_entryCapacity(value.EntryCapacity), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M20_entryPruningTailSize(var_entryPruningTailSize), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_gracePeriod(value.GracePeriod), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_graceInterval(value.GraceInterval), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M6_fanOut(value.FanOut), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_inFlightTTL(value.InFlightTTL), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M10_sleepMilli(value.SleepMilli)); } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + if (value is NativeWrapper_CryptographicMaterialsCache nativeWrapper) return nativeWrapper._impl; + return new CryptographicMaterialsCache(value); + + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + switch (value) + { + case CryptographicMaterialsCache valueWithImpl: + return valueWithImpl._impl; + case CryptographicMaterialsCacheBase nativeImpl: + return new NativeWrapper_CryptographicMaterialsCache(nativeImpl); + default: + throw new System.ArgumentException( + "Custom implementations of CryptographicMaterialsCache must extend CryptographicMaterialsCacheBase."); + } + } public static Amazon.KeyManagementService.IAmazonKeyManagementService FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_KmsClientReference(software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient value) { if (value is Com.Amazonaws.Kms.KeyManagementServiceShim shim) { return shim._impl; } @@ -2976,25 +3022,6 @@ public static software.amazon.cryptography.services.kms.internaldafny.types._IEn if (Amazon.KeyManagementService.EncryptionAlgorithmSpec.RSAES_OAEP_SHA_256.Equals(value)) return software.amazon.cryptography.services.kms.internaldafny.types.EncryptionAlgorithmSpec.create_RSAES__OAEP__SHA__256(); throw new System.ArgumentException("Invalid Amazon.KeyManagementService.EncryptionAlgorithmSpec value"); } - public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) - { - if (value is NativeWrapper_CryptographicMaterialsCache nativeWrapper) return nativeWrapper._impl; - return new CryptographicMaterialsCache(value); - - } - public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) - { - switch (value) - { - case CryptographicMaterialsCache valueWithImpl: - return valueWithImpl._impl; - case CryptographicMaterialsCacheBase nativeImpl: - return new NativeWrapper_CryptographicMaterialsCache(nativeImpl); - default: - throw new System.ArgumentException( - "Custom implementations of CryptographicMaterialsCache must extend CryptographicMaterialsCacheBase."); - } - } public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsManager value) { if (value is NativeWrapper_CryptographicMaterialsManager nativeWrapper) return nativeWrapper._impl; diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/CreateStaticKeyStores.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/CreateStaticKeyStores.dfy index ab54d7f60..f14550749 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/CreateStaticKeyStores.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/CreateStaticKeyStores.dfy @@ -135,8 +135,6 @@ module {:options "-functionSyntax:4"} CreateStaticKeyStores { History.GetBeaconKey := History.GetBeaconKey + [DafnyCallEvent(input, output)]; } - // These are all not supported operations in a static context - ghost predicate GetKeyStoreInfoEnsuresPublicly(output: Result) {true} @@ -153,10 +151,20 @@ module {:options "-functionSyntax:4"} CreateStaticKeyStores { ensures GetKeyStoreInfoEnsuresPublicly(output) ensures History.GetKeyStoreInfo == old(History.GetKeyStoreInfo) + [DafnyCallEvent((), output)] { - output := Failure(KeyStoreException( message := "Not Supported")); + output := Success( + AwsCryptographyKeyStoreTypes.GetKeyStoreInfoOutput( + keyStoreId := "key-store-id", + keyStoreName := "key-store-name", + logicalKeyStoreName := "logical-key-store-name", + grantTokens := [], + kmsConfiguration := KMSConfiguration.kmsKeyArn("arn:aws:kms:us-east-2:111122223333:key/1234abcd-12ab-34cd-56ef-1234567890ab") + ) + ); History.GetKeyStoreInfo := History.GetKeyStoreInfo + [DafnyCallEvent((), output)]; } + // All methods except GetKeyStoreInfo are not supported operations in a static context + ghost predicate CreateKeyStoreEnsuresPublicly(input: CreateKeyStoreInput , output: Result) {true} // The public method to be called by library consumers diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy index fd2f26828..4122112cc 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy @@ -211,7 +211,8 @@ module {:options "-functionSyntax:4"} KeyringFromKeyDescription { branchKeyIdSupplier := None, keyStore := keyStore, ttlSeconds := 0, - cache := None + cache := None, + partitionId := None ); var keyring := mpl.CreateAwsKmsHierarchicalKeyring(input); return keyring.MapFailure(e => AwsCryptographyMaterialProviders(e)); diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs index 79e337745..e477a7882 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs @@ -111,6 +111,11 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12 converted.StormTracking = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(concrete.dtor_StormTracking); return converted; } + if (value.is_Shared) + { + converted.Shared = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(concrete.dtor_Shared); + return converted; + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(AWS.Cryptography.MaterialProviders.CacheType value) @@ -135,6 +140,10 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_StormTracking(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(value.StormTracking)); } + if (value.IsSetShared()) + { + return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_Shared(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(value.Shared)); + } throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state"); } public static AWS.Cryptography.MaterialProviders.CommitmentPolicy FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_CommitmentPolicy(software.amazon.cryptography.materialproviders.internaldafny.types._ICommitmentPolicy value) @@ -211,7 +220,8 @@ public static AWS.Cryptography.MaterialProviders.CreateAwsKmsHierarchicalKeyring if (concrete._branchKeyIdSupplier.is_Some) converted.BranchKeyIdSupplier = (AWS.Cryptography.MaterialProviders.IBranchKeyIdSupplier)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M19_branchKeyIdSupplier(concrete._branchKeyIdSupplier); converted.KeyStore = (AWS.Cryptography.KeyStore.KeyStore)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M8_keyStore(concrete._keyStore); converted.TtlSeconds = (long)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M10_ttlSeconds(concrete._ttlSeconds); - if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M5_cache(concrete._cache); return converted; + if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M5_cache(concrete._cache); + if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M11_partitionId(concrete._partitionId); return converted; } public static software.amazon.cryptography.materialproviders.internaldafny.types._ICreateAwsKmsHierarchicalKeyringInput ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput(AWS.Cryptography.MaterialProviders.CreateAwsKmsHierarchicalKeyringInput value) { @@ -219,7 +229,8 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types string var_branchKeyId = value.IsSetBranchKeyId() ? value.BranchKeyId : (string)null; AWS.Cryptography.MaterialProviders.IBranchKeyIdSupplier var_branchKeyIdSupplier = value.IsSetBranchKeyIdSupplier() ? value.BranchKeyIdSupplier : (AWS.Cryptography.MaterialProviders.IBranchKeyIdSupplier)null; AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null; - return new software.amazon.cryptography.materialproviders.internaldafny.types.CreateAwsKmsHierarchicalKeyringInput(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M11_branchKeyId(var_branchKeyId), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M19_branchKeyIdSupplier(var_branchKeyIdSupplier), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M8_keyStore(value.KeyStore), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M10_ttlSeconds(value.TtlSeconds), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M5_cache(var_cache)); + string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null; + return new software.amazon.cryptography.materialproviders.internaldafny.types.CreateAwsKmsHierarchicalKeyringInput(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M11_branchKeyId(var_branchKeyId), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M19_branchKeyIdSupplier(var_branchKeyIdSupplier), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M8_keyStore(value.KeyStore), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M10_ttlSeconds(value.TtlSeconds), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__M11_partitionId(var_partitionId)); } public static AWS.Cryptography.MaterialProviders.CreateAwsKmsKeyringInput FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S24_CreateAwsKmsKeyringInput(software.amazon.cryptography.materialproviders.internaldafny.types._ICreateAwsKmsKeyringInput value) { @@ -1395,6 +1406,14 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache(value); } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_CommitmentPolicy__M4_ESDK(software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(value); @@ -1539,6 +1558,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__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__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__N17_materialProviders__S36_CreateAwsKmsHierarchicalKeyringInput__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__N17_materialProviders__S24_CreateAwsKmsKeyringInput__M8_kmsKeyId(Dafny.ISequence value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S8_KmsKeyId(value); @@ -2810,6 +2837,18 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types int? var_entryPruningTailSize = value.IsSetEntryPruningTailSize() ? value.EntryPruningTailSize : (int?)null; return new software.amazon.cryptography.materialproviders.internaldafny.types.StormTrackingCache(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_entryCapacity(value.EntryCapacity), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M20_entryPruningTailSize(var_entryPruningTailSize), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_gracePeriod(value.GracePeriod), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_graceInterval(value.GraceInterval), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M6_fanOut(value.FanOut), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_inFlightTTL(value.InFlightTTL), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M10_sleepMilli(value.SleepMilli)); } + internal static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); + } + internal static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) + { + // This is converting a reference type in a dependant module. + // Therefore it defers to the dependant module for conversion + return new WrappedNativeWrapper_CryptographicMaterialsCache((CryptographicMaterialsCacheBase)value); + } public static Amazon.KeyManagementService.IAmazonKeyManagementService FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_KmsClientReference(software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient value) { // This is converting a reference type in a dependant module. @@ -2960,18 +2999,6 @@ public static software.amazon.cryptography.services.kms.internaldafny.types._IEn if (Amazon.KeyManagementService.EncryptionAlgorithmSpec.RSAES_OAEP_SHA_256.Equals(value)) return software.amazon.cryptography.services.kms.internaldafny.types.EncryptionAlgorithmSpec.create_RSAES__OAEP__SHA__256(); throw new System.ArgumentException("Invalid Amazon.KeyManagementService.EncryptionAlgorithmSpec value"); } - internal static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value) - { - // This is converting a reference type in a dependant module. - // Therefore it defers to the dependant module for conversion - return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value); - } - internal static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value) - { - // This is converting a reference type in a dependant module. - // Therefore it defers to the dependant module for conversion - return new WrappedNativeWrapper_CryptographicMaterialsCache((CryptographicMaterialsCacheBase)value); - } internal static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsManager value) { // This is converting a reference type in a dependant module.