Skip to content

feat: Adding Caching CMM #80

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

feat: Adding Caching CMM #80

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
671bf19
feat: Adding Caching CMM
seebees Mar 20, 2025
8fffbea
Small updates
seebees Mar 20, 2025
cb45a30
first cut
seebees Mar 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
135 changes: 131 additions & 4 deletions ...s/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
CreateRawEcdhKeyring := [];
CreateDefaultCryptographicMaterialsManager := [];
CreateRequiredEncryptionContextCMM := [];
CreateCachingCMM := [];
CreateCryptographicMaterialsCache := [];
CreateDefaultClientSupplier := [];
InitializeEncryptionMaterials := [];
Expand Down Expand Up @@ -89,6 +90,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
ghost var CreateRawEcdhKeyring: seq<DafnyCallEvent<CreateRawEcdhKeyringInput, Result<IKeyring, Error>>>
ghost var CreateDefaultCryptographicMaterialsManager: seq<DafnyCallEvent<CreateDefaultCryptographicMaterialsManagerInput, Result<ICryptographicMaterialsManager, Error>>>
ghost var CreateRequiredEncryptionContextCMM: seq<DafnyCallEvent<CreateRequiredEncryptionContextCMMInput, Result<ICryptographicMaterialsManager, Error>>>
ghost var CreateCachingCMM: seq<DafnyCallEvent<CreateCachingCMMInput, Result<ICryptographicMaterialsManager, Error>>>
ghost var CreateCryptographicMaterialsCache: seq<DafnyCallEvent<CreateCryptographicMaterialsCacheInput, Result<ICryptographicMaterialsCache, Error>>>
ghost var CreateDefaultClientSupplier: seq<DafnyCallEvent<CreateDefaultClientSupplierInput, Result<IClientSupplier, Error>>>
ghost var InitializeEncryptionMaterials: seq<DafnyCallEvent<InitializeEncryptionMaterialsInput, Result<EncryptionMaterials, Error>>>
Expand Down Expand Up @@ -604,6 +606,44 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
ensures CreateRequiredEncryptionContextCMMEnsuresPublicly(input, output)
ensures History.CreateRequiredEncryptionContextCMM == old(History.CreateRequiredEncryptionContextCMM) + [DafnyCallEvent(input, output)]

predicate CreateCachingCMMEnsuresPublicly(input: CreateCachingCMMInput , output: Result<ICryptographicMaterialsManager, Error>)
// The public method to be called by library consumers
method CreateCachingCMM ( input: CreateCachingCMMInput )
returns (output: Result<ICryptographicMaterialsManager, Error>)
requires
&& ValidState()
&& input.underlyingCMC.ValidState()
&& input.underlyingCMC.Modifies !! {History} && ( input.underlyingCMM.Some? ==>
&& input.underlyingCMM.value.ValidState()
&& input.underlyingCMM.value.Modifies !! {History}
) && ( input.keyring.Some? ==>
&& input.keyring.value.ValidState()
&& input.keyring.value.Modifies !! {History}
)
modifies Modifies - {History} ,
input.underlyingCMC.Modifies ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {}) ,
History`CreateCachingCMM
// Dafny will skip type parameters when generating a default decreases clause.
decreases Modifies - {History} ,
input.underlyingCMC.Modifies ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {})
ensures
&& ValidState()
&& ( output.Success? ==>
&& output.value.ValidState()
&& output.value.Modifies !! {History}
&& fresh(output.value)
&& fresh ( output.value.Modifies
- Modifies - {History}
- input.underlyingCMC.Modifies
- (if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {})
- (if input.keyring.Some? then input.keyring.value.Modifies else {}) ) )
ensures CreateCachingCMMEnsuresPublicly(input, output)
ensures History.CreateCachingCMM == old(History.CreateCachingCMM) + [DafnyCallEvent(input, output)]

predicate CreateCryptographicMaterialsCacheEnsuresPublicly(input: CreateCryptographicMaterialsCacheInput , output: Result<ICryptographicMaterialsCache, Error>)
// The public method to be called by library consumers
method CreateCryptographicMaterialsCache ( input: CreateCryptographicMaterialsCacheInput )
Expand Down Expand Up @@ -951,6 +991,15 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
nameonly kmsClient: Option<ComAmazonawsKmsTypes.IKMSClient> := Option.None ,
nameonly grantTokens: Option<GrantTokenList> := Option.None
)
datatype CreateCachingCMMInput = | CreateCachingCMMInput (
nameonly underlyingCMC: ICryptographicMaterialsCache ,
nameonly cacheLimitTtlSeconds: PositiveInteger ,
nameonly underlyingCMM: Option<ICryptographicMaterialsManager> := Option.None ,
nameonly keyring: Option<IKeyring> := Option.None ,
nameonly partitionKey: Option<Utf8Bytes> := Option.None ,
nameonly limitBytes: Option<int64> := Option.None ,
nameonly limitMessages: Option<int32> := Option.None
)
datatype CreateCryptographicMaterialsCacheInput = | CreateCryptographicMaterialsCacheInput (
nameonly cache: CacheType
)
Expand Down Expand Up @@ -1376,14 +1425,14 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
)
datatype GetCacheEntryInput = | GetCacheEntryInput (
nameonly identifier: seq<uint8> ,
nameonly bytesUsed: Option<int64> := Option.None
nameonly bytesUsed: Option<PositiveLong> := Option.None
)
datatype GetCacheEntryOutput = | GetCacheEntryOutput (
nameonly materials: Materials ,
nameonly creationTime: PositiveLong ,
nameonly expiryTime: PositiveLong ,
nameonly messagesUsed: PositiveInteger ,
nameonly bytesUsed: PositiveInteger
nameonly bytesUsed: PositiveLong
)
datatype GetClientInput = | GetClientInput (
nameonly region: Region
Expand Down Expand Up @@ -1593,7 +1642,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
nameonly creationTime: PositiveLong ,
nameonly expiryTime: PositiveLong ,
nameonly messagesUsed: Option<PositiveInteger> := Option.None ,
nameonly bytesUsed: Option<PositiveInteger> := Option.None
nameonly bytesUsed: Option<PositiveLong> := Option.None
)
datatype RawEcdhStaticConfigurations =
| PublicKeyDiscovery(PublicKeyDiscovery: PublicKeyDiscoveryInput)
Expand Down Expand Up @@ -1635,7 +1684,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
| Milliseconds
datatype UpdateUsageMetadataInput = | UpdateUsageMetadataInput (
nameonly identifier: seq<uint8> ,
nameonly bytesUsed: PositiveInteger
nameonly bytesUsed: PositiveLong
)
type Utf8Bytes = ValidUTF8Bytes
datatype ValidateCommitmentPolicyOnDecryptInput = | ValidateCommitmentPolicyOnDecryptInput (
Expand Down Expand Up @@ -2328,6 +2377,49 @@ abstract module AbstractAwsCryptographyMaterialProvidersService
History.CreateRequiredEncryptionContextCMM := History.CreateRequiredEncryptionContextCMM + [DafnyCallEvent(input, output)];
}

predicate CreateCachingCMMEnsuresPublicly(input: CreateCachingCMMInput , output: Result<ICryptographicMaterialsManager, Error>)
{Operations.CreateCachingCMMEnsuresPublicly(input, output)}
// The public method to be called by library consumers
method CreateCachingCMM ( input: CreateCachingCMMInput )
returns (output: Result<ICryptographicMaterialsManager, Error>)
requires
&& ValidState()
&& input.underlyingCMC.ValidState()
&& input.underlyingCMC.Modifies !! {History} && ( input.underlyingCMM.Some? ==>
&& input.underlyingCMM.value.ValidState()
&& input.underlyingCMM.value.Modifies !! {History}
) && ( input.keyring.Some? ==>
&& input.keyring.value.ValidState()
&& input.keyring.value.Modifies !! {History}
)
modifies Modifies - {History} ,
input.underlyingCMC.Modifies ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {}) ,
History`CreateCachingCMM
// Dafny will skip type parameters when generating a default decreases clause.
decreases Modifies - {History} ,
input.underlyingCMC.Modifies ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {})
ensures
&& ValidState()
&& ( output.Success? ==>
&& output.value.ValidState()
&& output.value.Modifies !! {History}
&& fresh(output.value)
&& fresh ( output.value.Modifies
- Modifies - {History}
- input.underlyingCMC.Modifies
- (if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {})
- (if input.keyring.Some? then input.keyring.value.Modifies else {}) ) )
ensures CreateCachingCMMEnsuresPublicly(input, output)
ensures History.CreateCachingCMM == old(History.CreateCachingCMM) + [DafnyCallEvent(input, output)]
{
output := Operations.CreateCachingCMM(config, input);
History.CreateCachingCMM := History.CreateCachingCMM + [DafnyCallEvent(input, output)];
}

predicate CreateCryptographicMaterialsCacheEnsuresPublicly(input: CreateCryptographicMaterialsCacheInput , output: Result<ICryptographicMaterialsCache, Error>)
{Operations.CreateCryptographicMaterialsCacheEnsuresPublicly(input, output)}
// The public method to be called by library consumers
Expand Down Expand Up @@ -2959,6 +3051,41 @@ abstract module AbstractAwsCryptographyMaterialProvidersOperations {
ensures CreateRequiredEncryptionContextCMMEnsuresPublicly(input, output)


predicate CreateCachingCMMEnsuresPublicly(input: CreateCachingCMMInput , output: Result<ICryptographicMaterialsManager, Error>)
// The private method to be refined by the library developer


method CreateCachingCMM ( config: InternalConfig , input: CreateCachingCMMInput )
returns (output: Result<ICryptographicMaterialsManager, Error>)
requires
&& ValidInternalConfig?(config)
&& input.underlyingCMC.ValidState() && ( input.underlyingCMM.Some? ==>
&& input.underlyingCMM.value.ValidState()
) && ( input.keyring.Some? ==>
&& input.keyring.value.ValidState()
)
modifies ModifiesInternalConfig(config) ,
input.underlyingCMC.Modifies ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {})
// Dafny will skip type parameters when generating a default decreases clause.
decreases ModifiesInternalConfig(config) ,
input.underlyingCMC.Modifies ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {})
ensures
&& ValidInternalConfig?(config)
&& ( output.Success? ==>
&& output.value.ValidState()
&& fresh(output.value)
&& fresh ( output.value.Modifies
- ModifiesInternalConfig(config)
- input.underlyingCMC.Modifies
- (if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {})
- (if input.keyring.Some? then input.keyring.value.Modifies else {}) ) )
ensures CreateCachingCMMEnsuresPublicly(input, output)


predicate CreateCryptographicMaterialsCacheEnsuresPublicly(input: CreateCryptographicMaterialsCacheInput , output: Result<ICryptographicMaterialsCache, Error>)
// The private method to be refined by the library developer

Expand Down
55 changes: 55 additions & 0 deletions AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/cmms.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -158,3 +158,58 @@ structure CreateRequiredEncryptionContextCMMInput {
@javadoc("A list of Encryption Context keys which are required to be supplied during encryption and decryption, and correspond to Encryption Context key-value pairs which are not stored on the resulting message.")
requiredEncryptionContextKeys: EncryptionContextKeys
}

@positional
@javadoc("Outputs for creating a Caching Cryptographic Materials Manager.")
structure CreateCachingCMMOutput {
@required
@javadoc("The created Caching Cryptographic Materials Manager.")
materialsManager: CryptographicMaterialsManagerReference
}

@javadoc("Creates a Caching Cryptographic Materials Manager.")
operation CreateCachingCMM {
input: CreateCachingCMMInput,
output: CreateCachingCMMOutput,
}

@javadoc("Inputs for creating a Caching Cryptographic Materials Manager.")
structure CreateCachingCMMInput {

//= aws-encryption-sdk-specification/framework/caching-cmm.md#initialization
//= type=implication
//# On caching CMM initialization,
//# the caller MUST provide the following values:
//# - [Underlying Cryptographic Materials Cache (CMC)](#underlying-cryptographic-materials-cache)
//# - [Cache Limit TTL](#cache-limit-ttl)
@required
@javadoc("The Cryptographic Materials Cache the Caching Cryptographic Materials Manager will use to cache requests.")
underlyingCMC: CryptographicMaterialsCacheReference,
@required
@javadoc("Sets the maximum lifetime for entries in the cache, for both encrypt and decrypt operations. When the specified amount of time passes after initial creation of the entry, the entry will be considered unusable, and the next operation will incur a cache miss.")
Copy link
Contributor

@texastony texastony Oct 3, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit/Suggestion: we cache materials, not operations

Suggested change
@javadoc("Sets the maximum lifetime for entries in the cache, for both encrypt and decrypt operations. When the specified amount of time passes after initial creation of the entry, the entry will be considered unusable, and the next operation will incur a cache miss.")
@javadoc("Sets the maximum lifetime for entries in the cache, for both encrypt and decrypt materials. When the specified amount of time passes after initial creation of the entry, the entry will be considered unusable, and the next operation will incur a cache miss.")

Copy link
Contributor Author

@seebees seebees Oct 10, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hum, I think I want operations but I'm not sure.
The point here is that there is 1 cache.
But that items put in from encrypt are not hits on decrypt.

cacheLimitTtlSeconds: PositiveInteger,

//= aws-encryption-sdk-specification/framework/caching-cmm.md#initialization
//= type=implication
//# Additionally, the caller MUST provide one of the following values:
//# - [Underlying Cryptographic Materials Manager (CMM)](#underlying-cryptographic-materials-manager)
//# - [Keyring](keyring-interface.md)
@javadoc("The Cryptographic Materials Manager that the created Caching Cryptographic Materials Manager will delegate to. Either a Keyring or underlying Cryptographic Materials Manager must be specified.")
underlyingCMM: CryptographicMaterialsManagerReference,
@javadoc("The Keyring that the created Cryptographic Materials Manager will use to wrap data keys. The created Caching CMM will delegate to a Default Cryptographic Materials Manager created with this Keyring. Either a Keyring or an underlying Cryptographic Materials Manager must be specified as input.")
keyring: KeyringReference,

//= aws-encryption-sdk-specification/framework/caching-cmm.md#initialization
//= type=implication
//# Finally, the caching CMM MUST optionally accept the following values:
//# - [Partition ID](#partition-id)
//# - [Limit Bytes](#limit-bytes)
//# - [Limit Messages](#limit-messages)
@javadoc("Sets the partition ID for this CMM. By default, two CMMs will never use each other's cache entries. This helps ensure that CMMs with different delegates won't incorrectly use each other's encrypt and decrypt results. However, in certain special circumstances it can be useful to share entries between different CMMs - for example, if the backing CMM is constructed based on some parameters that depend on the operation, you may wish for delegates constructed with the same parameters to share the same partition. To accomplish this, set the same partition ID and backing cache on both CMMs; entries cached from one of these CMMs can then be used by the other. This should only be done with careful consideration and verification that the CMM delegates are equivalent for your application's purposes. By default, the partition ID is set to a random UUID to avoid any collisions.")
Copy link
Contributor

@texastony texastony Oct 3, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Question: javadoc is not handled by our Polymorph-.NET.
Is this content recorded in the public hosted docs?
Otherwise, .NET customers will never receive it.

Copy link
Contributor Author

@seebees seebees Oct 10, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This content comes from the ESDK-Java.
So it is somewhat public.
I'd like to get javadoc to work in every language so we don't have to worry about this :)

partitionKey: Utf8Bytes,
@javadoc("Sets the maximum number of plaintext bytes that can be encrypted under the same cached data key. This does not affect decrypt operations. Specifying this limit is optional; by default, the limit is set to 2^63 - 1. If this limit is set to zero, keys can only be cached if they are used for zero-length messages.")
limitBytes: Long,
@javadoc("Sets the maximum number of individual messages that can be encrypted under the same cached data key. This does not affect decrypt operations. Specifying this limit is optional; by default, the limit is set to 2^32. This is also the maximum accepted value.")
limitMessages: Integer,

}
8 changes: 4 additions & 4 deletions ...viders/dafny/AwsCryptographicMaterialProviders/Model/cryptographic-materials-cache.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ structure PutCacheEntryInput {
//# since this information can not be updated after the put operation.
expiryTime: PositiveLong,
messagesUsed: PositiveInteger,
bytesUsed: PositiveInteger,
bytesUsed: PositiveLong,
}

operation GetCacheEntry {
Expand All @@ -56,7 +56,7 @@ operation GetCacheEntry {
structure GetCacheEntryInput {
@required
identifier: Blob,
bytesUsed: Long
bytesUsed: PositiveLong

}

Expand Down Expand Up @@ -84,7 +84,7 @@ structure GetCacheEntryOutput {
@required
messagesUsed: PositiveInteger,
@required
bytesUsed: PositiveInteger,
bytesUsed: PositiveLong,
}

union Materials {
Expand All @@ -111,7 +111,7 @@ structure UpdateUsageMetadataInput {
@required
identifier: Blob,
@required
bytesUsed: PositiveInteger,
bytesUsed: PositiveLong,
}

@error("client")
Expand Down
1 change: 1 addition & 0 deletions ...cMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/material-provider.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ service AwsCryptographicMaterialProviders {
// CMMs
CreateDefaultCryptographicMaterialsManager,
CreateRequiredEncryptionContextCMM,
CreateCachingCMM,

// CMCs
CreateCryptographicMaterialsCache,
Expand Down
Loading
Loading