Skip to content

Commit fe14024

Browse files
RitvikKapilaRitvikKapila
committed
add tests
1 parent c675502 commit fe14024

File tree

8 files changed

+471
-74
lines changed

8 files changed

+471
-74
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ module SearchConfigToInfo {
171171
var cache;
172172
if cacheType.Shared? {
173173
cache := cacheType.Shared;
174-
reveal ValidSharedCache(config, keyStore);
174+
reveal ValidSharedCache(config);
175175

176176
// This axiom is important because it is not easy to prove
177177
// keyStore.Modifies !! cache.Modifies for a shared cache.

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ module SearchableEncryptionInfo {
183183
return Success(Keys(theMap));
184184
} else {
185185
match keyId {
186-
case DontUseKeyId => return Failure(E("KeyID must not be supplied with a MultiKeyStore"));
186+
case DontUseKeyId => return Failure(E("KeyID must be supplied with a MultiKeyStore"));
187187
case ShouldHaveKeyId => return Success(ShouldHaveKeys);
188188
case KeyId(id) => var now := Time.GetCurrent(); var theMap :- getKeysCache(stdNames, id, cacheTTL as MP.PositiveLong, partitionIdBytes, logicalKeyStoreNameBytes, now as MP.PositiveLong); return Success(Keys(theMap));
189189
}

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy‎

Lines changed: 219 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,225 @@ module TestBaseBeacon {
105105
expect goodAttrs["aws_dbe_b_std2"] == newAttrs["aws_dbe_b_std2"];
106106
}
107107

108+
method {:test} TestSharedCacheBeaconsSingleKeyStoreWithSamePartitionId()
109+
{
110+
var partitionId : string := "partitionId";
111+
var sharedCache : MPT.CacheType := GetSharedCache();
112+
var primitives :- expect Primitives.AtomicPrimitives();
113+
114+
// Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes
115+
// Dafny is working on a fix. Update this test when Dafny releases `4.9.2`.
116+
// Using `assume{:axiom} false;` for this test for now.
117+
// var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by {
118+
// assume {:axiom} C.ValidSharedCache(version.keySource);
119+
// }
120+
// var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
121+
// var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by {
122+
// assume{:axiom} false;
123+
// }
124+
assume{:axiom} false;
125+
126+
// This call is expected to fail because we are providing a Bad KeyStore which does NOT exist
127+
var badVersion := GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionId));
128+
var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives);
129+
var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc);
130+
var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId);
131+
expect badAttrs.Failure?;
132+
133+
// This is expected to pass because we pass a valid KeyStore
134+
var version := GetLotsaBeaconsSingleWithSharedCache(cache := sharedCache, partitionId := Some(partitionId));
135+
var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives);
136+
var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
137+
var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId);
138+
139+
// This is expected to pass now because the cache already has cached material for this Branch Key ID.
140+
// This is a hack to test that the correct material is cached.
141+
var badAttrsNowCached :- expect badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId);
142+
}
143+
144+
method {:test} TestSharedCacheBeaconsSingleKeyStoreWithDifferentPartitionId()
145+
{
146+
var sharedCache : MPT.CacheType := GetSharedCache();
147+
var primitives :- expect Primitives.AtomicPrimitives();
148+
149+
// Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes
150+
// Dafny is working on a fix. Update this test when Dafny releases `4.9.2`.
151+
// Using `assume{:axiom} false;` for this test for now.
152+
// var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by {
153+
// assume {:axiom} C.ValidSharedCache(version.keySource);
154+
// }
155+
// var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
156+
// var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by {
157+
// assume{:axiom} false;
158+
// }
159+
assume{:axiom} false;
160+
161+
// This call is expected to fail because we are providing a Bad KeyStore which does NOT exist
162+
var partitionIdBadVersion : string := "partitionIdBadVersion";
163+
var badVersion := GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionIdBadVersion));
164+
var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives);
165+
var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc);
166+
var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId);
167+
expect badAttrs.Failure?;
168+
169+
// This is expected to pass because we pass a valid KeyStore
170+
var partitionIdGoodVersion : string := "partitionIdGoodVersion";
171+
var version := GetLotsaBeaconsSingleWithSharedCache(cache := sharedCache, partitionId := Some(partitionIdGoodVersion));
172+
var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives);
173+
var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
174+
var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId);
175+
176+
// This is still expected to fail because the partitionId for the cached material is different.
177+
var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId);
178+
expect badAttrsNowCached.Failure?;
179+
}
180+
181+
method {:test} TestSharedCacheBeaconsSingleKeyStoreWithUnspecifiedPartitionId()
182+
{
183+
var sharedCache : MPT.CacheType := GetSharedCache();
184+
var primitives :- expect Primitives.AtomicPrimitives();
185+
186+
// Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes
187+
// Dafny is working on a fix. Update this test when Dafny releases `4.9.2`.
188+
// Using `assume{:axiom} false;` for this test for now.
189+
// var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by {
190+
// assume {:axiom} C.ValidSharedCache(version.keySource);
191+
// }
192+
// var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
193+
// var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by {
194+
// assume{:axiom} false;
195+
// }
196+
assume{:axiom} false;
197+
198+
// This call is expected to fail because we are providing a Bad KeyStore which does NOT exist
199+
var badVersion := GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := None);
200+
var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives);
201+
var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc);
202+
var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId);
203+
expect badAttrs.Failure?;
204+
205+
// This is expected to pass because we pass a valid KeyStore
206+
var version := GetLotsaBeaconsSingleWithSharedCache(cache := sharedCache, partitionId := None);
207+
var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives);
208+
var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
209+
var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId);
210+
211+
// This is still expected to fail because the partitionId for the cached material is different.
212+
// If the user does NOT specify the partitionId, it is set to a random UUID
213+
var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId);
214+
expect badAttrsNowCached.Failure?;
215+
}
216+
217+
method {:test} TestSharedCacheBeaconsMultiKeyStoreWithSamePartitionId()
218+
{
219+
var partitionId : string := "partitionId";
220+
var sharedCache : MPT.CacheType := GetSharedCache();
221+
var primitives :- expect Primitives.AtomicPrimitives();
222+
223+
// Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes
224+
// Dafny is working on a fix. Update this test when Dafny releases `4.9.2`.
225+
// Using `assume{:axiom} false;` for this test for now.
226+
// var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by {
227+
// assume {:axiom} C.ValidSharedCache(version.keySource);
228+
// }
229+
// var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
230+
// var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by {
231+
// assume{:axiom} false;
232+
// }
233+
assume{:axiom} false;
234+
235+
// This call is expected to fail because we are providing a Bad KeyStore which does NOT exist
236+
var badVersion := GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionId));
237+
var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives);
238+
var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc);
239+
var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
240+
expect badAttrs.Failure?;
241+
242+
// This is expected to pass because we pass a valid KeyStore
243+
var version := GetLotsaBeaconsMultiWithSharedCache(cache := sharedCache, partitionId := Some(partitionId));
244+
var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives);
245+
var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
246+
var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
247+
248+
// This is expected to pass now because the cache already has cached material for this Branch Key ID.
249+
// This is a hack to test that the correct material is cached.
250+
var badAttrsNowCached :- expect badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
251+
}
252+
253+
254+
method {:test} TestSharedCacheBeaconsMultiKeyStoreWithDifferentPartitionId()
255+
{
256+
var sharedCache : MPT.CacheType := GetSharedCache();
257+
var primitives :- expect Primitives.AtomicPrimitives();
258+
259+
// Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes
260+
// Dafny is working on a fix. Update this test when Dafny releases `4.9.2`.
261+
// Using `assume{:axiom} false;` for this test for now.
262+
// var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by {
263+
// assume {:axiom} C.ValidSharedCache(version.keySource);
264+
// }
265+
// var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
266+
// var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by {
267+
// assume{:axiom} false;
268+
// }
269+
assume{:axiom} false;
270+
271+
// This call is expected to fail because we are providing a Bad KeyStore which does NOT exist
272+
var partitionIdBadVersion : string := "partitionIdBadVersion";
273+
var badVersion := GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionIdBadVersion));
274+
var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives);
275+
var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc);
276+
var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
277+
expect badAttrs.Failure?;
278+
279+
// This is expected to pass because we pass a valid KeyStore
280+
var partitionIdGoodVersion : string := "partitionIdGoodVersion";
281+
var version := GetLotsaBeaconsMultiWithSharedCache(cache := sharedCache, partitionId := Some(partitionIdGoodVersion));
282+
var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives);
283+
var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
284+
var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
285+
286+
// This is still expected to fail because the partitionId for the cached material is different.
287+
var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
288+
expect badAttrsNowCached.Failure?;
289+
}
290+
291+
method {:test} TestSharedCacheBeaconsMultiKeyStoreWithUnspecifiedPartitionId()
292+
{
293+
var sharedCache : MPT.CacheType := GetSharedCache();
294+
var primitives :- expect Primitives.AtomicPrimitives();
295+
296+
// Verification by adding assume statements in "by" passes, but there's an error while transpiling code to runtimes
297+
// Dafny is working on a fix. Update this test when Dafny releases `4.9.2`.
298+
// Using `assume{:axiom} false;` for this test for now.
299+
// var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives) by {
300+
// assume {:axiom} C.ValidSharedCache(version.keySource);
301+
// }
302+
// var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
303+
// var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId) by {
304+
// assume{:axiom} false;
305+
// }
306+
assume{:axiom} false;
307+
308+
// This call is expected to fail because we are providing a Bad KeyStore which does NOT exist
309+
var badVersion := GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := None);
310+
var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives);
311+
var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc);
312+
var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
313+
expect badAttrs.Failure?;
314+
315+
// This is expected to pass because we pass a valid KeyStore
316+
var version := GetLotsaBeaconsMultiWithSharedCache(cache := sharedCache, partitionId := None);
317+
var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives);
318+
var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
319+
var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
320+
321+
// This is still expected to fail because the partitionId for the cached material is different.
322+
// If the user does NOT specify the partitionId, it is set to a random UUID
323+
var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
324+
expect badAttrsNowCached.Failure?;
325+
}
326+
108327
method {:test} TestBeaconValues()
109328
{
110329
var version := GetLotsaBeacons();

0 commit comments

Comments
 (0)