Skip to content

Commit c2281fb

Browse files
ajewellamzajewellamz
committed
m
1 parent 99ff4ef commit c2281fb

File tree

5 files changed

+172
-81
lines changed

5 files changed

+172
-81
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -345,9 +345,9 @@ module CompoundBeacon {
345345
if |inParts| == 0 then
346346
[]
347347
else if inParts[0].Encrypted? then
348-
[inParts[0].beacon.numberOfBuckets]
348+
[inParts[0].beacon.numberOfBuckets] + GetBucketCountsFromParts(inParts[1..])
349349
else
350-
[]
350+
GetBucketCountsFromParts(inParts[1..])
351351
}
352352

353353
// for the given attribute value, return the beacon value

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ module DynamoToStruct {
4040
}
4141
by method {
4242
var attrNames : seq<AttributeName> := SortedSets.ComputeSetToSequence(item.Keys);
43-
var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();
43+
var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>((k: AttributeName, v: StructuredDataTerminal) => true, false);
4444
SequenceIsSafeBecauseItIsInMemory(attrNames);
4545
for i : uint64 := 0 to |attrNames| as uint64 {
4646
var k := attrNames[i];
@@ -76,7 +76,7 @@ module DynamoToStruct {
7676
}
7777
by method {
7878
var attrNames : seq<AttributeName> := SortedSets.ComputeSetToSequence(orig.Keys);
79-
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>();
79+
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>((k: AttributeName, v: AttributeValue) => true, false);
8080
SequenceIsSafeBecauseItIsInMemory(attrNames);
8181
for i : uint64 := 0 to |attrNames| as uint64 {
8282
var k := attrNames[i];
@@ -125,7 +125,7 @@ module DynamoToStruct {
125125
}
126126
by method {
127127
var attrNames : seq<AttributeName> := SortedSets.ComputeSetToSequence(orig.Keys);
128-
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>();
128+
var m := new DafnyLibraries.MutableMap<AttributeName, AttributeValue>((k: AttributeName, v: AttributeValue) => true, false);
129129
SequenceIsSafeBecauseItIsInMemory(attrNames);
130130
for i : uint64 := 0 to |attrNames| as uint64 {
131131
var k := attrNames[i];

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

Lines changed: 125 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -135,37 +135,37 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
135135
print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n";
136136
}
137137

138-
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
139-
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
140-
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
141-
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
142-
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
143-
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
144-
// var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
145-
// var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors);
146-
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_39.json", keyVectors);
147-
// var _ :- expect WriteManifest.Write("encrypt.json");
148-
// var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
149-
// var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
138+
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
139+
var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
140+
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
141+
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
142+
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
143+
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
144+
var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
145+
var _ :- expect DecryptManifest.Decrypt("decrypt_go_38.json", keyVectors);
146+
var _ :- expect DecryptManifest.Decrypt("decrypt_java_39.json", keyVectors);
147+
var _ :- expect WriteManifest.Write("encrypt.json");
148+
var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
149+
var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
150150
if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
151151
print "\nRunning no tests\n";
152152
return;
153153
}
154154
Validate();
155155
StringOrdering();
156156
BucketTests();
157-
// LargeTests();
158-
// PerfQueryTests();
159-
// BasicIoTest();
160-
// RunIoTests();
161-
// BasicQueryTest();
162-
// ConfigModTest();
163-
// ComplexTests();
164-
// WriteTests();
165-
// RoundTripTests();
166-
// DecryptTests();
167-
// var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
168-
// DeleteTable(client);
157+
LargeTests();
158+
PerfQueryTests();
159+
BasicIoTest();
160+
RunIoTests();
161+
BasicQueryTest();
162+
ConfigModTest();
163+
ComplexTests();
164+
WriteTests();
165+
RoundTripTests();
166+
DecryptTests();
167+
var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
168+
DeleteTable(client);
169169
}
170170

171171
function MakeBucketRecord(x : nat) : DDB.AttributeMap
@@ -186,11 +186,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
186186
]
187187
}
188188

189-
method DoBucketQuery(client : DDB.IDynamoDBClient, bucket : nat, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, numQueries : nat)
189+
method DoBucketQuery(client : DDB.IDynamoDBClient, bucket : Types.BucketNumber, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, numQueries : Types.BucketCount)
190190
requires counts.Length == 100
191191
requires client.ValidState()
192192
requires client.Modifies !! {counts}
193-
requires 0 < numQueries
194193
ensures client.ValidState()
195194
modifies client.Modifies
196195
modifies counts
@@ -201,7 +200,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
201200
invariant client.ValidState()
202201
invariant client.Modifies !! {counts}
203202
{
204-
var bucketNumber := DDB.AttributeValue.N(String.Base10Int2String(bucket));
203+
var bucketNumber := DDB.AttributeValue.N(String.Base10Int2String(bucket as int));
205204
var values : DDB.ExpressionAttributeValueMap := query.ExpressionAttributeValues.UnwrapOr(map[]);
206205
values := values[":aws_dbe_bucket" := bucketNumber];
207206
var q := query.(ExclusiveStartKey := lastKey, ExpressionAttributeValues := Some(values));
@@ -222,8 +221,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
222221
if custom {
223222
expect "PreferredBucket" in item;
224223
expect item["PreferredBucket"].N?;
225-
var stored_bucket :- expect StrToInt(item["PreferredBucket"].N);
226-
expect bucket == stored_bucket % numQueries;
224+
var stored_bucket : int :- expect StrToInt(item["PreferredBucket"].N);
225+
expect bucket as int == stored_bucket % numQueries as int;
227226
}
228227
}
229228
}
@@ -276,7 +275,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
276275
}
277276

278277

279-
method TestBucketQueryFailure(client : DDB.IDynamoDBClient, bucket : nat, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, numQueries : nat)
278+
method TestBucketQueryFailure(client : DDB.IDynamoDBClient, bucket : Types.BucketCount, query : DDB.QueryInput, counts : array<int>, queryName : string, custom : bool, numQueries : Types.BucketCount)
280279
requires counts.Length == 100
281280
requires client.ValidState()
282281
requires client.Modifies !! {counts}
@@ -285,26 +284,42 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
285284
modifies client.Modifies
286285
modifies counts
287286
{
288-
var bucketNumber := DDB.AttributeValue.N(String.Base10Int2String(bucket));
287+
var bucketNumber := DDB.AttributeValue.N(String.Base10Int2String(bucket as int));
289288
var values : DDB.ExpressionAttributeValueMap := query.ExpressionAttributeValues.UnwrapOr(map[]);
290289
values := values[":aws_dbe_bucket" := bucketNumber];
291290
var q := query.(ExpressionAttributeValues := Some(values));
292291
var result := client.Query(q);
293292
expect result.Failure?;
294293
}
295294

296-
297-
method TestBucketQueries(client : DDB.IDynamoDBClient, numQueries : nat, q : DDB.QueryInput, queryName : string, custom : bool := false)
295+
method TestBucketQueries(client : DDB.IDynamoDBClient, numQueries : Types.BucketCount, q : DDB.QueryInput, trans : DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient, queryName : string, custom : bool := false)
298296
requires 0 < numQueries <= 5
299297
requires client.ValidState()
298+
requires trans.ValidState()
300299
ensures client.ValidState()
300+
ensures trans.ValidState()
301301
modifies client.Modifies
302+
modifies trans.Modifies
302303
{
304+
var input := Trans.GetNumberOfQueriesInput(input := q);
305+
var res :- expect trans.GetNumberOfQueries(input);
306+
if res.numberOfQueries != numQueries {
307+
print "numberOfQueries should have been\n", numQueries, " but was ", res.numberOfQueries, " for ", queryName,"\n";
308+
}
309+
expect res.numberOfQueries == numQueries;
310+
303311
var counts: array<int> := new int[100](i => 0);
304-
for i := 0 to numQueries {
312+
for i : Types.BucketNumber := 0 to numQueries
313+
invariant client.ValidState()
314+
invariant trans.ValidState()
315+
{
305316
DoBucketQuery(client, i, q, counts, queryName, custom, numQueries);
306317
}
307-
for i := numQueries to 5 {
318+
319+
for i : Types.BucketNumber := numQueries to 5
320+
invariant client.ValidState()
321+
invariant trans.ValidState()
322+
{
308323
TestBucketQueryFailure(client, i, q, counts, queryName, custom, numQueries);
309324
}
310325

@@ -522,6 +537,32 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
522537
ExpressionAttributeValues := Some(map[":attr2671" := DDB.AttributeValue.S("2_BBBB.6_FFFF.7_GGGG.1_AAAA")])
523538
)
524539
}
540+
function GetCompScan2671() : DDB.ScanInput
541+
{
542+
DDB.ScanInput(
543+
TableName := TableName,
544+
FilterExpression := Some("Comp2671 = :attr2671"),
545+
ExpressionAttributeValues := Some(map[":attr2671" := DDB.AttributeValue.S("2_BBBB.6_FFFF.7_GGGG.1_AAAA")])
546+
)
547+
}
548+
function GetCompQuery1472() : DDB.QueryInput
549+
{
550+
DDB.QueryInput(
551+
TableName := TableName,
552+
IndexName := Some("ATTR_INDEX1472"),
553+
FilterExpression := None,
554+
KeyConditionExpression := Some("Comp1472 = :attr1472"),
555+
ExpressionAttributeValues := Some(map[":attr1472" := DDB.AttributeValue.S("1_AAAA.4_DDDD.7_GGGG.2_BBBB")])
556+
)
557+
}
558+
function GetCompScan1472() : DDB.ScanInput
559+
{
560+
DDB.ScanInput(
561+
TableName := TableName,
562+
FilterExpression := Some("Comp1472 = :attr1472"),
563+
ExpressionAttributeValues := Some(map[":attr1472" := DDB.AttributeValue.S("1_AAAA.4_DDDD.7_GGGG.2_BBBB")])
564+
)
565+
}
525566

526567
function GetBucketQuery1() : DDB.QueryInput
527568
{
@@ -665,14 +706,24 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
665706
}
666707
}
667708

668-
method BucketTest3()
709+
method MakeTrans(config : TableConfig) returns (output : DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
710+
ensures fresh(output)
711+
ensures fresh(output.Modifies)
712+
ensures output.ValidState()
669713
{
670-
expect "bucket_encrypt" in largeEncryptionConfigs;
671-
var config := largeEncryptionConfigs["bucket_encrypt"];
672714
var configs := Types.DynamoDbTablesEncryptionConfig (tableEncryptionConfigs := map[TableName := config.config]);
673715
assume {:axiom} false;
674716
var trans :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(configs);
717+
return trans;
718+
}
675719

720+
method BucketTest3()
721+
{
722+
expect "bucket_encrypt" in largeEncryptionConfigs;
723+
var config := largeEncryptionConfigs["bucket_encrypt"];
724+
var trans := MakeTrans(config);
725+
assert fresh(trans);
726+
assert trans.ValidState();
676727
TestScanTrans(trans, GetBucketScan1(5), "Attr6 = :attr6");
677728
TestScanTrans(trans, GetBucketScan1(1), "(aws_dbe_b_Attr2 = :attr2) OR (aws_dbe_b_Attr2 = :attr2AA)");
678729
TestScanTrans(trans, GetBucketScan2(5, 1), "(Attr6 = :attr6 AND aws_dbe_b_Attr2 = :attr2) OR (Attr6 = :attr6 AND aws_dbe_b_Attr2 = :attr2AA)");
@@ -690,6 +741,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
690741
expect "bucket_encrypt" in largeEncryptionConfigs;
691742
var config := largeEncryptionConfigs["bucket_encrypt"];
692743
var wClient, rClient := SetupTestTable(config, config);
744+
var trans := MakeTrans(config);
745+
693746
for i : nat := 0 to 100 {
694747
var putInput := DDB.PutItemInput(
695748
TableName := TableName,
@@ -700,20 +753,20 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
700753
var q1 := DDB.QueryInput(
701754
TableName := TableName
702755
);
703-
TestBucketQueries(rClient, 5, GetBucketQuery5(), "bucket query 5");
704-
TestBucketQueries(rClient, 4, GetBucketQuery4(), "bucket query 4");
705-
TestBucketQueries(rClient, 3, GetBucketQuery3(), "bucket query 3");
706-
TestBucketQueries(rClient, 2, GetBucketQuery2(), "bucket query 2");
707-
TestBucketQueries(rClient, 1, GetBucketQuery1(), "bucket query 1");
756+
TestBucketQueries(rClient, 5, GetBucketQuery5(), trans, "bucket query 5");
757+
TestBucketQueries(rClient, 4, GetBucketQuery4(), trans, "bucket query 4");
758+
TestBucketQueries(rClient, 3, GetBucketQuery3(), trans, "bucket query 3");
759+
TestBucketQueries(rClient, 2, GetBucketQuery2(), trans, "bucket query 2");
760+
TestBucketQueries(rClient, 1, GetBucketQuery1(), trans, "bucket query 1");
708761

709-
TestBucketQueries(rClient, 5, GetBucketQuery15(), "bucket query 15");
710-
TestBucketQueries(rClient, 5, GetBucketQuery51(), "bucket query 51");
711-
TestBucketQueries(rClient, 5, GetBucketQuery23(), "bucket query 23");
762+
TestBucketQueries(rClient, 5, GetBucketQuery15(), trans, "bucket query 15");
763+
TestBucketQueries(rClient, 5, GetBucketQuery51(), trans, "bucket query 51");
764+
TestBucketQueries(rClient, 5, GetBucketQuery23(), trans, "bucket query 23");
712765

713-
TestBucketQueries(rClient, 1, GetBucketQuery15F(), "bucket query 15F", false);
714-
TestBucketQueries(rClient, 2, GetBucketQuery25F(), "bucket query 25F", false);
715-
TestBucketQueries(rClient, 3, GetBucketQuery35F(), "bucket query 35F", false);
716-
TestBucketQueries(rClient, 4, GetBucketQuery45F(), "bucket query 45F", false);
766+
TestBucketQueries(rClient, 1, GetBucketQuery15F(), trans, "bucket query 15F", false);
767+
TestBucketQueries(rClient, 2, GetBucketQuery25F(), trans, "bucket query 25F", false);
768+
TestBucketQueries(rClient, 3, GetBucketQuery35F(), trans, "bucket query 35F", false);
769+
TestBucketQueries(rClient, 4, GetBucketQuery45F(), trans, "bucket query 45F", false);
717770

718771
var scanCount4 := 0;
719772
var scanCount5 := 0;
@@ -757,19 +810,19 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
757810
expect "complex_bucket_encrypt" in largeEncryptionConfigs;
758811
var config := largeEncryptionConfigs["complex_bucket_encrypt"];
759812
var wClient, rClient := SetupTestTable(config, config);
813+
var trans := MakeTrans(config);
814+
760815
for i : nat := 0 to 100 {
761816
var putInput := DDB.PutItemInput(
762817
TableName := TableName,
763818
Item := MakeBucketRecord(i)
764819
);
765820
var _ :- expect wClient.PutItem(putInput);
766821
}
767-
print "BucketTest4 Wrote";
768-
TestBucketQueries(rClient, 2, GetCompQuery2671(), "comp query 2671");
769-
print "BucketTest4 Did One";
770-
771-
// TestBucketScan(rClient, GetBucketScan6(0,1,2,3,4,5));
772-
TestBucketScan(rClient, GetBucketScan6(5,4,3,2,1,0));
822+
TestBucketQueries(rClient, 2, GetCompQuery2671(), trans, "comp query 2671");
823+
TestBucketScan(rClient, GetCompScan2671());
824+
TestBucketQueries(rClient, 4, GetCompQuery1472(), trans, "comp query 1472");
825+
TestBucketScan(rClient, GetCompScan1472());
773826
}
774827

775828
// As BucketTest1, but with custom bucket selector
@@ -785,6 +838,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
785838
var nConfig := config.config.(search := Some(nSearch));
786839
config := config.(config := nConfig);
787840
var wClient, rClient := SetupTestTable(config, config);
841+
var trans := MakeTrans(config);
842+
788843
for i : nat := 0 to 100 {
789844
var putInput := DDB.PutItemInput(
790845
TableName := TableName,
@@ -795,20 +850,20 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
795850
var q1 := DDB.QueryInput(
796851
TableName := TableName
797852
);
798-
TestBucketQueries(rClient, 5, GetBucketQuery5(), "bucket query 5a", true);
799-
TestBucketQueries(rClient, 4, GetBucketQuery4(), "bucket query 4a", true);
800-
TestBucketQueries(rClient, 3, GetBucketQuery3(), "bucket query 3a", true);
801-
TestBucketQueries(rClient, 2, GetBucketQuery2(), "bucket query 2a", true);
802-
TestBucketQueries(rClient, 1, GetBucketQuery1(), "bucket query 1a", true);
853+
TestBucketQueries(rClient, 5, GetBucketQuery5(), trans, "bucket query 5a", true);
854+
TestBucketQueries(rClient, 4, GetBucketQuery4(), trans, "bucket query 4a", true);
855+
TestBucketQueries(rClient, 3, GetBucketQuery3(), trans, "bucket query 3a", true);
856+
TestBucketQueries(rClient, 2, GetBucketQuery2(), trans, "bucket query 2a", true);
857+
TestBucketQueries(rClient, 1, GetBucketQuery1(), trans, "bucket query 1a", true);
803858

804-
TestBucketQueries(rClient, 5, GetBucketQuery15(), "bucket query 15a", true);
805-
TestBucketQueries(rClient, 5, GetBucketQuery51(), "bucket query 51a", true);
806-
TestBucketQueries(rClient, 5, GetBucketQuery23(), "bucket query 23a", true);
859+
TestBucketQueries(rClient, 5, GetBucketQuery15(), trans, "bucket query 15a", true);
860+
TestBucketQueries(rClient, 5, GetBucketQuery51(), trans, "bucket query 51a", true);
861+
TestBucketQueries(rClient, 5, GetBucketQuery23(), trans, "bucket query 23a", true);
807862

808-
TestBucketQueries(rClient, 1, GetBucketQuery15F(), "bucket query 15Fa", true);
809-
TestBucketQueries(rClient, 2, GetBucketQuery25F(), "bucket query 25Fa", true);
810-
TestBucketQueries(rClient, 3, GetBucketQuery35F(), "bucket query 35Fa", true);
811-
TestBucketQueries(rClient, 4, GetBucketQuery45F(), "bucket query 45Fa", true);
863+
TestBucketQueries(rClient, 1, GetBucketQuery15F(), trans, "bucket query 15Fa", true);
864+
TestBucketQueries(rClient, 2, GetBucketQuery25F(), trans, "bucket query 25Fa", true);
865+
TestBucketQueries(rClient, 3, GetBucketQuery35F(), trans, "bucket query 35Fa", true);
866+
TestBucketQueries(rClient, 4, GetBucketQuery45F(), trans, "bucket query 45Fa", true);
812867

813868
// we don't test scan here, because scan doesn't use ":aws_dbe_bucket"
814869
}
@@ -1230,13 +1285,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
12301285
}
12311286
expect config in largeEncryptionConfigs;
12321287
var tconfig := largeEncryptionConfigs[config];
1233-
var configs := Types.DynamoDbTablesEncryptionConfig (
1234-
tableEncryptionConfigs := map[TableName := tconfig.config]
1235-
);
1236-
// because there are lots of pre-conditions on configs
1237-
assume {:axiom} false;
1238-
var client :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(configs);
1239-
LargeTestsClient(client, config);
1288+
var trans := MakeTrans(tconfig);
1289+
LargeTestsClient(trans, config);
12401290
}
12411291

12421292
method LargeTestsClient(client : Trans.IDynamoDbEncryptionTransformsClient, config : string)

0 commit comments

Comments
 (0)