Skip to content

Commit 57f6ea6

Browse files
RitvikKapilaRitvikKapila
committed
update smithy models
1 parent 58f411e commit 57f6ea6

File tree

5 files changed

+40
-23
lines changed

5 files changed

+40
-23
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -354,7 +354,8 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
354354
datatype MultiKeyStore = | MultiKeyStore (
355355
nameonly keyFieldName: string ,
356356
nameonly cacheTTL: int32 ,
357-
nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType> := Option.None
357+
nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType> := Option.None ,
358+
nameonly partitionId: Option<string> := Option.None
358359
)
359360
datatype PartOnly = | PartOnly (
360361

@@ -388,7 +389,9 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
388389
}
389390
datatype SingleKeyStore = | SingleKeyStore (
390391
nameonly keyId: string ,
391-
nameonly cacheTTL: int32
392+
nameonly cacheTTL: Option<int32> := Option.None ,
393+
nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType> := Option.None ,
394+
nameonly partitionId: Option<string> := Option.None
392395
)
393396
datatype StandardBeacon = | StandardBeacon (
394397
nameonly name: string ,

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -713,9 +713,12 @@ structure SingleKeyStore {
713713
@required
714714
@javadoc("The Beacon Key ID.")
715715
keyId : String,
716-
@required
717-
@javadoc("How long (in seconds) the beacon key material is cached locally before it is re-retrieved from DynamoDB and re-authed with AWS KMS.")
716+
@javadoc("How long (in seconds) the beacon key material is cached locally before it is re-retrieved from DynamoDB and re-authed with AWS KMS. Provide only one of cacheTTL or cache.")
718717
cacheTTL: Integer,
718+
@documentation("Provide the Shared Cache for Searchable Encryption. Provide only one of cacheTTL or cache.")
719+
cache : CacheType,
720+
@documentation("Partition ID to share DynamoDB Interceptors. TODO: Update description")
721+
partitionId: String
719722
}
720723

721724
//= specification/searchable-encryption/search-config.md#multi-key-store-initialization
@@ -734,7 +737,9 @@ structure MultiKeyStore {
734737
@javadoc("How long (in seconds) the beacon key material is cached locally before it is re-retrieved from DynamoDB and re-authed with AWS KMS.")
735738
cacheTTL: Integer,
736739
@javadoc("Which type of local cache to use.")
737-
cache : CacheType
740+
cache : CacheType,
741+
@documentation("Partition ID to share DynamoDB Interceptors. TODO: Update description")
742+
partitionId: String
738743
}
739744

740745
//= specification/searchable-encryption/search-config.md#beacon-key-source

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -138,6 +138,7 @@ module SearchConfigToInfo {
138138
else
139139
MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1));
140140

141+
// TODO : Add check that customers only provide either cacheTTL or cache in case of SingleKeyStore
141142
var cache;
142143
if cacheType.Shared? {
143144
cache := cacheType.Shared;

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ module SearchableEncryptionInfo {
2626
import MP = AwsCryptographyMaterialProvidersTypes
2727
import KeyStoreTypes = AwsCryptographyKeyStoreTypes
2828
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
29-
import CacheConstants
29+
import opened CacheConstants
3030

3131
//= specification/searchable-encryption/search-config.md#version-number
3232
//= type=implication
@@ -246,11 +246,19 @@ module SearchableEncryptionInfo {
246246
{
247247

248248
// Resource ID: Searchable Encryption [0x02]
249-
// var resourceId : seq<uint8> := RESOURCE_ID_HIERARCHICAL_KEYRING;
249+
var resourceId : seq<uint8> := RESOURCE_ID_HIERARCHICAL_KEYRING;
250250

251+
// Scope ID: Searchable Encryption [0x03]
252+
var scopeId : seq<uint8> := SCOPE_ID_SEARCHABLE_ENCRYPTION;
251253

254+
// Create the Suffix
252255
var keyIdBytesR := UTF8.Encode(keyId);
253256
var keyIdBytes :- keyIdBytesR.MapFailure(e => E(e));
257+
var suffix : seq<uint8> := keyIdBytes;
258+
259+
// Append Resource Id, Scope Id, Partition Id, and Suffix to create the cache identifier
260+
var identifier := resourceId + NULL_BYTE + scopeId + NULL_BYTE + partitionIdBytes + NULL_BYTE + suffix;
261+
254262
var getCacheInput := MP.GetCacheEntryInput(identifier := keyIdBytes, bytesUsed := None);
255263
verifyValidStateCache(cache);
256264
assume {:axiom} cache.Modifies == {};

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy‎

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -764,10 +764,10 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
764764
tmp5.search.Some? ==>
765765
var tmps6 := set t6 | t6 in tmp5.search.value.versions;
766766
forall tmp6 :: tmp6 in tmps6 ==>
767-
tmp6.keySource.multi? ==>
768-
tmp6.keySource.multi.cache.Some? ==>
769-
tmp6.keySource.multi.cache.value.Shared? ==>
770-
tmp6.keySource.multi.cache.value.Shared.ValidState()
767+
tmp6.keySource.single? ==>
768+
tmp6.keySource.single.cache.Some? ==>
769+
tmp6.keySource.single.cache.value.Shared? ==>
770+
tmp6.keySource.single.cache.value.Shared.ValidState()
771771
modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true
772772
&& t7.keyring.Some?
773773
:: t7.keyring.value,
@@ -788,10 +788,10 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
788788
modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
789789
&& t12.search.Some?
790790
, t13 <- t12.search.value.versions | true
791-
&& t13.keySource.multi?
792-
&& t13.keySource.multi.cache.Some?
793-
&& t13.keySource.multi.cache.value.Shared?
794-
:: t13.keySource.multi.cache.value.Shared,
791+
&& t13.keySource.single?
792+
&& t13.keySource.single.cache.Some?
793+
&& t13.keySource.single.cache.value.Shared?
794+
:: t13.keySource.single.cache.value.Shared,
795795
obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
796796
ensures res.Success? ==>
797797
&& fresh(res.value)
@@ -816,10 +816,10 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
816816
) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true
817817
&& t19.search.Some?
818818
, t20 <- t19.search.value.versions | true
819-
&& t20.keySource.multi?
820-
&& t20.keySource.multi.cache.Some?
821-
&& t20.keySource.multi.cache.value.Shared?
822-
:: t20.keySource.multi.cache.value.Shared,
819+
&& t20.keySource.single?
820+
&& t20.keySource.single.cache.Some?
821+
&& t20.keySource.single.cache.value.Shared?
822+
:: t20.keySource.single.cache.value.Shared,
823823
obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj
824824
) )
825825
&& fresh(res.value.History)
@@ -847,10 +847,10 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
847847
tmp26.search.Some? ==>
848848
var tmps27 := set t27 | t27 in tmp26.search.value.versions;
849849
forall tmp27 :: tmp27 in tmps27 ==>
850-
tmp27.keySource.multi? ==>
851-
tmp27.keySource.multi.cache.Some? ==>
852-
tmp27.keySource.multi.cache.value.Shared? ==>
853-
tmp27.keySource.multi.cache.value.Shared.ValidState()
850+
tmp27.keySource.single? ==>
851+
tmp27.keySource.single.cache.Some? ==>
852+
tmp27.keySource.single.cache.value.Shared? ==>
853+
tmp27.keySource.single.cache.value.Shared.ValidState()
854854

855855
// Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
856856
function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result<IDynamoDbEncryptionTransformsClient, Error> {

0 commit comments

Comments
 (0)