Skip to content

Commit 155a74c

Browse files
RitvikKapilaRitvikKapila
committed
address comments
1 parent ed67691 commit 155a74c

File tree

5 files changed

+92
-55
lines changed

5 files changed

+92
-55
lines changed

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -719,7 +719,7 @@ structure SingleKeyStore {
719719
@required
720720
@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.")
721721
cacheTTL: Integer,
722-
@documentation("Provide the Shared Cache for Searchable Encryption.")
722+
@documentation("Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore.")
723723
cache : CacheType,
724724
@documentation("Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.")
725725
partitionId: String

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

+15-9
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ module SearchConfigToInfo {
4040
requires ValidSearchConfig(outer.search)
4141
requires outer.search.Some? ==> ValidSharedCache(outer.search.value.versions[0].keySource)
4242
modifies if outer.search.Some? then outer.search.value.versions[0].keyStore.Modifies else {}
43+
ensures outer.search.Some? ==> ValidSharedCache(outer.search.value.versions[0].keySource)
4344
ensures output.Success? && output.value.Some? ==>
4445
&& output.value.value.ValidState()
4546
&& fresh(output.value.value.versions[0].keySource.client)
@@ -120,6 +121,7 @@ module SearchConfigToInfo {
120121
modifies keyStore.Modifies
121122
requires client.ValidState()
122123
requires ValidSharedCache(config)
124+
ensures ValidSharedCache(config)
123125
ensures client.ValidState()
124126
ensures output.Success? ==>
125127
&& output.value.ValidState()
@@ -148,9 +150,10 @@ module SearchConfigToInfo {
148150
//= specification/searchable-encryption/search-config.md#key-store-cache
149151
//# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
150152
//# MUST be created.
151-
//# For a [Single Key Store](#single-key-store-initialization), either the customer provides a cache, or we create a cache that MUST have [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity)
152-
//# equal to 1.
153-
//# For a [Multi Key Store](#multi-key-store-initialization), either the customer provides a cache, or we create a cache that MUST have [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity)
153+
//# For a [Single Key Store](#single-key-store-initialization), either the user provides a cache, or we create a cache that MUST have [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity)
154+
//# equal to 1. If the user provides a cache which is not `Shared`, they SHOULD set the [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity)
155+
//# of the provided `CacheType` to 1, because the [Single Key Store](#single-key-store-initialization) only ever caches one entry. Even if the user provides an entryCapacity > 1, the [Single Key Store](#single-key-store-initialization) will only cache one entry.
156+
//# For a [Multi Key Store](#multi-key-store-initialization), either the user provides a cache, or we create a cache that MUST have [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity)
154157
//# equal to 1000.
155158
var cacheType : MPT.CacheType :=
156159
if config.multi? then
@@ -160,8 +163,9 @@ module SearchConfigToInfo {
160163
MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1000))
161164
else
162165
if config.single.cache.Some? then
163-
// Ideally, we only want to pass a cache here with entryCapacity = 1
164-
// because the SingleKeyStore caches only one value.
166+
// If the user provides a CacheType, and it is NOT Shared,
167+
// we SHOULD only allow an entryCapacity = 1
168+
// because the SingleKeyStore only ever caches one value.
165169
// That is, we SHOULD add a check here for entryCapacity = 1.
166170
// However, that requires us to write an if block for each CacheType.
167171
// Also, it does NOT matter what the entryCapacity is, because the cache
@@ -174,10 +178,6 @@ module SearchConfigToInfo {
174178
if cacheType.Shared? {
175179
cache := cacheType.Shared;
176180
reveal ValidSharedCache(config);
177-
178-
// This axiom is important because it is not easy to prove
179-
// keyStore.Modifies !! cache.Modifies for a shared cache.
180-
assume {:axiom} keyStore.Modifies !! cache.Modifies;
181181
} else {
182182
//= specification/searchable-encryption/search-config.md#key-store-cache
183183
//# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
@@ -228,6 +228,11 @@ module SearchConfigToInfo {
228228
:- Need(0 < config.single.cacheTTL, E("Beacon Cache TTL must be at least 1."));
229229
output := Success(I.KeySource(client, keyStore, I.SingleLoc(config.single.keyId), cache, config.single.cacheTTL as uint32, partitionIdBytes, logicalKeyStoreNameBytes));
230230
}
231+
assert output.value.ValidState() by {
232+
// This axiom is important because it is not easy to prove
233+
// keyStore.Modifies !! cache.Modifies for a shared cache.
234+
assume {:axiom} keyStore.Modifies !! cache.Modifies;
235+
}
231236
}
232237

233238
// convert configured BeaconVersion to internal BeaconVersion
@@ -236,6 +241,7 @@ module SearchConfigToInfo {
236241
requires ValidBeaconVersion(config)
237242
requires ValidSharedCache(config.keySource)
238243
modifies config.keyStore.Modifies
244+
ensures ValidSharedCache(config.keySource)
239245
ensures output.Success? ==>
240246
&& output.value.ValidState()
241247
&& fresh(output.value.keySource.client)

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

+59-35
Original file line numberDiff line numberDiff line change
@@ -138,10 +138,8 @@ module SearchableEncryptionInfo {
138138
var uuid :- uuid?
139139
.MapFailure(e => Error.DynamoDbEncryptionException(message := e));
140140

141-
var uuidBytes: seq<uint8> :- UUID.ToByteArray(uuid)
142-
.MapFailure(e => Error.DynamoDbEncryptionException(message := e));
143-
144-
output := Success(uuidBytes);
141+
output := UUID.ToByteArray(uuid)
142+
.MapFailure(e => Error.DynamoDbEncryptionException(message := e));
145143
}
146144

147145
datatype KeyLocation =
@@ -176,7 +174,15 @@ module SearchableEncryptionInfo {
176174
if keyLoc.SingleLoc? {
177175
:- Need(keyId.DontUseKeyId?, E("KeyID should not be supplied with a SingleKeyStore"));
178176
var now := Time.GetCurrent();
179-
var theMap :- getKeysCache(client, stdNames, keyLoc.keyId, cacheTTL as MP.PositiveLong, partitionIdBytes, logicalKeyStoreNameBytes, now as MP.PositiveLong);
177+
var theMap :- getKeysCache(
178+
client,
179+
stdNames,
180+
keyLoc.keyId,
181+
cacheTTL as MP.PositiveLong,
182+
partitionIdBytes,
183+
logicalKeyStoreNameBytes,
184+
now as MP.PositiveLong
185+
);
180186
return Success(Keys(theMap));
181187
} else if keyLoc.LiteralLoc? {
182188
:- Need(keyId.DontUseKeyId?, E("KeyID should not be supplied with a LiteralKeyStore"));
@@ -186,7 +192,18 @@ module SearchableEncryptionInfo {
186192
match keyId {
187193
case DontUseKeyId => return Failure(E("KeyID must be supplied with a MultiKeyStore"));
188194
case ShouldHaveKeyId => return Success(ShouldHaveKeys);
189-
case KeyId(id) => var now := Time.GetCurrent(); var theMap :- getKeysCache(client, stdNames, id, cacheTTL as MP.PositiveLong, partitionIdBytes, logicalKeyStoreNameBytes, now as MP.PositiveLong); return Success(Keys(theMap));
195+
case KeyId(id) =>
196+
var now := Time.GetCurrent();
197+
var theMap :- getKeysCache(
198+
client,
199+
stdNames,
200+
id,
201+
cacheTTL as MP.PositiveLong,
202+
partitionIdBytes,
203+
logicalKeyStoreNameBytes,
204+
now as MP.PositiveLong
205+
);
206+
return Success(Keys(theMap));
190207
}
191208
}
192209
}
@@ -227,37 +244,40 @@ module SearchableEncryptionInfo {
227244
returns (output : Result<HmacKeyMap, Error>)
228245
requires Seq.HasNoDuplicates(stdNames)
229246
requires ValidState()
247+
requires client.ValidState()
230248
modifies Modifies()
249+
modifies client.Modifies
231250
ensures ValidState()
251+
ensures client.ValidState()
232252

233253
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
234254
//= type=implication
235255
//# Get beacon key MUST Call the associated [Key Store Cache](#key-store-cache)
236256
//# [Get Cache Entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#get-cache-entry)
237-
//# with the `beacon key id`.
257+
//# with the cache identifier defined in the [Searchable Encryption Cache Identifier](#searchable-encryption-cache-identifier) section.
238258
ensures output.Success? ==>
239-
&& var oldHistory := old(cache.History.GetCacheEntry);
240-
&& var newHistory := cache.History.GetCacheEntry;
241-
&& |newHistory| == |oldHistory|+1
242-
&& var cacheInput := Seq.Last(newHistory).input;
243-
&& var cacheOutput := Seq.Last(newHistory).output;
259+
&& var oldGetCacheHistory := old(cache.History.GetCacheEntry);
260+
&& var newGetCacheHistory := cache.History.GetCacheEntry;
261+
&& |newGetCacheHistory| == |oldGetCacheHistory|+1
262+
&& var getCacheInput := Seq.Last(newGetCacheHistory).input;
263+
&& var getCacheOutput := Seq.Last(newGetCacheHistory).output;
244264
&& UTF8.Encode(keyId).Success?
245265

246266
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
247267
//= type=implication
248268
//# If a [cache entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#cache-entry)
249269
//# exists, get beacon key MUST return the [entry materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#materials).
250-
&& (cacheOutput.Success? && cacheEntryWithinLimits(
251-
creationTime := cacheOutput.value.creationTime,
270+
&& (getCacheOutput.Success? && cacheEntryWithinLimits(
271+
creationTime := getCacheOutput.value.creationTime,
252272
now := now,
253273
ttlSeconds := cacheTTL
254274
) ==>
255-
&& cacheOutput.value.materials.BeaconKey?
256-
&& cacheOutput.value.materials.BeaconKey.hmacKeys.Some?
257-
&& output.value == cacheOutput.value.materials.BeaconKey.hmacKeys.value)
275+
&& getCacheOutput.value.materials.BeaconKey?
276+
&& getCacheOutput.value.materials.BeaconKey.hmacKeys.Some?
277+
&& output.value == getCacheOutput.value.materials.BeaconKey.hmacKeys.value)
258278

259-
&& (cacheOutput.Failure? || !cacheEntryWithinLimits(
260-
creationTime := cacheOutput.value.creationTime,
279+
&& (getCacheOutput.Failure? || !cacheEntryWithinLimits(
280+
creationTime := getCacheOutput.value.creationTime,
261281
now := now,
262282
ttlSeconds := cacheTTL
263283
) ==>
@@ -274,20 +294,30 @@ module SearchableEncryptionInfo {
274294
//= type=implication
275295
//# The `beacon key id` MUST be passed to the configured `KeyStore`'s `GetBeaconKey` operation.
276296
&& storeInput.branchKeyIdentifier == keyId
277-
&& var oldPutHistory := old(cache.History.PutCacheEntry);
278-
&& var newPutHistory := cache.History.PutCacheEntry;
279-
&& |newPutHistory| == |oldPutHistory|+1
297+
&& var oldPutCacheHistory := old(cache.History.PutCacheEntry);
298+
&& var newPutCacheHistory := cache.History.PutCacheEntry;
299+
&& |newPutCacheHistory| == |oldPutCacheHistory|+1
280300
&& (
281-
var storeOutput := Seq.Last(newPutHistory).output;
282-
|| storeOutput.Success?
283-
|| storeOutput.error.EntryAlreadyExists?
301+
var putCacheOutput := Seq.Last(newPutCacheHistory).output;
302+
|| putCacheOutput.Success?
303+
|| putCacheOutput.error.EntryAlreadyExists?
284304
)
285-
&& var storeInput := Seq.Last(newPutHistory).input;
286-
&& var storeOutput := Seq.Last(newPutHistory).output;
305+
&& var putCacheInput := Seq.Last(newPutCacheHistory).input;
306+
&& var putCacheOutput := Seq.Last(newPutCacheHistory).output;
307+
308+
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
309+
//# The Searchable Encryption cache identifier for [Key Store Cache](#key-store-cache)
310+
//# [Get Cache Entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#get-cache-entry)
311+
//# and the [Key Store Cache](#key-store-cache)
312+
//# [Put Cache Entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#put-cache-entry)
313+
//# MUST be the same.
314+
&& putCacheInput.identifier == getCacheInput.identifier
315+
287316
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
288317
//= type=implication
289318
//# These cached materials MUST be returned.
290-
&& storeInput.materials.BeaconKey? ==> storeInput.materials.BeaconKey.hmacKeys == Some(output.value)
319+
&& putCacheInput.materials.BeaconKey?
320+
&& putCacheInput.materials.BeaconKey.hmacKeys == Some(output.value)
291321
)
292322
{
293323

@@ -311,15 +341,9 @@ module SearchableEncryptionInfo {
311341
var identifierDigestInput := Prim.DigestInput(
312342
digestAlgorithm := hashAlgorithm, message := identifier
313343
);
314-
var maybeCacheDigest := Digest.Digest(identifierDigestInput);
344+
var maybeCacheDigest := client.Digest(identifierDigestInput);
315345
var cacheDigest :- maybeCacheDigest.MapFailure(e => AwsCryptographyPrimitives(e));
316346

317-
:- Need(
318-
|cacheDigest| == Digest.Length(hashAlgorithm),
319-
Error.DynamoDbEncryptionException(
320-
message := "Digest generated a message not equal to the expected length.")
321-
);
322-
323347
// Use the SHA384 of the identifier as the cache identifier
324348
var getCacheInput := MP.GetCacheEntryInput(identifier := cacheDigest, bytesUsed := None);
325349
verifyValidStateCache(cache);

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/SingleKeyStore.java

+4-4
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ public class SingleKeyStore {
2222
private final Integer cacheTTL;
2323

2424
/**
25-
* Provide the Shared Cache for Searchable Encryption.
25+
* Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore.
2626
*/
2727
private final CacheType cache;
2828

@@ -53,7 +53,7 @@ public Integer cacheTTL() {
5353
}
5454

5555
/**
56-
* @return Provide the Shared Cache for Searchable Encryption.
56+
* @return Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore.
5757
*/
5858
public CacheType cache() {
5959
return this.cache;
@@ -96,12 +96,12 @@ public interface Builder {
9696
Integer cacheTTL();
9797

9898
/**
99-
* @param cache Provide the Shared Cache for Searchable Encryption.
99+
* @param cache Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore.
100100
*/
101101
Builder cache(CacheType cache);
102102

103103
/**
104-
* @return Provide the Shared Cache for Searchable Encryption.
104+
* @return Which type of local cache to use. Please see the [spec](https://github.com/aws/aws-database-encryption-sdk-dynamodb/blob/main/specification/searchable-encryption/search-config.md#key-store-cache) on how to provide a cache for a SingleKeyStore.
105105
*/
106106
CacheType cache();
107107

0 commit comments

Comments
 (0)