Skip to content

Commit 425077e

Browse files
ajewellamzajewellamz
committed
m
1 parent 98bd960 commit 425077e

File tree

6 files changed

+1230
-12
lines changed

6 files changed

+1230
-12
lines changed

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ module DynamoToStruct {
7777
&& StructuredToAttr(s[kv.0]).Success?
7878
&& kv.1 == StructuredToAttr(s[kv.0]).value
7979
{
80-
if forall k <- s.Keys :: IsValid_AttributeName(k) then
80+
if forall k <- s :: IsValid_AttributeName(k) then
8181
var structuredData := map k <- s :: k := StructuredToAttr(s[k]);
8282
MapKeysMatchItems(s);
8383
MapError(SimplifyMapValue(structuredData))
@@ -477,7 +477,7 @@ module DynamoToStruct {
477477
// lets Dafny find the correct termination metric.
478478
// See "The Parent Trick" for details: <https://leino.science/papers/krml283.html>.
479479
function method MapAttrToBytes(ghost parent: AttributeValue, m: MapAttributeValue, depth : nat): (ret: Result<seq<uint8>, string>)
480-
requires forall kv <- m.Items :: kv.1 < parent
480+
requires forall k <- m :: m[k] < parent
481481
{
482482
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#value-type
483483
//# Value Type MUST be the [Type ID](#type-id) of the type of [Map Value](#map-value).
@@ -492,7 +492,8 @@ module DynamoToStruct {
492492
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-value
493493
//# A Map MAY hold any DynamoDB Attribute Value data type,
494494
//# and MAY hold values of different types.
495-
var bytesResults := map kv <- m.Items :: kv.0 := AttrToBytes(kv.1, true, depth+1);
495+
var bytesResults := map k <- m :: k := AttrToBytes(m[k], true, depth+1);
496+
496497
var count :- U32ToBigEndian(|m|);
497498
var bytes :- SimplifyMapValue(bytesResults);
498499
var body :- CollectMap(bytes);

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -57,12 +57,23 @@ module StructuredEncryptionHeader {
5757
type Legend = x : seq<LegendByte> | |x| < UINT16_LIMIT
5858
type CMPUtf8Bytes = x : CMP.Utf8Bytes | |x| < UINT16_LIMIT
5959

60-
predicate method IsVersion2Schema(data : CanonCryptoList)
61-
{
62-
exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
60+
predicate method {:tailrecursion} IsVersion2Schema(data : CanonCryptoList, pos : uint32 := 0) : (ret : bool)
61+
requires |data| < UINT32_LIMIT
62+
requires pos <= |data| as uint32
63+
requires forall i | 0 <= i < pos :: data[i].action != SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
64+
decreases |data| as uint32 - pos
65+
ensures ret ==> (exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT)
66+
{
67+
if pos == |data| as uint32 then
68+
false
69+
else if data[pos].action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT then
70+
true
71+
else
72+
IsVersion2Schema(data, pos+1)
6373
}
6474

6575
function method VersionFromSchema(data : CanonCryptoList) : (ret : Version)
76+
requires |data| < UINT32_LIMIT
6677
ensures (exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT) <==> (ret == 2)
6778
ensures !(exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT) <==> (ret == 1)
6879
{
@@ -229,8 +240,9 @@ module StructuredEncryptionHeader {
229240
//# If any [Crypto Action](./structures.md#crypto-action) is configured as
230241
//# [SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT Crypto Action](./structures.md#sign_and_include_in_encryption_context)
231242
//# the Version MUST be 0x02; otherwise, Version MUST be 0x01.
232-
ensures ret.Success? ==> ret.value.version == VersionFromSchema(schema)
243+
ensures ret.Success? ==> |schema| < UINT32_LIMIT && ret.value.version == VersionFromSchema(schema)
233244
{
245+
:- Need(|schema| < UINT32_LIMIT, E("Unexpected large schema"));
234246
:- Need(ValidEncryptionContext(mat.encryptionContext), E("Invalid Encryption Context"));
235247
:- Need(0 < |mat.encryptedDataKeys|, E("There must be at least one data key"));
236248
:- Need(|mat.encryptedDataKeys| < UINT8_LIMIT, E("Too many data keys."));

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ module WrappedDDBEncryptionMain {
6161
config :- expect AddJson(config, "data.json", keyVectors);
6262
config :- expect AddJson(config, "iotest.json", keyVectors);
6363
config :- expect AddJson(config, "PermTest.json", keyVectors);
64+
config :- expect AddJson(config, "large_records.json", keyVectors);
6465
config.RunAllTests(keyVectors);
6566
}
6667
}

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

Lines changed: 46 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -46,9 +46,15 @@ module {:options "-functionSyntax:4"} JsonConfig {
4646
item : DDB.AttributeMap
4747
)
4848

49+
datatype LargeRecord = LargeRecord (
50+
name : string,
51+
count : nat,
52+
item : DDB.AttributeMap
53+
)
54+
4955
datatype TableConfig = TableConfig (
5056
name : ConfigName,
51-
config : Types.DynamoDbTableEncryptionConfig,
57+
config : AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTableEncryptionConfig,
5258
vanilla : bool
5359
)
5460

@@ -1410,7 +1416,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
14101416
return Success(results);
14111417
}
14121418

1413-
14141419
method GetRecord(data : JSON) returns (output : Result<Record, string>)
14151420
{
14161421
var item :- JsonToDdbItem(data);
@@ -1424,4 +1429,43 @@ module {:options "-functionSyntax:4"} JsonConfig {
14241429
var num :- StrToNat(hash.N);
14251430
return Success(Record(num, item));
14261431
}
1432+
1433+
method GetLarge(name : string, data : JSON) returns (output : Result<LargeRecord, string>)
1434+
{
1435+
:- Need(data.Object?, "LargeRecord must be a JSON object.");
1436+
var count := 0;
1437+
var item : DDB.AttributeMap := map[];
1438+
for i := 0 to |data.obj| {
1439+
var obj := data.obj[i];
1440+
match obj.0 {
1441+
case "Count" =>
1442+
:- Need(obj.1.Number?, "GetPrefix length must be a number");
1443+
count :- DecimalToInt(obj.1.num);
1444+
case "Item" => var src :- JsonToDdbItem(obj.1); item := src;
1445+
case _ => return Failure("Unexpected part of a LargeRecord : '" + obj.0 + "'");
1446+
}
1447+
}
1448+
if (count <= 0) {
1449+
return Failure("Missing or invalid Count in LargeRecord : '" + name + "'");
1450+
}
1451+
if (|item| == 0) {
1452+
return Failure("Missing or Empty LargeRecord : '" + name + "'");
1453+
}
1454+
var record := LargeRecord(name, count, item);
1455+
return Success(record);
1456+
}
1457+
1458+
method GetLarges(data : JSON) returns (output : Result<seq<LargeRecord>, string>)
1459+
{
1460+
:- Need(data.Object?, "Larges must be a JSON object.");
1461+
var results : seq<LargeRecord> := [];
1462+
for i := 0 to |data.obj| {
1463+
var obj := data.obj[i];
1464+
var record :- GetLarge(obj.0, obj.1);
1465+
results := results + [record];
1466+
}
1467+
return Success(results);
1468+
}
1469+
1470+
14271471
}

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

Lines changed: 95 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
4141
import MPT = AwsCryptographyMaterialProvidersTypes
4242
import Primitives = AtomicPrimitives
4343
import ParseJsonManifests
44+
import Time
45+
import Trans = AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
46+
import TransOp = AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations
47+
import DdbMiddlewareConfig
48+
import DynamoDbEncryptionTransforms
4449

4550

4651
datatype TestVectorConfig = TestVectorConfig (
@@ -58,7 +63,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
5863
writeTests : seq<WriteTest>,
5964
roundTripTests : seq<RoundTripTest>,
6065
decryptTests : seq<DecryptTest>,
61-
strings : seq<string>
66+
strings : seq<string>,
67+
large : seq<LargeRecord>
6268
) {
6369

6470
method RunAllTests(keyVectors: KeyVectors.KeyVectorsClient)
@@ -78,6 +84,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
7884
print |configsForIoTest|, " configsForIoTest.\n";
7985
print |configsForModTest|, " configsForModTest.\n";
8086
print |strings|, " strings.\n";
87+
print |large|, " large.\n";
8188
if |roundTripTests| != 0 {
8289
print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n";
8390
}
@@ -107,6 +114,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
107114
return;
108115
}
109116
StringOrdering();
117+
LargeTests();
110118
BasicIoTest();
111119
RunIoTests();
112120
BasicQueryTest();
@@ -484,6 +492,87 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
484492
}
485493
}
486494

495+
const TestConfigs : set<string> := {"all"}
496+
const TestRecords : set<string> := {"all"}
497+
498+
predicate DoTestConfig(name : string)
499+
{
500+
"all" in TestConfigs || name in TestConfigs
501+
}
502+
503+
predicate DoTestRecord(name : string)
504+
{
505+
"all" in TestRecords || name in TestRecords
506+
}
507+
508+
method LargeTests()
509+
{
510+
print "LargeTests\n";
511+
DoLargeTest("do_nothing");
512+
DoLargeTest("do_nothing_nosign");
513+
DoLargeTest("full_encrypt");
514+
DoLargeTest("full_encrypt_nosign");
515+
DoLargeTest("full_sign");
516+
DoLargeTest("full_sign_nosign");
517+
}
518+
519+
method DoLargeTest(config : string)
520+
{
521+
if !DoTestConfig(config) {
522+
return;
523+
}
524+
expect config in tableEncryptionConfigs;
525+
var tconfig := tableEncryptionConfigs[config];
526+
var configs := Types.DynamoDbTablesEncryptionConfig (
527+
tableEncryptionConfigs := map[TableName := tconfig.config]
528+
);
529+
// because there are lots of pre-conditions on configs
530+
assume {:axiom} false;
531+
var client :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(configs);
532+
LargeTestsClient(client, config);
533+
}
534+
535+
method LargeTestsClient(client : Trans.IDynamoDbEncryptionTransformsClient, config : string)
536+
requires client.ValidState()
537+
ensures client.ValidState()
538+
modifies client.Modifies
539+
{
540+
for i := 0 to |large| {
541+
RunLargeTest(large[i], client, config);
542+
}
543+
}
544+
545+
method RunLargeTest(record : LargeRecord, client : Trans.IDynamoDbEncryptionTransformsClient, config : string)
546+
requires client.ValidState()
547+
ensures client.ValidState()
548+
modifies client.Modifies
549+
{
550+
if !DoTestRecord(record.name) {
551+
return;
552+
}
553+
554+
var time := Time.GetAbsoluteTime();
555+
for i := 0 to record.count {
556+
var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item));
557+
var put_input_output :- expect client.PutItemInputTransform(put_input_input);
558+
}
559+
var elapsed := Time.TimeSince(time);
560+
Time.PrintTimeLong(elapsed, "Large Encrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config);
561+
562+
var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item));
563+
var put_input_output :- expect client.PutItemInputTransform(put_input_input);
564+
time := Time.GetAbsoluteTime();
565+
for i := 0 to record.count {
566+
var orig_get_input := DDB.GetItemInput(TableName := TableName, Key := map[]);
567+
var get_output := DDB.GetItemOutput(Item := Some(put_input_output.transformedInput.Item));
568+
var trans_get_input := Trans.GetItemOutputTransformInput(sdkOutput := get_output, originalInput := orig_get_input);
569+
var put_output :- expect client.GetItemOutputTransform(trans_get_input);
570+
571+
}
572+
elapsed := Time.TimeSince(time);
573+
Time.PrintTimeLong(elapsed, "Large Decrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config);
574+
}
575+
487576
method RoundTripTests()
488577
{
489578
print "RoundTripTests\n";
@@ -999,7 +1088,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
9991088

10001089
function MakeEmptyTestVector() : TestVectorConfig
10011090
{
1002-
TestVectorConfig(MakeCreateTableInput(), [], map[], [], map[], map[], [], [], [], [], [], [], [], [], [])
1091+
TestVectorConfig(MakeCreateTableInput(), [], map[], [], map[], map[], [], [], [], [], [], [], [], [], [], [])
10031092
}
10041093

10051094
method ParseTestVector(data : JSON, prev : TestVectorConfig, keyVectors: KeyVectors.KeyVectorsClient)
@@ -1024,6 +1113,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10241113
var roundTripTests : seq<RoundTripTest> := [];
10251114
var decryptTests : seq<DecryptTest> := [];
10261115
var strings : seq<string> := [];
1116+
var large : seq<LargeRecord> := [];
10271117

10281118
for i := 0 to |data.obj| {
10291119
match data.obj[i].0 {
@@ -1042,6 +1132,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10421132
case "RoundTripTest" => roundTripTests :- GetRoundTripTests(data.obj[i].1, keyVectors);
10431133
case "DecryptTests" => decryptTests :- GetDecryptTests(data.obj[i].1, keyVectors);
10441134
case "Strings" => strings :- GetStrings(data.obj[i].1);
1135+
case "Large" => large :- GetLarges(data.obj[i].1);
10451136
case _ => return Failure("Unexpected top level tag " + data.obj[i].0);
10461137
}
10471138
}
@@ -1063,7 +1154,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10631154
writeTests := prev.writeTests + writeTests,
10641155
roundTripTests := prev.roundTripTests + roundTripTests,
10651156
decryptTests := prev.decryptTests + decryptTests,
1066-
strings := prev.strings + strings
1157+
strings := prev.strings + strings,
1158+
large := prev.large + large
10671159
)
10681160
);
10691161
}

0 commit comments

Comments
 (0)