Skip to content

Commit bbebafc

Browse files
ajewellamzajewellamz
committed
m
1 parent 07fa45c commit bbebafc

File tree

10 files changed

+319
-187
lines changed

10 files changed

+319
-187
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

+15-9
Original file line numberDiff line numberDiff line change
@@ -58,13 +58,19 @@ module
5858
requires tableName in config.tableEncryptionConfigs
5959
ensures SearchModifies(config, tableName) <= TheModifies(config)
6060

61-
function method {:tailrecursion} AddSignedBeaconActions(names : seq<string>, actions : ET.AttributeActions) : ET.AttributeActions
61+
function method {:tailrecursion} AddSignedBeaconActions(
62+
names : seq<string>,
63+
actions : ET.AttributeActions,
64+
pos : nat := 0
65+
) : ET.AttributeActions
6266
requires forall k <- names :: DDB.IsValid_AttributeName(k)
67+
requires pos <= |names|
68+
decreases |names| - pos
6369
{
64-
if |names| == 0 then
70+
if |names| == pos then
6571
actions
6672
else
67-
AddSignedBeaconActions(names[1..], actions[names[0] := SET.SIGN_ONLY])
73+
AddSignedBeaconActions(names, actions[names[0] := SET.SIGN_ONLY], pos+1)
6874
}
6975

7076
predicate method IsConfigured(config : AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTableEncryptionConfig, name : string)
@@ -79,11 +85,11 @@ module
7985
{
8086
forall tableName <- configs :: ValidTableConfig?(configs[tableName])
8187
}
82-
predicate {:opaque} CorrectlyTransferedStructure?(
88+
predicate {:opaque} CorrectlyTransferredStructure?(
8389
internalConfigs: map<string, DdbMiddlewareConfig.ValidTableConfig>,
8490
config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig
8591
)
86-
ensures 0 == |internalConfigs| ==> CorrectlyTransferedStructure?(internalConfigs, config)
92+
ensures 0 == |internalConfigs| ==> CorrectlyTransferredStructure?(internalConfigs, config)
8793
{
8894
forall tableName <- internalConfigs
8995
::
@@ -142,7 +148,7 @@ module
142148
invariant forall k <- m' :: m'[k] == config.tableEncryptionConfigs[k]
143149
invariant forall internalConfig <- internalConfigs.Values :: internalConfig.logicalTableName in allLogicalTableNames
144150

145-
invariant CorrectlyTransferedStructure?(internalConfigs, config)
151+
invariant CorrectlyTransferredStructure?(internalConfigs, config)
146152
invariant AllTableConfigsValid?(internalConfigs)
147153
invariant ValidConfig?(Config(internalConfigs))
148154

@@ -223,10 +229,10 @@ module
223229
assert internalConfig.physicalTableName == tableName;
224230
}
225231

226-
assert CorrectlyTransferedStructure?(internalConfigs, config) by {
227-
reveal CorrectlyTransferedStructure?();
232+
assert CorrectlyTransferredStructure?(internalConfigs, config) by {
233+
reveal CorrectlyTransferredStructure?();
228234
reveal ConfigsMatch();
229-
assert CorrectlyTransferedStructure?(internalConfigs - {tableName}, config);
235+
assert CorrectlyTransferredStructure?(internalConfigs - {tableName}, config);
230236
assert ConfigsMatch(tableName, internalConfig, inputConfig);
231237
}
232238

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy

+12-7
Original file line numberDiff line numberDiff line change
@@ -191,25 +191,30 @@ module DynamoDbItemEncryptorUtil {
191191
keys : seq<UTF8.ValidUTF8Bytes>,
192192
context : MPL.EncryptionContext,
193193
legend : string,
194+
keyPos : nat := 0,
195+
legendPos : nat := 0,
194196
attrMap : DDB.AttributeMap := map[]
195197
)
196198
: Result<DDB.AttributeMap, string>
197199
requires forall k <- keys :: k in context
200+
requires keyPos <= |keys|
201+
requires legendPos <= |legend|
202+
decreases |keys| - keyPos
198203
{
199-
if |keys| == 0 then
200-
if |legend| == 0 then
204+
if |keys| == keyPos then
205+
if |legend| == legendPos then
201206
Success(attrMap)
202207
else
203208
Failure("Encryption Context Legend is too long.")
204209
else
205-
var key : UTF8.ValidUTF8Bytes := keys[0];
210+
var key : UTF8.ValidUTF8Bytes := keys[keyPos];
206211
if SE.EC_ATTR_PREFIX < key then
207-
:- Need(0 < |legend|, "Encryption Context Legend is too short.");
212+
:- Need(legendPos < |legend|, "Encryption Context Legend is too short.");
208213
var attrName :- GetAttributeName(key);
209-
var attrValue :- GetAttrValue(context[key], legend[0]);
210-
GetV2AttrMap(keys[1..], context, legend[1..], attrMap[attrName := attrValue])
214+
var attrValue :- GetAttrValue(context[key], legend[legendPos]);
215+
GetV2AttrMap(keys, context, legend, keyPos+1, legendPos+1, attrMap[attrName := attrValue])
211216
else
212-
GetV2AttrMap(keys[1..], context, legend, attrMap)
217+
GetV2AttrMap(keys, context, legend, keyPos+1, legendPos, attrMap)
213218
}
214219

215220
function method GetAttributeName(ddbAttrKey: UTF8.ValidUTF8Bytes)

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

+93-41
Original file line numberDiff line numberDiff line change
@@ -114,16 +114,16 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
114114
function method {:opaque} GetBinary(data : AuthList, path : Path): (result: Result<StructuredDataTerminal, Error>)
115115
ensures result.Success? ==> exists x :: x in data && x.key == path
116116
{
117-
var data := FindAuth(data, path);
117+
var pos := FindAuth(data, path);
118118

119-
if data.None? then
119+
if pos.None? then
120120
Failure(E("The field name " + Paths.PathToString(path) + " is required."))
121-
else if data.value.data.typeId != BYTES_TYPE_ID then
121+
else if data[pos.value].data.typeId != BYTES_TYPE_ID then
122122
Failure(E(Paths.PathToString(path) + " must be a binary Terminal."))
123-
else if data.value.action != DO_NOT_SIGN then
123+
else if data[pos.value].action != DO_NOT_SIGN then
124124
Failure(E(Paths.PathToString(path) + " must be DO_NOT_SIGN."))
125125
else
126-
Success(data.value.data)
126+
Success(data[pos.value].data)
127127
}
128128

129129
// Return the sum of the sizes of the given fields
@@ -269,35 +269,84 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
269269
output := GetV2EncryptionContext2(contextAttrs);
270270
}
271271

272-
function method {:opaque} Find(haystack : CryptoList, needle : Path) : Result<CryptoItem, Error>
272+
function {:opaque} Find(haystack : CryptoList, needle : Path, start : nat := 0) : (res : Result<nat, Error>)
273+
requires start <= |haystack|
274+
requires forall i | 0 <= i < start :: haystack[i].key != needle
275+
ensures (exists x <- haystack :: x.key == needle) <==> res.Success?
276+
ensures (forall x <- haystack :: x.key != needle) <==> res.Failure?
277+
ensures (forall x <- haystack :: x.key != needle) <==> res == Failure(E("Not Found"))
278+
ensures res.Success? ==>
279+
&& 0 <= res.value < |haystack|
280+
&& haystack[res.value].key == needle
281+
&& (forall i | 0 <= i < res.value :: haystack[i].key != needle)
282+
decreases |haystack| - start
273283
{
274-
if |haystack| == 0 then
284+
if |haystack| == start then
275285
Failure(E("Not Found"))
276-
else if haystack[0].key == needle
277-
then Success(haystack[0])
286+
else if haystack[start].key == needle then
287+
Success(start)
278288
else
279-
Find(haystack[1..], needle)
289+
Find(haystack, needle, start + 1)
290+
}
291+
by method {
292+
for i := 0 to |haystack|
293+
invariant forall x <- haystack[..i] :: x.key != needle
294+
{
295+
if haystack[i].key == needle {
296+
return Success(i);
297+
}
298+
}
299+
return Failure(E("Not Found"));
280300
}
281301

282-
function method {:opaque} FindAuth(haystack : AuthList, needle : Path) : (result : Option<AuthItem>)
283-
ensures result.Some? ==> exists x :: x in haystack && x.key == needle
302+
function {:opaque} FindAuth(haystack : AuthList, needle : Path, start : nat := 0) : (res : Option<nat>)
303+
requires start <= |haystack|
304+
requires forall i | 0 <= i < start :: haystack[i].key != needle
305+
ensures (exists x <- haystack :: x.key == needle) <==> res.Some?
306+
ensures (forall x <- haystack :: x.key != needle) <==> res == None
307+
ensures res.Some? ==>
308+
&& 0 <= res.value < |haystack|
309+
&& haystack[res.value].key == needle
310+
&& (forall i | 0 <= i < res.value :: haystack[i].key != needle)
311+
decreases |haystack| - start
284312
{
285-
if |haystack| == 0 then
313+
if |haystack| == start then
286314
None
287-
else if haystack[0].key == needle
288-
then Some(haystack[0])
315+
else if haystack[start].key == needle then
316+
Some(start)
289317
else
290-
FindAuth(haystack[1..], needle)
318+
FindAuth(haystack, needle, start + 1)
319+
}
320+
by method {
321+
for i := 0 to |haystack|
322+
invariant forall x <- haystack[..i] :: x.key != needle
323+
{
324+
if haystack[i].key == needle {
325+
return Some(i);
326+
}
327+
}
328+
return None;
291329
}
292330

293-
function method {:opaque} CountEncrypted(list : CanonCryptoList) : nat
331+
function {:opaque} CountEncrypted(list : CanonCryptoList) : nat
294332
{
295333
if |list| == 0 then
296334
0
297335
else if list[0].action == ENCRYPT_AND_SIGN then
298336
1 + CountEncrypted(list[1..])
299337
else
300338
CountEncrypted(list[1..])
339+
} by method {
340+
reveal CountEncrypted();
341+
var result : nat := 0;
342+
for i := |list| downto 0
343+
invariant result == CountEncrypted(list[i..])
344+
{
345+
if list[i].action == ENCRYPT_AND_SIGN {
346+
result := result + 1;
347+
}
348+
}
349+
return result;
301350
}
302351

303352
method {:vcs_split_on_every_assert} GetV2EncryptionContext2(fields : CryptoList)
@@ -355,7 +404,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
355404
var fieldUtf8 := keys[i];
356405
var fieldStr := fieldMap[fieldUtf8];
357406
var item :- Find(fields, fieldMap[fieldUtf8]);
358-
var attr : StructuredDataTerminal := item.data;
407+
var attr : StructuredDataTerminal := fields[item].data;
359408
var attrStr : ValidUTF8Bytes;
360409
var legendChar : char;
361410
if attr.typeId == NULL {
@@ -395,34 +444,33 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
395444
keys : seq<string>,
396445
plaintextStructure: StructuredDataMap,
397446
cryptoSchema: CryptoSchemaMap,
398-
ghost origKeys : seq<string> := keys,
447+
pos : nat := 0,
399448
acc : CryptoList := []
400449
)
401450
: (ret : Result<CryptoList, Error>)
451+
requires 0 <= pos <= |keys|
452+
requires |acc| == pos
402453
requires forall k <- keys :: k in plaintextStructure
403454
requires forall k <- keys :: k in cryptoSchema
404455
requires forall k <- acc :: |k.key| == 1
405-
requires CryptoListHasNoDuplicates(acc)
406-
requires |acc| + |keys| == |origKeys|
407-
requires keys == origKeys[|acc|..]
408-
requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(origKeys[i])
456+
requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(keys[i])
409457
requires Seq.HasNoDuplicates(keys)
410-
requires Seq.HasNoDuplicates(origKeys)
458+
decreases |keys| - pos
411459

412460
ensures ret.Success? ==>
413461
&& (forall k <- ret.value :: |k.key| == 1)
414462
&& CryptoListHasNoDuplicates(ret.value)
415463
{
416464
reveal Seq.HasNoDuplicates();
417465
Paths.StringToUniPathUnique();
418-
if |keys| == 0 then
466+
if |keys| == pos then
419467
Success(acc)
420468
else
421-
var key := keys[0];
469+
var key := keys[pos];
422470
var path := Paths.StringToUniPath(key);
423471
var item := CryptoItem(key := path, data := plaintextStructure[key], action := cryptoSchema[key]);
424472
var newAcc := acc + [item];
425-
BuildCryptoMap2(keys[1..], plaintextStructure, cryptoSchema, origKeys, newAcc)
473+
BuildCryptoMap2(keys, plaintextStructure, cryptoSchema, pos+1, newAcc)
426474
}
427475

428476
function method BuildCryptoMap(plaintextStructure: StructuredDataMap, cryptoSchema: CryptoSchemaMap) :
@@ -440,33 +488,33 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
440488
keys : seq<string>,
441489
plaintextStructure: StructuredDataMap,
442490
authSchema: AuthenticateSchemaMap,
443-
ghost origKeys : seq<string> := keys,
491+
pos : nat := 0,
444492
acc : AuthList := []
445493
)
446494
: (ret : Result<AuthList, Error>)
495+
requires 0 <= pos <= |keys|
496+
requires |acc| == pos
447497
requires forall k <- keys :: k in plaintextStructure
448498
requires forall k <- keys :: k in authSchema
449499
requires forall k <- acc :: |k.key| == 1
500+
requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(keys[i])
450501
requires AuthListHasNoDuplicates(acc)
451-
requires |acc| + |keys| == |origKeys|
452-
requires keys == origKeys[|acc|..]
453-
requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(origKeys[i])
454502
requires Seq.HasNoDuplicates(keys)
455-
requires Seq.HasNoDuplicates(origKeys)
503+
decreases |keys| - pos
456504

457505
ensures ret.Success? ==>
458506
&& (forall k <- ret.value :: |k.key| == 1)
459507
&& AuthListHasNoDuplicates(ret.value)
460508
{
461509
reveal Seq.HasNoDuplicates();
462-
if |keys| == 0 then
510+
if |keys| == pos then
463511
Success(acc)
464512
else
465-
var key := keys[0];
513+
var key := keys[pos];
466514
var path := Paths.StringToUniPath(key);
467515
var item := AuthItem(key := path, data := plaintextStructure[key], action := authSchema[key]);
468516
var newAcc := acc + [item];
469-
BuildAuthMap2(keys[1..], plaintextStructure, authSchema, origKeys, newAcc)
517+
BuildAuthMap2(keys, plaintextStructure, authSchema, pos+1, newAcc)
470518
}
471519

472520
function method BuildAuthMap(plaintextStructure: StructuredDataMap, authSchema: AuthenticateSchemaMap)
@@ -480,24 +528,28 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
480528
BuildAuthMap2(keys, plaintextStructure, authSchema)
481529
}
482530

483-
function method UnBuildCryptoMap(list : CryptoList, dataSoFar : StructuredDataMap := map[], actionsSoFar : CryptoSchemaMap := map[]) :
531+
function method {:tailrecursion} UnBuildCryptoMap(list : CryptoList, pos : nat := 0, dataSoFar : StructuredDataMap := map[], actionsSoFar : CryptoSchemaMap := map[]) :
484532
(res : Result<(StructuredDataMap, CryptoSchemaMap), Error>)
533+
requires 0 <= pos <= |list|
534+
requires |dataSoFar| == pos
535+
requires |actionsSoFar| <= pos
485536
requires forall k <- actionsSoFar :: k in dataSoFar
486537
requires (forall v :: v in actionsSoFar.Values ==> IsAuthAttr(v))
487538
requires forall k <- list :: |k.key| == 1
539+
decreases |list| - pos
488540
ensures res.Success? ==>
489541
&& (forall k <- res.value.1 :: k in res.value.0)
490542
&& (forall v :: v in res.value.1.Values ==> IsAuthAttr(v))
491543
{
492-
if |list| == 0 then
544+
if |list| == pos then
493545
Success((dataSoFar, actionsSoFar))
494546
else
495-
var key :- Paths.UniPathToString(list[0].key);
547+
var key :- Paths.UniPathToString(list[pos].key);
496548
:- Need(key !in dataSoFar, E("Duplicate Key " + key));
497-
if IsAuthAttr(list[0].action) then
498-
UnBuildCryptoMap(list[1..], dataSoFar[key := list[0].data], actionsSoFar[key := list[0].action])
549+
if IsAuthAttr(list[pos].action) then
550+
UnBuildCryptoMap(list, pos+1, dataSoFar[key := list[pos].data], actionsSoFar[key := list[pos].action])
499551
else
500-
UnBuildCryptoMap(list[1..], dataSoFar[key := list[0].data], actionsSoFar)
552+
UnBuildCryptoMap(list, pos+1, dataSoFar[key := list[pos].data], actionsSoFar)
501553
}
502554

503555
lemma EncryptStructureOutputHasSinglePaths(origData : CryptoList, finalData : CryptoList)

0 commit comments

Comments
 (0)