Skip to content

Commit 0f4f37a

Browse files
lucasmcdonald3lucasmcdonald3
committed
m
1 parent fe03425 commit 0f4f37a

File tree

2 files changed

+136
-33
lines changed

2 files changed

+136
-33
lines changed

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

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
4+
include "../Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy"
5+
include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
6+
7+
module {:extern} CreateWrappedItemEncryptor {
8+
import opened Wrappers
9+
import AwsCryptographyDbEncryptionSdkDynamoDbTypes
10+
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
11+
import DynamoDbItemEncryptor
12+
import Operations = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
13+
14+
// The `ensures` clause is copy-pasted from the DynamoDbItemEncryptor client method's `ensures` clause.
15+
method {:extern} CreateWrappedItemEncryptor(config: ENC.DynamoDbItemEncryptorConfig)
16+
returns (output: Result<ENC.IDynamoDbItemEncryptorClient, AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error>)
17+
requires config.keyring.Some? ==>
18+
config.keyring.value.ValidState()
19+
requires config.cmm.Some? ==>
20+
config.cmm.value.ValidState()
21+
requires config.legacyOverride.Some? ==>
22+
config.legacyOverride.value.encryptor.ValidState()
23+
modifies if config.keyring.Some? then
24+
config.keyring.value.Modifies
25+
else {}
26+
modifies if config.cmm.Some? then
27+
config.cmm.value.Modifies
28+
else {}
29+
modifies if config.legacyOverride.Some? then
30+
config.legacyOverride.value.encryptor.Modifies
31+
else {}
32+
ensures output.Success? ==>
33+
&& output.value is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient
34+
&& fresh(output.value)
35+
&& fresh(output.value.History)
36+
&& output.value.ValidState()
37+
&& var rconfig := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config;
38+
&& fresh(output.value.Modifies - Operations.ModifiesInternalConfig(rconfig))
39+
&& rconfig.logicalTableName == config.logicalTableName
40+
&& rconfig.partitionKeyName == config.partitionKeyName
41+
&& rconfig.sortKeyName == config.sortKeyName
42+
&& rconfig.attributeActionsOnEncrypt == config.attributeActionsOnEncrypt
43+
&& rconfig.allowedUnsignedAttributes == config.allowedUnsignedAttributes
44+
&& rconfig.allowedUnsignedAttributePrefix == config.allowedUnsignedAttributePrefix
45+
&& rconfig.algorithmSuiteId == config.algorithmSuiteId
46+
47+
//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#attribute-actions
48+
//= type=implication
49+
//# The [Key Action](#key-action)
50+
//# MUST be configured to the partition attribute and, if present, sort attribute.
51+
&& rconfig.version == Operations.VersionFromActions(config.attributeActionsOnEncrypt)
52+
&& config.partitionKeyName in config.attributeActionsOnEncrypt
53+
&& config.attributeActionsOnEncrypt[config.partitionKeyName] == Operations.KeyActionFromVersion(rconfig.version)
54+
&& (config.sortKeyName.Some? ==>
55+
&& config.sortKeyName.value in config.attributeActionsOnEncrypt
56+
&& config.attributeActionsOnEncrypt[config.sortKeyName.value] == Operations.KeyActionFromVersion(rconfig.version))
57+
58+
//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#plaintext-policy
59+
//# If not specified, encryption and decryption MUST behave according to `FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ`.
60+
ensures
61+
&& output.Success?
62+
&& config.plaintextOverride.None?
63+
==>
64+
&& var config := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config;
65+
&& config.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
66+
{
67+
var encryptor :- expect DynamoDbItemEncryptor.DynamoDbItemEncryptor(config);
68+
return Success(encryptor);
69+
}
70+
}

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

Lines changed: 66 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33

44
include "JsonItem.dfy"
55
include "CreateInterceptedDDBClient.dfy"
6+
include "CreateWrappedItemEncryptor.dfy"
67
include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
78

89
module {:options "-functionSyntax:4"} JsonConfig {
@@ -31,10 +32,10 @@ module {:options "-functionSyntax:4"} JsonConfig {
3132
import ParseJsonManifests
3233
import CreateInterceptedDDBClient
3334
import DynamoDbItemEncryptor
35+
import CreateWrappedItemEncryptor
36+
import Operations = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
3437

3538

36-
const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
37-
3839
predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000}
3940
type ConfigName = string
4041

@@ -130,7 +131,11 @@ module {:options "-functionSyntax:4"} JsonConfig {
130131
}
131132
}
132133

133-
method GetRoundTripTests(data : JSON) returns (output : Result<seq<RoundTripTest>, string>)
134+
method GetRoundTripTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
135+
returns (output : Result<seq<RoundTripTest>, string>)
136+
requires keys.ValidState()
137+
modifies keys.Modifies
138+
ensures keys.ValidState()
134139
{
135140
:- Need(data.Object?, "RoundTripTest Test must be an object.");
136141
var configs : map<string, TableConfig> := map[];
@@ -139,26 +144,34 @@ module {:options "-functionSyntax:4"} JsonConfig {
139144
for i := 0 to |data.obj| {
140145
var obj := data.obj[i];
141146
match obj.0 {
142-
case "Configs" => var src :- GetTableConfigs(obj.1); configs := src;
147+
case "Configs" => var src :- GetTableConfigs(obj.1, keys); configs := src;
143148
case "Records" => var src :- GetRecords(obj.1); records := src;
144149
case _ => return Failure("Unexpected part of a write test : '" + obj.0 + "'");
145150
}
146151
}
147152
return Success([RoundTripTest(configs, records)]);
148153
}
149154

150-
method GetWriteTests(data : JSON) returns (output : Result<seq<WriteTest> , string>)
155+
method GetWriteTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
156+
returns (output : Result<seq<WriteTest> , string>)
157+
requires keys.ValidState()
158+
modifies keys.Modifies
159+
ensures keys.ValidState()
151160
{
152161
:- Need(data.Array?, "Write Test list must be an array.");
153162
var results : seq<WriteTest> := [];
154163
for i := 0 to |data.arr| {
155164
var obj := data.arr[i];
156-
var item :- GetOneWriteTest(obj);
165+
var item :- GetOneWriteTest(obj, keys);
157166
results := results + [item];
158167
}
159168
return Success(results);
160169
}
161-
method GetOneWriteTest(data : JSON) returns (output : Result<WriteTest, string>)
170+
method GetOneWriteTest(data : JSON, keys: KeyVectors.KeyVectorsClient)
171+
returns (output : Result<WriteTest, string>)
172+
requires keys.ValidState()
173+
modifies keys.Modifies
174+
ensures keys.ValidState()
162175
{
163176
:- Need(data.Object?, "A Write Test must be an object.");
164177
var config : Option<TableConfig> := None;
@@ -168,7 +181,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
168181
for i := 0 to |data.obj| {
169182
var obj := data.obj[i];
170183
match obj.0 {
171-
case "Config" => var src :- GetOneTableConfig("foo", obj.1); config := Some(src);
184+
case "Config" => var src :- GetOneTableConfig("foo", obj.1, keys); config := Some(src);
172185
case "FileName" =>
173186
:- Need(obj.1.String?, "Write Test file name must be a string.");
174187
fileName := obj.1.str;
@@ -181,18 +194,26 @@ module {:options "-functionSyntax:4"} JsonConfig {
181194
return Success(WriteTest(config.value, records, fileName));
182195
}
183196

184-
method GetDecryptTests(data : JSON) returns (output : Result<seq<DecryptTest> , string>)
197+
method GetDecryptTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
198+
returns (output : Result<seq<DecryptTest> , string>)
199+
requires keys.ValidState()
200+
modifies keys.Modifies
201+
ensures keys.ValidState()
185202
{
186203
:- Need(data.Array?, "Decrypt Test list must be an array.");
187204
var results : seq<DecryptTest> := [];
188205
for i := 0 to |data.arr| {
189206
var obj := data.arr[i];
190-
var item :- GetOneDecryptTest(obj);
207+
var item :- GetOneDecryptTest(obj, keys);
191208
results := results + [item];
192209
}
193210
return Success(results);
194211
}
195-
method GetOneDecryptTest(data : JSON) returns (output : Result<DecryptTest, string>)
212+
method GetOneDecryptTest(data : JSON, keys: KeyVectors.KeyVectorsClient)
213+
returns (output : Result<DecryptTest, string>)
214+
requires keys.ValidState()
215+
modifies keys.Modifies
216+
ensures keys.ValidState()
196217
{
197218
:- Need(data.Object?, "A Decrypt Test must be an object.");
198219
var config : Option<TableConfig> := None;
@@ -202,7 +223,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
202223
for i := 0 to |data.obj| {
203224
var obj := data.obj[i];
204225
match obj.0 {
205-
case "Config" => var src :- GetOneTableConfig("foo", obj.1); config := Some(src);
226+
case "Config" => var src :- GetOneTableConfig("foo", obj.1, keys); config := Some(src);
206227
case "EncryptedRecords" => encRecords :- GetRecords(obj.1);
207228
case "PlainTextRecords" => plainRecords :- GetRecords(obj.1);
208229
case _ => return Failure("Unexpected part of a encrypt test : '" + obj.0 + "'");
@@ -214,24 +235,31 @@ module {:options "-functionSyntax:4"} JsonConfig {
214235
return Success(DecryptTest(config.value, encRecords, plainRecords));
215236
}
216237

217-
method GetTableConfigs(data : JSON) returns (output : Result<map<string, TableConfig> , string>)
238+
method GetTableConfigs(data : JSON, keys: KeyVectors.KeyVectorsClient)
239+
returns (output : Result<map<string, TableConfig> , string>)
240+
requires keys.ValidState()
241+
modifies keys.Modifies
242+
ensures keys.ValidState()
218243
{
219244
:- Need(data.Object?, "Search Config list must be an object.");
220245
var results : map<string, TableConfig> := map[];
221246
for i := 0 to |data.obj| {
222247
var obj := data.obj[i];
223-
var item :- GetOneTableConfig(obj.0, obj.1);
248+
var item :- GetOneTableConfig(obj.0, obj.1, keys);
224249
results := results[obj.0 := item];
225250
}
226251
return Success(results);
227252
}
228253

229-
method GetItemEncryptor(name : string, data : JSON)
254+
method GetItemEncryptor(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
230255
returns (encryptor : Result<DynamoDbItemEncryptor.DynamoDbItemEncryptorClient, string>)
256+
requires keys.ValidState()
257+
modifies keys.Modifies
258+
ensures keys.ValidState()
231259
ensures encryptor.Success? ==>
232260
&& encryptor.value.ValidState()
233261
&& fresh(encryptor.value)
234-
&& fresh(encryptor.value.Modifies)
262+
&& fresh(encryptor.value.Modifies - Operations.ModifiesInternalConfig(encryptor.value.config))
235263
{
236264
:- Need(data.Object?, "A Table Config must be an object.");
237265
var logicalTableName := TableName;
@@ -296,11 +324,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
296324
}
297325
}
298326

299-
var keys :- expect KeyVectors.KeyVectors(
300-
KeyVectorsTypes.KeyVectorsConfig(
301-
keyManifestPath := DEFAULT_KEYS
302-
)
303-
);
304327
var keyDescription :-
305328
if |key| == 0 then
306329
Success(KeyVectorsTypes.Hierarchy(KeyVectorsTypes.HierarchyKeyring(
@@ -327,13 +350,20 @@ module {:options "-functionSyntax:4"} JsonConfig {
327350
legacyOverride := legacyOverride,
328351
plaintextOverride := plaintextOverride
329352
);
330-
var enc : ENC.IDynamoDbItemEncryptorClient :- expect DynamoDbItemEncryptor.DynamoDbItemEncryptor(encryptorConfig);
353+
var enc : ENC.IDynamoDbItemEncryptorClient :- expect CreateWrappedItemEncryptor.CreateWrappedItemEncryptor(encryptorConfig);
354+
// var enc : ENC.IDynamoDbItemEncryptorClient :- expect DynamoDbItemEncryptor.DynamoDbItemEncryptor(encryptorConfig);
331355
assert enc is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
332356
var encr := enc as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
333357
return Success(encr);
334358
}
335359

336-
method GetOneTableConfig(name : string, data : JSON) returns (output : Result<TableConfig, string>)
360+
361+
362+
method GetOneTableConfig(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
363+
returns (output : Result<TableConfig, string>)
364+
requires keys.ValidState()
365+
modifies keys.Modifies
366+
ensures keys.ValidState()
337367
{
338368
:- Need(data.Object?, "A Table Config must be an object.");
339369
var logicalTableName := TableName;
@@ -400,11 +430,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
400430
}
401431
}
402432

403-
var keys :- expect KeyVectors.KeyVectors(
404-
KeyVectorsTypes.KeyVectorsConfig(
405-
keyManifestPath := DEFAULT_KEYS
406-
)
407-
);
408433
var keyDescription :-
409434
if |key| == 0 then
410435
Success(KeyVectorsTypes.Hierarchy(KeyVectorsTypes.HierarchyKeyring(
@@ -1114,19 +1139,27 @@ module {:options "-functionSyntax:4"} JsonConfig {
11141139
));
11151140
}
11161141

1117-
method GetIoTests(data : JSON) returns (output : Result<seq<IoTest> , string>)
1142+
method GetIoTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
1143+
returns (output : Result<seq<IoTest> , string>)
1144+
requires keys.ValidState()
1145+
modifies keys.Modifies
1146+
ensures keys.ValidState()
11181147
{
11191148
:- Need(data.Object?, "IoTests must be an object.");
11201149
var results : seq<IoTest> := [];
11211150
for i := 0 to |data.obj| {
11221151
var obj := data.obj[i];
1123-
var item :- GetOneIoTest(obj.0, obj.1);
1152+
var item :- GetOneIoTest(obj.0, obj.1, keys);
11241153
results := results + [item];
11251154
}
11261155
return Success(results);
11271156
}
11281157

1129-
method GetOneIoTest(name : string, data : JSON) returns (output : Result<IoTest, string>)
1158+
method GetOneIoTest(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
1159+
returns (output : Result<IoTest, string>)
1160+
requires keys.ValidState()
1161+
modifies keys.Modifies
1162+
ensures keys.ValidState()
11301163
{
11311164
:- Need(data.Object?, "IoTest must be an object.");
11321165
var readConfig : Option<TableConfig> := None;
@@ -1138,8 +1171,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
11381171
for i := 0 to |data.obj| {
11391172
var obj := data.obj[i];
11401173
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);
1174+
case "WriteConfig" => var config :- GetOneTableConfig(obj.0, obj.1, keys); writeConfig := Some(config);
1175+
case "ReadConfig" => var config :- GetOneTableConfig(obj.0, obj.1, keys); readConfig := Some(config);
11431176
case "Records" => records :- GetRecords(obj.1);
11441177
case "Values" => values :- GetValueMap(data.obj[i].1);
11451178
case "Queries" => queries :- GetSimpleQueries(data.obj[i].1);

0 commit comments

Comments
 (0)