Skip to content

Commit 43e38a2

Browse files
rishav-karanjitrishav-karanjit
committed
key path
1 parent 991a330 commit 43e38a2

File tree

1 file changed

+32
-74
lines changed

1 file changed

+32
-74
lines changed

‎TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy‎

Lines changed: 32 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
3232
import CreateInterceptedDDBClient
3333
import DynamoDbItemEncryptor
3434

35+
// TODO: Add extern for DEFAULT_KEYS
36+
const DEFAULT_KEYS : string := "../../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
3537

3638
predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000}
3739
type ConfigName = string
@@ -128,11 +130,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
128130
}
129131
}
130132

131-
method GetRoundTripTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
132-
returns (output : Result<seq<RoundTripTest>, string>)
133-
requires keys.ValidState()
134-
modifies keys.Modifies
135-
ensures keys.ValidState()
133+
method GetRoundTripTests(data : JSON) returns (output : Result<seq<RoundTripTest>, string>)
136134
{
137135
:- Need(data.Object?, "RoundTripTest Test must be an object.");
138136
var configs : map<string, TableConfig> := map[];
@@ -141,34 +139,26 @@ module {:options "-functionSyntax:4"} JsonConfig {
141139
for i := 0 to |data.obj| {
142140
var obj := data.obj[i];
143141
match obj.0 {
144-
case "Configs" => var src :- GetTableConfigs(obj.1, keys); configs := src;
142+
case "Configs" => var src :- GetTableConfigs(obj.1); configs := src;
145143
case "Records" => var src :- GetRecords(obj.1); records := src;
146144
case _ => return Failure("Unexpected part of a write test : '" + obj.0 + "'");
147145
}
148146
}
149147
return Success([RoundTripTest(configs, records)]);
150148
}
151149

152-
method GetWriteTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
153-
returns (output : Result<seq<WriteTest> , string>)
154-
requires keys.ValidState()
155-
modifies keys.Modifies
156-
ensures keys.ValidState()
150+
method GetWriteTests(data : JSON) returns (output : Result<seq<WriteTest> , string>)
157151
{
158152
:- Need(data.Array?, "Write Test list must be an array.");
159153
var results : seq<WriteTest> := [];
160154
for i := 0 to |data.arr| {
161155
var obj := data.arr[i];
162-
var item :- GetOneWriteTest(obj, keys);
156+
var item :- GetOneWriteTest(obj);
163157
results := results + [item];
164158
}
165159
return Success(results);
166160
}
167-
method GetOneWriteTest(data : JSON, keys: KeyVectors.KeyVectorsClient)
168-
returns (output : Result<WriteTest, string>)
169-
requires keys.ValidState()
170-
modifies keys.Modifies
171-
ensures keys.ValidState()
161+
method GetOneWriteTest(data : JSON) returns (output : Result<WriteTest, string>)
172162
{
173163
:- Need(data.Object?, "A Write Test must be an object.");
174164
var config : Option<TableConfig> := None;
@@ -178,7 +168,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
178168
for i := 0 to |data.obj| {
179169
var obj := data.obj[i];
180170
match obj.0 {
181-
case "Config" => var src :- GetOneTableConfig("foo", obj.1, keys); config := Some(src);
171+
case "Config" => var src :- GetOneTableConfig("foo", obj.1); config := Some(src);
182172
case "FileName" =>
183173
:- Need(obj.1.String?, "Write Test file name must be a string.");
184174
fileName := obj.1.str;
@@ -191,26 +181,18 @@ module {:options "-functionSyntax:4"} JsonConfig {
191181
return Success(WriteTest(config.value, records, fileName));
192182
}
193183

194-
method GetDecryptTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
195-
returns (output : Result<seq<DecryptTest> , string>)
196-
requires keys.ValidState()
197-
modifies keys.Modifies
198-
ensures keys.ValidState()
184+
method GetDecryptTests(data : JSON) returns (output : Result<seq<DecryptTest> , string>)
199185
{
200186
:- Need(data.Array?, "Decrypt Test list must be an array.");
201187
var results : seq<DecryptTest> := [];
202188
for i := 0 to |data.arr| {
203189
var obj := data.arr[i];
204-
var item :- GetOneDecryptTest(obj, keys);
190+
var item :- GetOneDecryptTest(obj);
205191
results := results + [item];
206192
}
207193
return Success(results);
208194
}
209-
method GetOneDecryptTest(data : JSON, keys: KeyVectors.KeyVectorsClient)
210-
returns (output : Result<DecryptTest, string>)
211-
requires keys.ValidState()
212-
modifies keys.Modifies
213-
ensures keys.ValidState()
195+
method GetOneDecryptTest(data : JSON) returns (output : Result<DecryptTest, string>)
214196
{
215197
:- Need(data.Object?, "A Decrypt Test must be an object.");
216198
var config : Option<TableConfig> := None;
@@ -220,7 +202,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
220202
for i := 0 to |data.obj| {
221203
var obj := data.obj[i];
222204
match obj.0 {
223-
case "Config" => var src :- GetOneTableConfig("foo", obj.1, keys); config := Some(src);
205+
case "Config" => var src :- GetOneTableConfig("foo", obj.1); config := Some(src);
224206
case "EncryptedRecords" => encRecords :- GetRecords(obj.1);
225207
case "PlainTextRecords" => plainRecords :- GetRecords(obj.1);
226208
case _ => return Failure("Unexpected part of a encrypt test : '" + obj.0 + "'");
@@ -232,27 +214,20 @@ module {:options "-functionSyntax:4"} JsonConfig {
232214
return Success(DecryptTest(config.value, encRecords, plainRecords));
233215
}
234216

235-
method GetTableConfigs(data : JSON, keys: KeyVectors.KeyVectorsClient)
236-
returns (output : Result<map<string, TableConfig> , string>)
237-
requires keys.ValidState()
238-
modifies keys.Modifies
239-
ensures keys.ValidState()
217+
method GetTableConfigs(data : JSON) returns (output : Result<map<string, TableConfig> , string>)
240218
{
241219
:- Need(data.Object?, "Search Config list must be an object.");
242220
var results : map<string, TableConfig> := map[];
243221
for i := 0 to |data.obj| {
244222
var obj := data.obj[i];
245-
var item :- GetOneTableConfig(obj.0, obj.1, keys);
223+
var item :- GetOneTableConfig(obj.0, obj.1);
246224
results := results[obj.0 := item];
247225
}
248226
return Success(results);
249227
}
250228

251-
method GetItemEncryptor(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
229+
method GetItemEncryptor(name : string, data : JSON)
252230
returns (encryptor : Result<DynamoDbItemEncryptor.DynamoDbItemEncryptorClient, string>)
253-
requires keys.ValidState()
254-
modifies keys.Modifies
255-
ensures keys.ValidState()
256231
ensures encryptor.Success? ==>
257232
&& encryptor.value.ValidState()
258233
&& fresh(encryptor.value)
@@ -321,6 +296,11 @@ module {:options "-functionSyntax:4"} JsonConfig {
321296
}
322297
}
323298

299+
var keys :- expect KeyVectors.KeyVectors(
300+
KeyVectorsTypes.KeyVectorsConfig(
301+
keyManifestPath := DEFAULT_KEYS
302+
)
303+
);
324304
var keyDescription :-
325305
if |key| == 0 then
326306
Success(KeyVectorsTypes.Hierarchy(KeyVectorsTypes.HierarchyKeyring(
@@ -353,11 +333,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
353333
return Success(encr);
354334
}
355335

356-
method GetOneTableConfig(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
357-
returns (output : Result<TableConfig, string>)
358-
requires keys.ValidState()
359-
modifies keys.Modifies
360-
ensures keys.ValidState()
336+
method GetOneTableConfig(name : string, data : JSON) returns (output : Result<TableConfig, string>)
361337
{
362338
:- Need(data.Object?, "A Table Config must be an object.");
363339
var logicalTableName := TableName;
@@ -424,6 +400,11 @@ module {:options "-functionSyntax:4"} JsonConfig {
424400
}
425401
}
426402

403+
var keys :- expect KeyVectors.KeyVectors(
404+
KeyVectorsTypes.KeyVectorsConfig(
405+
keyManifestPath := DEFAULT_KEYS
406+
)
407+
);
427408
var keyDescription :-
428409
if |key| == 0 then
429410
Success(KeyVectorsTypes.Hierarchy(KeyVectorsTypes.HierarchyKeyring(
@@ -543,22 +524,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
543524
var cache :- expect mpl.CreateCryptographicMaterialsCache(input);
544525

545526
var client :- expect Primitives.AtomicPrimitives();
546-
547-
// Create a test partitionIdBytes
548-
var partitionIdBytes : seq<uint8> :- expect SI.GenerateUuidBytes();
549-
550-
// Create a random logicalKeyStoreNameBytes
551-
// Ideally, this should be taken from the KeyStore store,
552-
// but logicalKeyStoreName variable doesn't exist in the
553-
// trait AwsCryptographyKeyStoreTypes.IKeyStoreClient
554-
// Therefore, the only way to get logicalKeyStoreName is
555-
// to call GetKeyStoreInfo, which we don't need to do here
556-
// since this method does NOT test the shared cache
557-
// which is the only place logicalKeyStoreName is used
558-
// (in the cache identifier)
559-
var logicalKeyStoreNameBytes : seq<uint8> :- expect SI.GenerateUuidBytes();
560-
561-
var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32, partitionIdBytes, logicalKeyStoreNameBytes);
527+
var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32);
562528

563529
var bv :- expect SI.MakeBeaconVersion(1, src, map[], map[], map[]);
564530
return Success(bv);
@@ -1148,27 +1114,19 @@ module {:options "-functionSyntax:4"} JsonConfig {
11481114
));
11491115
}
11501116

1151-
method GetIoTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
1152-
returns (output : Result<seq<IoTest> , string>)
1153-
requires keys.ValidState()
1154-
modifies keys.Modifies
1155-
ensures keys.ValidState()
1117+
method GetIoTests(data : JSON) returns (output : Result<seq<IoTest> , string>)
11561118
{
11571119
:- Need(data.Object?, "IoTests must be an object.");
11581120
var results : seq<IoTest> := [];
11591121
for i := 0 to |data.obj| {
11601122
var obj := data.obj[i];
1161-
var item :- GetOneIoTest(obj.0, obj.1, keys);
1123+
var item :- GetOneIoTest(obj.0, obj.1);
11621124
results := results + [item];
11631125
}
11641126
return Success(results);
11651127
}
11661128

1167-
method GetOneIoTest(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
1168-
returns (output : Result<IoTest, string>)
1169-
requires keys.ValidState()
1170-
modifies keys.Modifies
1171-
ensures keys.ValidState()
1129+
method GetOneIoTest(name : string, data : JSON) returns (output : Result<IoTest, string>)
11721130
{
11731131
:- Need(data.Object?, "IoTest must be an object.");
11741132
var readConfig : Option<TableConfig> := None;
@@ -1180,8 +1138,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
11801138
for i := 0 to |data.obj| {
11811139
var obj := data.obj[i];
11821140
match obj.0 {
1183-
case "WriteConfig" => var config :- GetOneTableConfig(obj.0, obj.1, keys); writeConfig := Some(config);
1184-
case "ReadConfig" => var config :- GetOneTableConfig(obj.0, obj.1, keys); readConfig := Some(config);
1141+
case "WriteConfig" => var config :- GetOneTableConfig(obj.0, obj.1); writeConfig := Some(config);
1142+
case "ReadConfig" => var config :- GetOneTableConfig(obj.0, obj.1); readConfig := Some(config);
11851143
case "Records" => records :- GetRecords(obj.1);
11861144
case "Values" => values :- GetValueMap(data.obj[i].1);
11871145
case "Queries" => queries :- GetSimpleQueries(data.obj[i].1);

0 commit comments

Comments
 (0)