Skip to content

Commit 0e9fb34

Browse files
ajewellamzajewellamz
authored
feat: test vectors (#704)
* feat: test vectors
1 parent 8e78ad1 commit 0e9fb34

File tree

17 files changed

+1956
-1286
lines changed

17 files changed

+1956
-1286
lines changed

‎.github/workflows/ci_test_vector_net.yml

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,4 @@ jobs:
5959
working-directory: ./TestVectors/runtimes/net
6060
run: |
6161
cp ../java/*.json .
62-
# dotnet run
63-
echo can't build until we make type conversions public
64-
echo can't run until we update MPL/ComAmazonawsDynamodb
62+
dotnet run

‎DynamoDbEncryption/runtimes/java/src/test/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryptionInterceptorIntegrationTests.java

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -390,12 +390,18 @@ public void TestScan() {
390390
.tableName(TEST_TABLE_NAME)
391391
.filterExpression("partition_key = :val")
392392
.expressionAttributeValues(attrValues)
393-
.build();
394-
395-
ScanResponse scanResponse = ddbKmsKeyring.scan(scanRequest);
396-
assertEquals(200, scanResponse.sdkHttpResponse().statusCode());
397-
assertEquals(2, (double) scanResponse.count());
398-
Map<String, AttributeValue> item = scanResponse.items().get(0);
393+
.consistentRead(true)
394+
.build();
395+
List<Map<String,AttributeValue>> results = new ArrayList<>();
396+
ScanResponse scanResponse;
397+
do {
398+
scanResponse = ddbKmsKeyring.scan(scanRequest);
399+
assertEquals(200, scanResponse.sdkHttpResponse().statusCode());
400+
results.addAll(scanResponse.items());
401+
scanRequest = scanRequest.toBuilder().exclusiveStartKey(scanResponse.lastEvaluatedKey()).build();
402+
} while (scanResponse.lastEvaluatedKey().size() > 0);
403+
assertEquals(2, (double) results.size());
404+
Map<String, AttributeValue> item = results.get(0);
399405
assertEquals(partitionValue, item.get(TEST_PARTITION_NAME).s());
400406
assertEquals(attrValue, item.get(TEST_ATTR_NAME).s());
401407
}

‎DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@
3434
<ItemGroup>
3535
<PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.300.2"/>
3636
<PackageReference Include="AWSSDK.Core" Version="3.7.300.2"/>
37-
<PackageReference Include="AWS.Cryptography.MaterialProviders" Version="1.0.0"/>
37+
<ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>
3838
<!--
3939
System.Collections.Immutable can be removed once dafny.msbuild is updated with
4040
https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned

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

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
4+
include "JsonConfig.dfy"
5+
include "WriteManifest.dfy"
6+
include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
7+
8+
module {:options "-functionSyntax:4"} DecryptManifest {
9+
import opened Wrappers
10+
import opened StandardLibrary
11+
import opened StandardLibrary.UInt
12+
import opened JSON.Values
13+
import opened WriteManifest
14+
import JSON.API
15+
import JSON.Errors
16+
import DdbItemJson
17+
import StandardLibrary.String
18+
import FileIO
19+
import opened JSONHelpers
20+
import JsonConfig
21+
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
22+
23+
method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON) returns (output : Result<bool, string>)
24+
{
25+
var enc :- JsonConfig.GetRecord(encrypted);
26+
var plain :- JsonConfig.GetRecord(plaintext);
27+
var encryptor :- JsonConfig.GetItemEncryptor(name, config);
28+
var decrypted :- expect encryptor.DecryptItem(
29+
ENC.DecryptItemInput(
30+
encryptedItem:=enc.item
31+
)
32+
);
33+
expect DdbItemJson.NormalizeItem(decrypted.plaintextItem) == DdbItemJson.NormalizeItem(plain.item);
34+
35+
return Success(true);
36+
}
37+
38+
method OneNegativeTest(name : string, config : JSON, encrypted : JSON) returns (output : Result<bool, string>)
39+
{
40+
var enc :- JsonConfig.GetRecord(encrypted);
41+
var encryptor :- JsonConfig.GetItemEncryptor(name, config);
42+
var decrypted := encryptor.DecryptItem(
43+
ENC.DecryptItemInput(
44+
encryptedItem:=enc.item
45+
)
46+
);
47+
if decrypted.Success? {
48+
return Failure("Failed to fail to decrypt " + name);
49+
}
50+
return Success(true);
51+
}
52+
53+
method OneTest(name : string, value : JSON) returns (output : Result<bool, string>)
54+
{
55+
:- Need(value.Object?, "Test must be an object");
56+
print "Decrypting ", name, "\n";
57+
58+
var types : Option<string> := None;
59+
var description : Option<string> := None;
60+
var config : Option<JSON> := None;
61+
var encrypted : Option<JSON> := None;
62+
var plaintext : Option<JSON> := None;
63+
64+
for i := 0 to |value.obj| {
65+
var obj := value.obj[i];
66+
match obj.0 {
67+
case "type" =>
68+
:- Need(obj.1.String?, "Value of 'type' must be a string.");
69+
types := Some(obj.1.str);
70+
case "description" =>
71+
:- Need(obj.1.String?, "Value of 'description' must be a string.");
72+
description := Some(obj.1.str);
73+
case "config" =>
74+
:- Need(obj.1.Object?, "Value of 'config' must be an object.");
75+
config := Some(obj.1);
76+
case "encrypted" =>
77+
:- Need(obj.1.Object?, "Value of 'record' must be an object.");
78+
encrypted := Some(obj.1);
79+
case "plaintext" =>
80+
:- Need(obj.1.Object?, "Value of 'record' must be an object.");
81+
plaintext := Some(obj.1);
82+
case _ => return Failure("Unknown test member : " + obj.0 + " in " + name);
83+
}
84+
}
85+
:- Need(types.Some?, "Test requires a 'type' member.");
86+
:- Need(description.Some?, "Test requires a 'description' member.");
87+
:- Need(config.Some?, "Test requires a 'config' member.");
88+
:- Need(encrypted.Some?, "Test requires a 'encrypted' member.");
89+
90+
if types.value == "positive-decrypt" {
91+
:- Need(plaintext.Some?, "positive-decrypt Test requires a 'plaintext' member.");
92+
output := OnePositiveTest(name, config.value, encrypted.value, plaintext.value);
93+
} else if types.value == "negative-decrypt" {
94+
output := OneNegativeTest(name, config.value, encrypted.value);
95+
} else {
96+
return Failure("Invalid encrypt type : '" + types.value + "'.");
97+
}
98+
}
99+
100+
method Decrypt(inFile : string) returns (output : Result<bool, string>)
101+
{
102+
var configBv :- expect FileIO.ReadBytesFromFile(inFile);
103+
var configBytes := BvToBytes(configBv);
104+
var json :- expect API.Deserialize(configBytes);
105+
106+
:- Need(json.Object?, "Decrypt file must contain a JSON object.");
107+
var keys : Option<string> := None;
108+
var client : Option<seq<(string, JSON)>> := None;
109+
var manifest : Option<seq<(string, JSON)>> := None;
110+
var tests : Option<seq<(string, JSON)>> := None;
111+
112+
for i := 0 to |json.obj| {
113+
var obj := json.obj[i];
114+
match obj.0 {
115+
case "keys" =>
116+
:- Need(obj.1.String?, "Value of 'keys' must be a string.");
117+
keys := Some(obj.1.str);
118+
case "client" =>
119+
:- Need(obj.1.Object?, "Value of 'client' must be an Object.");
120+
client := Some(obj.1.obj);
121+
case "manifest" =>
122+
:- Need(obj.1.Object?, "Value of 'manifest' must be an object.");
123+
manifest := Some(obj.1.obj);
124+
case "tests" =>
125+
:- Need(obj.1.Object?, "Value of 'tests' must be an object.");
126+
tests := Some(obj.1.obj);
127+
case _ => return Failure("Unknown top level encrypt tag : " + obj.0);
128+
}
129+
}
130+
:- Need(keys.Some?, "Decrypt manifest requires a 'keys' member.");
131+
:- Need(client.Some?, "Decrypt manifest requires a 'client' member.");
132+
:- Need(manifest.Some?, "Decrypt manifest requires a 'manifest' member.");
133+
:- Need(tests.Some?, "Decrypt manifest requires a 'tests' member.");
134+
135+
for i := 0 to |manifest.value| {
136+
var obj := manifest.value[i];
137+
match obj.0 {
138+
case "type" =>
139+
:- Need(obj.1.String?, "Value of 'type' must be a string.");
140+
:- Need(obj.1.str == DECRYPT_TYPE, "Value of 'type' must be '" + DECRYPT_TYPE + "'.");
141+
case "version" =>
142+
:- Need(obj.1.String?, "Value of 'version' must be a string.");
143+
:- Need(obj.1.str == "1", "Value of 'version' must be '1'");
144+
case _ => return Failure("Unknown manifest member : " + obj.0);
145+
}
146+
}
147+
148+
for i := 0 to |tests.value| {
149+
var obj := tests.value[i];
150+
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
151+
var _ :- OneTest(obj.0, obj.1);
152+
}
153+
154+
return Success(true);
155+
}
156+
157+
}

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

Lines changed: 197 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,197 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
4+
include "JsonConfig.dfy"
5+
include "WriteManifest.dfy"
6+
include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
7+
8+
module {:options "-functionSyntax:4"} EncryptManifest {
9+
import opened Wrappers
10+
import opened StandardLibrary
11+
import opened StandardLibrary.UInt
12+
import opened JSON.Values
13+
import opened WriteManifest
14+
import JSON.API
15+
import JSON.Errors
16+
import opened DynamoDbEncryptionUtil
17+
import DdbItemJson
18+
import StandardLibrary.String
19+
import FileIO
20+
import opened JSONHelpers
21+
import JsonConfig
22+
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
23+
24+
function Manifest() : (string, JSON)
25+
{
26+
var result : seq<(string, JSON)> :=
27+
[
28+
("type", String(DECRYPT_TYPE)),
29+
("version", String("1"))
30+
];
31+
("manifest", Object(result))
32+
}
33+
34+
function Client(lang : string, version : string) : (string, JSON)
35+
{
36+
var result : seq<(string, JSON)> :=
37+
[
38+
("name", String(LIB_PREFIX + lang)),
39+
("version", String(version))
40+
];
41+
("client", Object(result))
42+
}
43+
44+
method OnePositiveTest(name : string, theType : string, desc : string, config : JSON, decryptConfig : Option<JSON>, record : JSON) returns (output : Result<(string, JSON), string>)
45+
{
46+
var rec :- JsonConfig.GetRecord(record);
47+
var encryptor :- JsonConfig.GetItemEncryptor(name, config);
48+
var encrypted :- expect encryptor.EncryptItem(
49+
ENC.EncryptItemInput(
50+
plaintextItem:=rec.item
51+
)
52+
);
53+
var item :- expect DdbItemJson.DdbItemToJson(encrypted.encryptedItem);
54+
55+
var result : seq<(string, JSON)> :=
56+
[
57+
("type", String(theType)),
58+
("description", String(desc)),
59+
("config", if decryptConfig.Some? then decryptConfig.value else config),
60+
("plaintext", record),
61+
("encrypted", item)
62+
];
63+
return Success((name, Object(result)));
64+
}
65+
66+
method OneNegativeTest(name : string, config : JSON, record : JSON) returns (output : Result<bool, string>)
67+
{
68+
var rec :- JsonConfig.GetRecord(record);
69+
var encryptor :- JsonConfig.GetItemEncryptor(name, config);
70+
var encrypted := encryptor.EncryptItem(
71+
ENC.EncryptItemInput(
72+
plaintextItem:=rec.item
73+
)
74+
);
75+
if encrypted.Success? {
76+
return Failure("Test " + name + " failed to fail to encrypt.");
77+
}
78+
return Success(true);
79+
}
80+
81+
82+
method OneTest(name : string, value : JSON) returns (output : Result<Option<(string, JSON)>, string>)
83+
{
84+
:- Need(value.Object?, "Test must be an object");
85+
print "Examining ", name, "\n";
86+
87+
var types : Option<string> := None;
88+
var description : Option<string> := None;
89+
var config : Option<JSON> := None;
90+
var decryptConfig : Option<JSON> := None;
91+
var record : Option<JSON> := None;
92+
93+
for i := 0 to |value.obj| {
94+
var obj := value.obj[i];
95+
match obj.0 {
96+
case "type" =>
97+
:- Need(obj.1.String?, "Value of 'type' must be a string.");
98+
types := Some(obj.1.str);
99+
case "description" =>
100+
:- Need(obj.1.String?, "Value of 'description' must be a string.");
101+
description := Some(obj.1.str);
102+
case "config" =>
103+
:- Need(obj.1.Object?, "Value of 'config' must be an object.");
104+
config := Some(obj.1);
105+
case "decryptConfig" =>
106+
:- Need(obj.1.Object?, "Value of 'decryptConfig' must be an object.");
107+
decryptConfig := Some(obj.1);
108+
case "record" =>
109+
:- Need(obj.1.Object?, "Value of 'record' must be an object.");
110+
record := Some(obj.1);
111+
case _ => return Failure("Unknown test member : " + obj.0 + " in " + name);
112+
}
113+
}
114+
:- Need(types.Some?, "Test requires a 'type' member.");
115+
:- Need(description.Some?, "Test requires a 'description' member.");
116+
:- Need(config.Some?, "Test requires a 'config' member.");
117+
:- Need(record.Some?, "Test requires a 'record' member.");
118+
119+
if types.value == "positive-encrypt" {
120+
var x :- OnePositiveTest(name, "positive-decrypt", description.value, config.value, decryptConfig, record.value);
121+
return Success(Some(x));
122+
} else if types.value == "negative-decrypt" {
123+
var x :- OnePositiveTest(name, "negative-decrypt", description.value, config.value, decryptConfig, record.value);
124+
return Success(Some(x));
125+
} else if types.value == "negative-encrypt" {
126+
var _ := OneNegativeTest(name, config.value, record.value);
127+
return Success(None);
128+
} else {
129+
return Failure("Invalid encrypt type : '" + types.value + "'.");
130+
}
131+
}
132+
133+
method Encrypt(inFile : string, outFile : string, lang : string, version : string) returns (output : Result<bool, string>)
134+
{
135+
var configBv :- expect FileIO.ReadBytesFromFile(inFile);
136+
var configBytes := BvToBytes(configBv);
137+
var json :- expect API.Deserialize(configBytes);
138+
139+
:- Need(json.Object?, "Encrypt file must contain a JSON object.");
140+
var keys : Option<string> := None;
141+
var manifest : Option<seq<(string, JSON)>> := None;
142+
var tests : Option<seq<(string, JSON)>> := None;
143+
144+
for i := 0 to |json.obj| {
145+
var obj := json.obj[i];
146+
match obj.0 {
147+
case "keys" =>
148+
:- Need(obj.1.String?, "Value of 'keys' must be a string.");
149+
keys := Some(obj.1.str);
150+
case "manifest" =>
151+
:- Need(obj.1.Object?, "Value of 'manifest' must be an object.");
152+
manifest := Some(obj.1.obj);
153+
case "tests" =>
154+
:- Need(obj.1.Object?, "Value of 'tests' must be an object.");
155+
tests := Some(obj.1.obj);
156+
case _ => return Failure("Unknown top level encrypt tag : " + obj.0);
157+
}
158+
}
159+
:- Need(keys.Some?, "Encrypt manifest requires a 'keys' member.");
160+
:- Need(manifest.Some?, "Encrypt manifest requires a 'manifest' member.");
161+
:- Need(tests.Some?, "Encrypt manifest requires a 'tests' member.");
162+
163+
for i := 0 to |manifest.value| {
164+
var obj := manifest.value[i];
165+
match obj.0 {
166+
case "type" =>
167+
:- Need(obj.1.String?, "Value of 'type' must be a string.");
168+
:- Need(obj.1.str == ENCRYPT_TYPE, "Value of 'type' must be '" + ENCRYPT_TYPE + "'.");
169+
case "version" =>
170+
:- Need(obj.1.String?, "Value of 'version' must be a string.");
171+
:- Need(obj.1.str == "1", "Value of 'version' must be '1'");
172+
case _ => return Failure("Unknown manifest member : " + obj.0);
173+
}
174+
}
175+
176+
var result : seq<(string, JSON)> :=
177+
[Manifest(), Client(lang, version), ("keys", String("file://keys.json"))];
178+
179+
var test : seq<(string, JSON)> := [];
180+
181+
for i := 0 to |tests.value| {
182+
var obj := tests.value[i];
183+
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
184+
var newTest :- OneTest(obj.0, obj.1);
185+
if newTest.Some? {
186+
test := test + [newTest.value];
187+
}
188+
}
189+
190+
var final := Object(result + [("tests", Object(test))]);
191+
var jsonBytes :- expect API.Serialize(final);
192+
var jsonBv := BytesBv(jsonBytes);
193+
var x :- expect FileIO.WriteBytesToFile(outFile, jsonBv);
194+
return Success(true);
195+
}
196+
197+
}

0 commit comments

Comments
 (0)