Skip to content

Commit dabcaf1

Browse files
lucasmcdonald3lucasmcdonald3
authored
chore(TestVectors): Reuse single KeyVectors client across TestVectors (#1577)
1 parent 04a8eb2 commit dabcaf1

File tree

6 files changed

+167
-77
lines changed

6 files changed

+167
-77
lines changed

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

Lines changed: 26 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,17 @@ module {:options "-functionSyntax:4"} DecryptManifest {
2020
import opened JSONHelpers
2121
import JsonConfig
2222
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
23+
import KeyVectors
2324

24-
method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON) returns (output : Result<bool, string>)
25+
method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON, keys : KeyVectors.KeyVectorsClient)
26+
returns (output : Result<bool, string>)
27+
requires keys.ValidState()
28+
modifies keys.Modifies
29+
ensures keys.ValidState()
2530
{
2631
var enc :- JsonConfig.GetRecord(encrypted);
2732
var plain :- JsonConfig.GetRecord(plaintext);
28-
var encryptor :- JsonConfig.GetItemEncryptor(name, config);
33+
var encryptor :- JsonConfig.GetItemEncryptor(name, config, keys);
2934
var decrypted :- expect encryptor.DecryptItem(
3035
ENC.DecryptItemInput(
3136
encryptedItem:=enc.item
@@ -36,10 +41,14 @@ module {:options "-functionSyntax:4"} DecryptManifest {
3641
return Success(true);
3742
}
3843

39-
method OneNegativeTest(name : string, config : JSON, encrypted : JSON) returns (output : Result<bool, string>)
44+
method OneNegativeTest(name : string, config : JSON, encrypted : JSON, keys: KeyVectors.KeyVectorsClient)
45+
returns (output : Result<bool, string>)
46+
requires keys.ValidState()
47+
modifies keys.Modifies
48+
ensures keys.ValidState()
4049
{
4150
var enc :- JsonConfig.GetRecord(encrypted);
42-
var encryptor :- JsonConfig.GetItemEncryptor(name, config);
51+
var encryptor :- JsonConfig.GetItemEncryptor(name, config, keys);
4352
var decrypted := encryptor.DecryptItem(
4453
ENC.DecryptItemInput(
4554
encryptedItem:=enc.item
@@ -51,7 +60,11 @@ module {:options "-functionSyntax:4"} DecryptManifest {
5160
return Success(true);
5261
}
5362

54-
method OneTest(name : string, value : JSON) returns (output : Result<bool, string>)
63+
method OneTest(name : string, value : JSON, keys: KeyVectors.KeyVectorsClient)
64+
returns (output : Result<bool, string>)
65+
requires keys.ValidState()
66+
modifies keys.Modifies
67+
ensures keys.ValidState()
5568
{
5669
:- Need(value.Object?, "Test must be an object");
5770

@@ -89,15 +102,19 @@ module {:options "-functionSyntax:4"} DecryptManifest {
89102

90103
if types.value == "positive-decrypt" {
91104
:- Need(plaintext.Some?, "positive-decrypt Test requires a 'plaintext' member.");
92-
output := OnePositiveTest(name, config.value, encrypted.value, plaintext.value);
105+
output := OnePositiveTest(name, config.value, encrypted.value, plaintext.value, keys);
93106
} else if types.value == "negative-decrypt" {
94-
output := OneNegativeTest(name, config.value, encrypted.value);
107+
output := OneNegativeTest(name, config.value, encrypted.value, keys);
95108
} else {
96109
return Failure("Invalid encrypt type : '" + types.value + "'.");
97110
}
98111
}
99112

100-
method Decrypt(inFile : string) returns (output : Result<bool, string>)
113+
method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient)
114+
returns (output : Result<bool, string>)
115+
requires keyVectors.ValidState()
116+
modifies keyVectors.Modifies
117+
ensures keyVectors.ValidState()
101118
{
102119
var timeStamp :- expect Time.GetCurrentTimeStamp();
103120
print timeStamp + " Decrypt : ", inFile, "\n";
@@ -154,7 +171,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
154171
for i := 0 to |tests.value| {
155172
var obj := tests.value[i];
156173
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
157-
var _ :- OneTest(obj.0, obj.1);
174+
var _ :- OneTest(obj.0, obj.1, keyVectors);
158175
}
159176

160177
timeStamp :- expect Time.GetCurrentTimeStamp();

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

Lines changed: 27 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ module {:options "-functionSyntax:4"} EncryptManifest {
2121
import opened JSONHelpers
2222
import JsonConfig
2323
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
24+
import KeyVectors
2425

2526
function Manifest() : (string, JSON)
2627
{
@@ -42,10 +43,14 @@ module {:options "-functionSyntax:4"} EncryptManifest {
4243
("client", Object(result))
4344
}
4445

45-
method OnePositiveTest(name : string, theType : string, desc : string, config : JSON, decryptConfig : Option<JSON>, record : JSON) returns (output : Result<(string, JSON), string>)
46+
method OnePositiveTest(name : string, theType : string, desc : string, config : JSON, decryptConfig : Option<JSON>, record : JSON, keys: KeyVectors.KeyVectorsClient)
47+
returns (output : Result<(string, JSON), string>)
48+
requires keys.ValidState()
49+
modifies keys.Modifies
50+
ensures keys.ValidState()
4651
{
4752
var rec :- JsonConfig.GetRecord(record);
48-
var encryptor :- JsonConfig.GetItemEncryptor(name, config);
53+
var encryptor :- JsonConfig.GetItemEncryptor(name, config, keys);
4954
var encrypted :- expect encryptor.EncryptItem(
5055
ENC.EncryptItemInput(
5156
plaintextItem:=rec.item
@@ -64,10 +69,14 @@ module {:options "-functionSyntax:4"} EncryptManifest {
6469
return Success((name, Object(result)));
6570
}
6671

67-
method OneNegativeTest(name : string, config : JSON, record : JSON) returns (output : Result<bool, string>)
72+
method OneNegativeTest(name : string, config : JSON, record : JSON, keys: KeyVectors.KeyVectorsClient)
73+
returns (output : Result<bool, string>)
74+
requires keys.ValidState()
75+
modifies keys.Modifies
76+
ensures keys.ValidState()
6877
{
6978
var rec :- JsonConfig.GetRecord(record);
70-
var encryptor :- JsonConfig.GetItemEncryptor(name, config);
79+
var encryptor :- JsonConfig.GetItemEncryptor(name, config, keys);
7180
var encrypted := encryptor.EncryptItem(
7281
ENC.EncryptItemInput(
7382
plaintextItem:=rec.item
@@ -80,7 +89,11 @@ module {:options "-functionSyntax:4"} EncryptManifest {
8089
}
8190

8291

83-
method OneTest(name : string, value : JSON) returns (output : Result<Option<(string, JSON)>, string>)
92+
method OneTest(name : string, value : JSON, keys: KeyVectors.KeyVectorsClient)
93+
returns (output : Result<Option<(string, JSON)>, string>)
94+
requires keys.ValidState()
95+
modifies keys.Modifies
96+
ensures keys.ValidState()
8497
{
8598
:- Need(value.Object?, "Test must be an object");
8699

@@ -117,20 +130,24 @@ module {:options "-functionSyntax:4"} EncryptManifest {
117130
:- Need(record.Some?, "Test requires a 'record' member.");
118131

119132
if types.value == "positive-encrypt" {
120-
var x :- OnePositiveTest(name, "positive-decrypt", description.value, config.value, decryptConfig, record.value);
133+
var x :- OnePositiveTest(name, "positive-decrypt", description.value, config.value, decryptConfig, record.value, keys);
121134
return Success(Some(x));
122135
} else if types.value == "negative-decrypt" {
123-
var x :- OnePositiveTest(name, "negative-decrypt", description.value, config.value, decryptConfig, record.value);
136+
var x :- OnePositiveTest(name, "negative-decrypt", description.value, config.value, decryptConfig, record.value, keys);
124137
return Success(Some(x));
125138
} else if types.value == "negative-encrypt" {
126-
var _ := OneNegativeTest(name, config.value, record.value);
139+
var _ := OneNegativeTest(name, config.value, record.value, keys);
127140
return Success(None);
128141
} else {
129142
return Failure("Invalid encrypt type : '" + types.value + "'.");
130143
}
131144
}
132145

133-
method Encrypt(inFile : string, outFile : string, lang : string, version : string) returns (output : Result<bool, string>)
146+
method Encrypt(inFile : string, outFile : string, lang : string, version : string, keyVectors: KeyVectors.KeyVectorsClient)
147+
returns (output : Result<bool, string>)
148+
requires keyVectors.ValidState()
149+
modifies keyVectors.Modifies
150+
ensures keyVectors.ValidState()
134151
{
135152
var timeStamp :- expect Time.GetCurrentTimeStamp();
136153
print timeStamp + " Encrypt : ", inFile, "\n";
@@ -187,7 +204,7 @@ module {:options "-functionSyntax:4"} EncryptManifest {
187204
for i := 0 to |tests.value| {
188205
var obj := tests.value[i];
189206
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
190-
var newTest :- OneTest(obj.0, obj.1);
207+
var newTest :- OneTest(obj.0, obj.1, keyVectors);
191208
if newTest.Some? {
192209
test := test + [newTest.value];
193210
}

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

Lines changed: 33 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,17 @@ module WrappedDDBEncryptionMain {
1414
import FileIO
1515
import JSON.API
1616
import opened JSONHelpers
17+
import KeyVectors
18+
import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
1719

18-
method AddJson(prev : TestVectorConfig, file : string) returns (output : Result<TestVectorConfig, string>)
20+
21+
const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
22+
23+
method AddJson(prev : TestVectorConfig, file : string, keyVectors: KeyVectors.KeyVectorsClient)
24+
returns (output : Result<TestVectorConfig, string>)
25+
requires keyVectors.ValidState()
26+
modifies keyVectors.Modifies
27+
ensures keyVectors.ValidState()
1928
{
2029
var configBv := FileIO.ReadBytesFromFile(file);
2130
if configBv.Failure? {
@@ -24,20 +33,35 @@ module WrappedDDBEncryptionMain {
2433
}
2534
var configBytes := BvToBytes(configBv.value);
2635
var json :- expect API.Deserialize(configBytes);
27-
output := ParseTestVector(json, prev);
36+
output := ParseTestVector(json, prev, keyVectors);
2837
if output.Failure? {
2938
print output.error, "\n";
3039
}
3140
}
3241

33-
method ASDF() {
42+
method ASDF()
43+
{
44+
// KeyVectors client passed to every test.
45+
// All test vectors currently use the same keys manifest, located at DEFAULT_KEYS.
46+
// All test vectors can share this same KeyVectors client.
47+
48+
// To use a different keys manifest, create a new KeyVectors client.
49+
// If you need to create a new KeyVectors client, create it as infrequently as possible.
50+
// Creating this client frequently means JSON is parsed frequently.
51+
// Parsing JSON is very slow in Python. Parse JSON as infrequently as possible.
52+
var keyVectors :- expect KeyVectors.KeyVectors(
53+
KeyVectorsTypes.KeyVectorsConfig(
54+
keyManifestPath := DEFAULT_KEYS
55+
)
56+
);
57+
3458
WriteSetPermutations.WriteSetPermutations();
3559
var config := MakeEmptyTestVector();
36-
config :- expect AddJson(config, "records.json");
37-
config :- expect AddJson(config, "configs.json");
38-
config :- expect AddJson(config, "data.json");
39-
config :- expect AddJson(config, "iotest.json");
40-
config :- expect AddJson(config, "PermTest.json");
41-
config.RunAllTests();
60+
config :- expect AddJson(config, "records.json", keyVectors);
61+
config :- expect AddJson(config, "configs.json", keyVectors);
62+
config :- expect AddJson(config, "data.json", keyVectors);
63+
config :- expect AddJson(config, "iotest.json", keyVectors);
64+
config :- expect AddJson(config, "PermTest.json", keyVectors);
65+
config.RunAllTests(keyVectors);
4266
}
4367
}

0 commit comments

Comments
 (0)