Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit dbbd44d

Browse files
ajewellamzajewellamz
committedApr 25, 2025··
m
1 parent 97d853e commit dbbd44d

File tree

5 files changed

+81
-84
lines changed

5 files changed

+81
-84
lines changed
 

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

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,12 @@ module DynamoToStruct {
2525

2626
type TerminalDataMap = map<AttributeName, StructuredDataTerminal>
2727

28+
// This file exists for ItemToStructured and StructuredToItem and their variants,
29+
// which provide conversion between an AttributeMap and a StructuredDataMap
30+
2831

32+
// Identical to ItemToStructured, except that the result does not include any attributes configured as DO_NOTHING\
33+
// Such attributes are unneeded, as they do not partake in signing nor encryption
2934
function method ItemToStructured2(item : AttributeMap, actions : Types.AttributeActions) : (ret : Result<TerminalDataMap, Error>)
3035
{
3136
// var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();
@@ -36,6 +41,9 @@ module DynamoToStruct {
3641
MapError(SimplifyMapValue(structuredMap))
3742
}
3843

44+
// Identical to StructuredToItem, except that any non encrypted fields in the original are passed through unchanged
45+
// and only encrypted fields are run through StructuredToAttr
46+
// This one is used for encryption, and so anything in s but not in orig is also kept
3947
function method StructuredToItemEncrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
4048
{
4149
var ddbMap := map k <- orig :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]);
@@ -49,16 +57,16 @@ module DynamoToStruct {
4957
Success(oldMap + newMap)
5058
}
5159

60+
// Identical to StructuredToItem, except that any non encrypted fields in the original are passed through unchanged
61+
// and only encrypted fields are run through StructuredToAttr\
62+
// This one is used for decryption, and so anything in s but not in orig is ignored
5263
function method StructuredToItemDecrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
5364
{
5465
var ddbMap := map k <- orig | !(ReservedPrefix <= k) :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]);
5566
MapKeysMatchItems(orig);
5667
MapError(SimplifyMapValue(ddbMap))
5768
}
5869

59-
// This file exists for these two functions : ItemToStructured and StructuredToItem
60-
// which provide conversion between an AttributeMap and a StructuredDataMap
61-
6270
// Convert AttributeMap to StructuredDataMap
6371
function method {:opaque} ItemToStructured(item : AttributeMap) : (ret : Result<TerminalDataMap, Error>)
6472

@@ -146,6 +154,7 @@ module DynamoToStruct {
146154
Success(SeqPosToUInt32(x, pos))
147155
}
148156

157+
// This is safe because are dealing with DynamoDB items, and so no numbers wil exceed 400K
149158
function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32)
150159
ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64
151160
ensures ret == x + y
@@ -155,6 +164,7 @@ module DynamoToStruct {
155164
value as uint32
156165
}
157166

167+
// This is safe because are dealing with DynamoDB items, and so no numbers will exceed 400K
158168
function method {:opaque} Add32_3(x : uint32, y : uint32, z : uint32) : (ret : uint32)
159169
ensures x as uint64 + y as uint64 + z as uint64 <= UINT32_MAX as uint64
160170
ensures ret == x + y + z

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -111,12 +111,12 @@ module {:options "-functionSyntax:4"} DecryptManifest {
111111
}
112112
}
113113

114-
function LogFileName() : string
114+
function LogFileName() : Option<string>
115115
{
116-
if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then
117-
"..\\..\\PerfLog.txt"
118-
else
119-
"../../PerfLog.txt"
116+
// if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then
117+
// "..\\..\\PerfLog.txt"
118+
// else
119+
Some("../../PerfLog.txt")
120120
}
121121

122122
method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient)
@@ -182,7 +182,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
182182
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
183183
var _ :- OneTest(obj.0, obj.1, keyVectors);
184184
}
185-
Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, Some(LogFileName()));
185+
Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, LogFileName());
186186

187187
timeStamp :- expect Time.GetCurrentTimeStamp();
188188
print timeStamp + " Tests Complete.\n";

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

Lines changed: 1 addition & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
4848

4949
datatype LargeRecord = LargeRecord (
5050
name : string,
51-
count : nat,
5251
item : DDB.AttributeMap
5352
)
5453

@@ -1433,25 +1432,18 @@ module {:options "-functionSyntax:4"} JsonConfig {
14331432
method GetLarge(name : string, data : JSON) returns (output : Result<LargeRecord, string>)
14341433
{
14351434
:- Need(data.Object?, "LargeRecord must be a JSON object.");
1436-
var count := 0;
14371435
var item : DDB.AttributeMap := map[];
14381436
for i := 0 to |data.obj| {
14391437
var obj := data.obj[i];
14401438
match obj.0 {
1441-
case "Count" =>
1442-
:- Need(obj.1.Number?, "GetPrefix length must be a number");
1443-
count :- DecimalToInt(obj.1.num);
14441439
case "Item" => var src :- JsonToDdbItem(obj.1); item := src;
14451440
case _ => return Failure("Unexpected part of a LargeRecord : '" + obj.0 + "'");
14461441
}
14471442
}
1448-
if (count <= 0) {
1449-
return Failure("Missing or invalid Count in LargeRecord : '" + name + "'");
1450-
}
14511443
if (|item| == 0) {
14521444
return Failure("Missing or Empty LargeRecord : '" + name + "'");
14531445
}
1454-
var record := LargeRecord(name, count, item);
1446+
var record := LargeRecord(name, item);
14551447
return Success(record);
14561448
}
14571449

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

Lines changed: 61 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
1313
import opened Wrappers
1414
import opened StandardLibrary
1515
import opened StandardLibrary.UInt
16-
import opened StandardLibrary.String
1716
import JSON.API
1817
import opened JSON.Values
1918
import JSON.Errors
@@ -46,7 +45,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
4645
import TransOp = AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations
4746
import DdbMiddlewareConfig
4847
import DynamoDbEncryptionTransforms
48+
import OsLang
4949

50+
const PerfIterations : uint32 := 1000
5051

5152
datatype TestVectorConfig = TestVectorConfig (
5253
schemaOnEncrypt : DDB.CreateTableInput,
@@ -73,60 +74,60 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
7374
modifies keyVectors.Modifies
7475
ensures keyVectors.ValidState()
7576
{
76-
print "DBE Test Vectors\n";
77-
print |globalRecords|, " records.\n";
78-
print |tableEncryptionConfigs|, " tableEncryptionConfigs.\n";
79-
print |largeEncryptionConfigs|, " largeEncryptionConfigs.\n";
80-
print |queries|, " queries.\n";
81-
print |names|, " names.\n";
82-
print |values|, " values.\n";
83-
print |failingQueries|, " failingQueries.\n";
84-
print |complexTests|, " complexTests.\n";
85-
print |ioTests|, " ioTests.\n";
86-
print |configsForIoTest|, " configsForIoTest.\n";
87-
print |configsForModTest|, " configsForModTest.\n";
88-
print |strings|, " strings.\n";
89-
print |large|, " large.\n";
90-
if |roundTripTests| != 0 {
91-
print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n";
92-
}
93-
if |roundTripTests| > 1 {
94-
print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n";
95-
}
96-
97-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
98-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
99-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
100-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
101-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
102-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
103-
var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
104-
var _ :- expect WriteManifest.Write("encrypt.json");
105-
var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
106-
var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
107-
if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
108-
print "\nRunning no tests\n";
109-
return;
110-
}
111-
Validate();
112-
// Because of Dafny-Rust's lack of modules, there is no way to mae an interceptor for the wrapped DB-ESDK client.
113-
// So we create runtimes/rust/SkipLocal.txt to skip those tests that need the wrapped client.
114-
var skipLocal := FileIO.ReadBytesFromFile("SkipLocal.txt");
115-
if skipLocal.Success? {
116-
return;
117-
}
118-
StringOrdering();
77+
// print "DBE Test Vectors\n";
78+
// print |globalRecords|, " records.\n";
79+
// print |tableEncryptionConfigs|, " tableEncryptionConfigs.\n";
80+
// print |largeEncryptionConfigs|, " largeEncryptionConfigs.\n";
81+
// print |queries|, " queries.\n";
82+
// print |names|, " names.\n";
83+
// print |values|, " values.\n";
84+
// print |failingQueries|, " failingQueries.\n";
85+
// print |complexTests|, " complexTests.\n";
86+
// print |ioTests|, " ioTests.\n";
87+
// print |configsForIoTest|, " configsForIoTest.\n";
88+
// print |configsForModTest|, " configsForModTest.\n";
89+
// print |strings|, " strings.\n";
90+
// print |large|, " large.\n";
91+
// if |roundTripTests| != 0 {
92+
// print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n";
93+
// }
94+
// if |roundTripTests| > 1 {
95+
// print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n";
96+
// }
97+
98+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
99+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
100+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
101+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
102+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
103+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
104+
// var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
105+
// var _ :- expect WriteManifest.Write("encrypt.json");
106+
// var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
107+
// var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
108+
// if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
109+
// print "\nRunning no tests\n";
110+
// return;
111+
// }
112+
// Validate();
113+
// // Because of Dafny-Rust's lack of modules, there is no way to make an interceptor for the wrapped DB-ESDK client.
114+
// // So we create runtimes/rust/SkipLocal.txt to skip those tests that need the wrapped client.
115+
// var skipLocal := FileIO.ReadBytesFromFile("SkipLocal.txt");
116+
// if skipLocal.Success? {
117+
// return;
118+
// }
119+
// StringOrdering();
119120
LargeTests();
120-
BasicIoTest();
121-
RunIoTests();
122-
BasicQueryTest();
123-
ConfigModTest();
124-
ComplexTests();
125-
WriteTests();
126-
RoundTripTests();
127-
DecryptTests();
128-
var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
129-
DeleteTable(client);
121+
// BasicIoTest();
122+
// RunIoTests();
123+
// BasicQueryTest();
124+
// ConfigModTest();
125+
// ComplexTests();
126+
// WriteTests();
127+
// RoundTripTests();
128+
// DecryptTests();
129+
// var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
130+
// DeleteTable(client);
130131
}
131132

132133
function NewOrderRecord(i : nat, str : string) : Record
@@ -494,8 +495,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
494495
}
495496
}
496497

497-
const TestConfigs : set<string> := {"all"}
498-
const TestRecords : set<string> := {"all"}
498+
const TestConfigs : set<string> := {"full_sign_nosign"}
499+
const TestRecords : set<string> := {"flat"}
499500

500501
predicate DoTestConfig(name : string)
501502
{
@@ -554,25 +555,23 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
554555
}
555556

556557
var time := Time.GetAbsoluteTime();
557-
for i := 0 to record.count {
558+
for i : uint32 := 0 to PerfIterations {
558559
var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item));
559560
var put_input_output :- expect client.PutItemInputTransform(put_input_input);
560561
}
561-
var elapsed := Time.TimeSince(time);
562-
Time.PrintTimeLong(elapsed, "Large Encrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config);
562+
Time.PrintTimeSinceLong(time, "Large Encrypt " + record.name + config, DecryptManifest.LogFileName());
563563

564564
var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item));
565565
var put_input_output :- expect client.PutItemInputTransform(put_input_input);
566566
time := Time.GetAbsoluteTime();
567-
for i := 0 to record.count {
567+
for i : uint32 := 0 to PerfIterations {
568568
var orig_get_input := DDB.GetItemInput(TableName := TableName, Key := map[]);
569569
var get_output := DDB.GetItemOutput(Item := Some(put_input_output.transformedInput.Item));
570570
var trans_get_input := Trans.GetItemOutputTransformInput(sdkOutput := get_output, originalInput := orig_get_input);
571571
var put_output :- expect client.GetItemOutputTransform(trans_get_input);
572572

573573
}
574-
elapsed := Time.TimeSince(time);
575-
Time.PrintTimeLong(elapsed, "Large Decrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config);
574+
Time.PrintTimeSinceLong(time, "Large Decrypt " + record.name + config, DecryptManifest.LogFileName());
576575
}
577576

578577
method RoundTripTests()

‎TestVectors/runtimes/java/large_records.json

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -846,14 +846,12 @@
846846
},
847847
"Large": {
848848
"tiny": {
849-
"Count": 1000,
850849
"Item": {
851850
"PK": "012345678900123456789001234567890",
852851
"00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"
853852
}
854853
},
855854
"flat": {
856-
"Count": 1000,
857855
"Item": {
858856
"PK": "012345678900123456789001234567890",
859857
"00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
@@ -957,7 +955,6 @@
957955
}
958956
},
959957
"nested_map": {
960-
"Count": 1000,
961958
"Item": {
962959
"PK": "012345678900123456789001234567890",
963960
"00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": {
@@ -1065,7 +1062,6 @@
10651062
}
10661063
},
10671064
"nested_list": {
1068-
"Count": 1000,
10691065
"Item": {
10701066
"PK": "012345678900123456789001234567890",
10711067
"00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": {

0 commit comments

Comments
 (0)
Please sign in to comment.