Skip to content

Commit 92e3fa3

Browse files
rishav-karanjitrishav-karanjit
committed
Revert "key path"
This reverts commit 43e38a2.
1 parent 10ba751 commit 92e3fa3

File tree

1 file changed

+74
-32
lines changed

1 file changed

+74
-32
lines changed

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

Lines changed: 74 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,6 @@ 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"
3735

3836
predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000}
3937
type ConfigName = string
@@ -130,7 +128,11 @@ module {:options "-functionSyntax:4"} JsonConfig {
130128
}
131129
}
132130

133-
method GetRoundTripTests(data : JSON) returns (output : Result<seq<RoundTripTest>, string>)
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()
134136
{
135137
:- Need(data.Object?, "RoundTripTest Test must be an object.");
136138
var configs : map<string, TableConfig> := map[];
@@ -139,26 +141,34 @@ module {:options "-functionSyntax:4"} JsonConfig {
139141
for i := 0 to |data.obj| {
140142
var obj := data.obj[i];
141143
match obj.0 {
142-
case "Configs" => var src :- GetTableConfigs(obj.1); configs := src;
144+
case "Configs" => var src :- GetTableConfigs(obj.1, keys); configs := src;
143145
case "Records" => var src :- GetRecords(obj.1); records := src;
144146
case _ => return Failure("Unexpected part of a write test : '" + obj.0 + "'");
145147
}
146148
}
147149
return Success([RoundTripTest(configs, records)]);
148150
}
149151

150-
method GetWriteTests(data : JSON) returns (output : Result<seq<WriteTest> , string>)
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()
151157
{
152158
:- Need(data.Array?, "Write Test list must be an array.");
153159
var results : seq<WriteTest> := [];
154160
for i := 0 to |data.arr| {
155161
var obj := data.arr[i];
156-
var item :- GetOneWriteTest(obj);
162+
var item :- GetOneWriteTest(obj, keys);
157163
results := results + [item];
158164
}
159165
return Success(results);
160166
}
161-
method GetOneWriteTest(data : JSON) returns (output : Result<WriteTest, string>)
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()
162172
{
163173
:- Need(data.Object?, "A Write Test must be an object.");
164174
var config : Option<TableConfig> := None;
@@ -168,7 +178,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
168178
for i := 0 to |data.obj| {
169179
var obj := data.obj[i];
170180
match obj.0 {
171-
case "Config" => var src :- GetOneTableConfig("foo", obj.1); config := Some(src);
181+
case "Config" => var src :- GetOneTableConfig("foo", obj.1, keys); config := Some(src);
172182
case "FileName" =>
173183
:- Need(obj.1.String?, "Write Test file name must be a string.");
174184
fileName := obj.1.str;
@@ -181,18 +191,26 @@ module {:options "-functionSyntax:4"} JsonConfig {
181191
return Success(WriteTest(config.value, records, fileName));
182192
}
183193

184-
method GetDecryptTests(data : JSON) returns (output : Result<seq<DecryptTest> , string>)
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()
185199
{
186200
:- Need(data.Array?, "Decrypt Test list must be an array.");
187201
var results : seq<DecryptTest> := [];
188202
for i := 0 to |data.arr| {
189203
var obj := data.arr[i];
190-
var item :- GetOneDecryptTest(obj);
204+
var item :- GetOneDecryptTest(obj, keys);
191205
results := results + [item];
192206
}
193207
return Success(results);
194208
}
195-
method GetOneDecryptTest(data : JSON) returns (output : Result<DecryptTest, string>)
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()
196214
{
197215
:- Need(data.Object?, "A Decrypt Test must be an object.");
198216
var config : Option<TableConfig> := None;
@@ -202,7 +220,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
202220
for i := 0 to |data.obj| {
203221
var obj := data.obj[i];
204222
match obj.0 {
205-
case "Config" => var src :- GetOneTableConfig("foo", obj.1); config := Some(src);
223+
case "Config" => var src :- GetOneTableConfig("foo", obj.1, keys); config := Some(src);
206224
case "EncryptedRecords" => encRecords :- GetRecords(obj.1);
207225
case "PlainTextRecords" => plainRecords :- GetRecords(obj.1);
208226
case _ => return Failure("Unexpected part of a encrypt test : '" + obj.0 + "'");
@@ -214,20 +232,27 @@ module {:options "-functionSyntax:4"} JsonConfig {
214232
return Success(DecryptTest(config.value, encRecords, plainRecords));
215233
}
216234

217-
method GetTableConfigs(data : JSON) returns (output : Result<map<string, TableConfig> , string>)
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()
218240
{
219241
:- Need(data.Object?, "Search Config list must be an object.");
220242
var results : map<string, TableConfig> := map[];
221243
for i := 0 to |data.obj| {
222244
var obj := data.obj[i];
223-
var item :- GetOneTableConfig(obj.0, obj.1);
245+
var item :- GetOneTableConfig(obj.0, obj.1, keys);
224246
results := results[obj.0 := item];
225247
}
226248
return Success(results);
227249
}
228250

229-
method GetItemEncryptor(name : string, data : JSON)
251+
method GetItemEncryptor(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
230252
returns (encryptor : Result<DynamoDbItemEncryptor.DynamoDbItemEncryptorClient, string>)
253+
requires keys.ValidState()
254+
modifies keys.Modifies
255+
ensures keys.ValidState()
231256
ensures encryptor.Success? ==>
232257
&& encryptor.value.ValidState()
233258
&& fresh(encryptor.value)
@@ -296,11 +321,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
296321
}
297322
}
298323

299-
var keys :- expect KeyVectors.KeyVectors(
300-
KeyVectorsTypes.KeyVectorsConfig(
301-
keyManifestPath := DEFAULT_KEYS
302-
)
303-
);
304324
var keyDescription :-
305325
if |key| == 0 then
306326
Success(KeyVectorsTypes.Hierarchy(KeyVectorsTypes.HierarchyKeyring(
@@ -333,7 +353,11 @@ module {:options "-functionSyntax:4"} JsonConfig {
333353
return Success(encr);
334354
}
335355

336-
method GetOneTableConfig(name : string, data : JSON) returns (output : Result<TableConfig, string>)
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()
337361
{
338362
:- Need(data.Object?, "A Table Config must be an object.");
339363
var logicalTableName := TableName;
@@ -400,11 +424,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
400424
}
401425
}
402426

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

526545
var client :- expect Primitives.AtomicPrimitives();
527-
var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32);
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);
528562

529563
var bv :- expect SI.MakeBeaconVersion(1, src, map[], map[], map[]);
530564
return Success(bv);
@@ -1114,19 +1148,27 @@ module {:options "-functionSyntax:4"} JsonConfig {
11141148
));
11151149
}
11161150

1117-
method GetIoTests(data : JSON) returns (output : Result<seq<IoTest> , string>)
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()
11181156
{
11191157
:- Need(data.Object?, "IoTests must be an object.");
11201158
var results : seq<IoTest> := [];
11211159
for i := 0 to |data.obj| {
11221160
var obj := data.obj[i];
1123-
var item :- GetOneIoTest(obj.0, obj.1);
1161+
var item :- GetOneIoTest(obj.0, obj.1, keys);
11241162
results := results + [item];
11251163
}
11261164
return Success(results);
11271165
}
11281166

1129-
method GetOneIoTest(name : string, data : JSON) returns (output : Result<IoTest, string>)
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()
11301172
{
11311173
:- Need(data.Object?, "IoTest must be an object.");
11321174
var readConfig : Option<TableConfig> := None;
@@ -1138,8 +1180,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
11381180
for i := 0 to |data.obj| {
11391181
var obj := data.obj[i];
11401182
match obj.0 {
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);
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);
11431185
case "Records" => records :- GetRecords(obj.1);
11441186
case "Values" => values :- GetValueMap(data.obj[i].1);
11451187
case "Queries" => queries :- GetSimpleQueries(data.obj[i].1);

0 commit comments

Comments
 (0)