Skip to content

Commit 392339a

Browse files
ajewellamzajewellamz
committed
m
1 parent 58ecd55 commit 392339a

File tree

5 files changed

+60
-73
lines changed

5 files changed

+60
-73
lines changed

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,12 +31,12 @@ module DynamoToStruct {
3131
// var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();
3232
// return MakeError("Not valid attribute names : ");
3333

34-
var structuredMap := map k <- item | k in actions && actions[k] != DO_NOTHING :: k := AttrToStructured(item[k]);
34+
var structuredMap := map k <- item | (k in actions && actions[k] != DO_NOTHING) || (ReservedPrefix <= k) :: k := AttrToStructured(item[k]);
3535
MapKeysMatchItems(item);
3636
MapError(SimplifyMapValue(structuredMap))
3737
}
3838

39-
function method StructuredToItem2(s : TerminalDataMap, orig : AttributeMap, actions : Types.AttributeActions) : (ret : Result<AttributeMap, Error>)
39+
function method StructuredToItem2(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
4040
{
4141
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]);
4242
MapKeysMatchItems(orig);
@@ -405,7 +405,7 @@ module DynamoToStruct {
405405
&& ListAttrToBytes(a.L, depth).Success?
406406
&& ret.value[PREFIX_LEN..] == ListAttrToBytes(a.L, depth).value
407407
&& ListAttrToBytes(a.L, depth).value[..LENGTH_LEN] == U32ToBigEndian(|a.L|).value
408-
&& ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value
408+
// && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value
409409
&& (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN)
410410

411411
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-attribute

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

Lines changed: 24 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -223,6 +223,25 @@ module SearchableEncryptionInfo {
223223
return Success(keyLoc.keys);
224224
}
225225

226+
function method PosLongAdd(x : MP.PositiveLong, y : MP.PositiveLong) : MP.PositiveLong
227+
{
228+
assert MP.IsValid_PositiveLong(x);
229+
assert MP.IsValid_PositiveLong(y);
230+
if x as nat + y as nat < INT64_MAX_LIMIT then
231+
x + y
232+
else
233+
INT64_MAX_LIMIT as MP.PositiveLong
234+
}
235+
function method PosLongSub(x : MP.PositiveLong, y : MP.PositiveLong) : MP.PositiveLong
236+
{
237+
assert MP.IsValid_PositiveLong(x);
238+
assert MP.IsValid_PositiveLong(y);
239+
if x <= y then
240+
0
241+
else
242+
x - y
243+
}
244+
226245
// Checks if (time_now - cache creation time of the extracted cache entry) is less than the allowed
227246
// TTL of the current Beacon Key Source calling the getEntry method from the cache.
228247
// Mitigates risk if another Beacon Key Source wrote the entry with a longer TTL.
@@ -232,7 +251,10 @@ module SearchableEncryptionInfo {
232251
ttlSeconds: MP.PositiveLong
233252
): (output: bool)
234253
{
235-
now - creationTime <= ttlSeconds as MP.PositiveLong
254+
if now <= creationTime then
255+
true
256+
else
257+
PosLongSub(now, creationTime) <= ttlSeconds as MP.PositiveLong
236258
}
237259

238260
method getKeysCache(
@@ -406,7 +428,6 @@ module SearchableEncryptionInfo {
406428
var keyMap :- getAllKeys(stdNames, key.value);
407429
var beaconKeyMaterials := rawBeaconKeyMaterials.beaconKeyMaterials.(beaconKey := None, hmacKeys := Some(keyMap));
408430

409-
expect now < UInt.BoundedInts.INT64_MAX - cacheTTL;
410431
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
411432
//# These materials MUST be put into the associated [Key Store Cache](#key-store-cache)
412433
//# with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time)
@@ -415,7 +436,7 @@ module SearchableEncryptionInfo {
415436
identifier := cacheDigest,
416437
materials := MP.Materials.BeaconKey(beaconKeyMaterials),
417438
creationTime := now,
418-
expiryTime := now + cacheTTL,
439+
expiryTime := PosLongAdd(now, cacheTTL),
419440
messagesUsed := None,
420441
bytesUsed := None
421442
);

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

Lines changed: 31 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -417,6 +417,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
417417
ensures version == 1 <==> ret == CSE.SIGN_ONLY
418418
ensures version == 2 <==> ret == CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
419419
{
420+
assert StructuredEncryptionHeader.ValidVersion(version);
421+
assert version == 1 || version == 2;
420422
if version == 2 then
421423
CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
422424
else
@@ -546,7 +548,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
546548
// get CryptoSchema for this item
547549
function method ConfigToCryptoSchema(
548550
config : InternalConfig,
549-
item : ComAmazonawsDynamodbTypes.AttributeMap)
551+
item : DynamoToStruct.TerminalDataMap)
550552
: (ret : Result<CSE.CryptoSchemaMap, DDBE.Error>)
551553

552554
//= specification/dynamodb-encryption-client/encrypt-item.md#behavior
@@ -590,7 +592,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
590592
// get AuthenticateSchema for this item
591593
function method ConfigToAuthenticateSchema(
592594
config : InternalConfig,
593-
item : ComAmazonawsDynamodbTypes.AttributeMap)
595+
item : DynamoToStruct.TerminalDataMap)
594596
: (ret : CSE.AuthenticateSchemaMap)
595597
requires ValidInternalConfig?(config)
596598

@@ -636,6 +638,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
636638
ensures ret.Success? ==> forall k <- ret.value.Keys :: InSignatureScope(config, k)
637639
ensures ret.Success? ==> forall k <- ret.value.Keys :: !ret.value[k].DO_NOTHING?
638640
{
641+
assert forall k <- schema :: SE.IsAuthAttr(schema[k]);
642+
assert forall k <- schema :: !schema[k].DO_NOTHING?;
639643
:- Need(forall k <- schema :: InSignatureScope(config, k),
640644
DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: mismatch with signature scope"));
641645
:- Need(forall k <- schema :: ComAmazonawsDynamodbTypes.IsValid_AttributeName(k),
@@ -747,22 +751,22 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
747751
&& (|config.structuredEncryption.History.EncryptStructure| == |old(config.structuredEncryption.History.EncryptStructure)| + 1)
748752
&& (Seq.Last(config.structuredEncryption.History.EncryptStructure).output.Success?)
749753

750-
//= specification/dynamodb-encryption-client/encrypt-item.md#behavior
751-
//= type=implication
752-
//# - Crypto Schema MUST be a [Crypto Schema](../structured-encryption/structures.md#crypto-schema)
753-
//# analogous to the [configured Attribute Actions](./ddb-table-encryption-config.md#attribute-actions).
754-
&& ConfigToCryptoSchema(config, input.plaintextItem).Success?
755-
&& Seq.Last(config.structuredEncryption.History.EncryptStructure).input.cryptoSchema
756-
== ConfigToCryptoSchema(config, input.plaintextItem).value
757-
758754
//= specification/dynamodb-encryption-client/encrypt-item.md#behavior
759755
//= type=implication
760756
//# - Structured Data MUST be the Structured Data converted above.
761-
&& DynamoToStruct.ItemToStructured(input.plaintextItem).Success?
762-
&& var plaintextStructure := DynamoToStruct.ItemToStructured(input.plaintextItem).value;
757+
&& DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt).Success?
758+
&& var plaintextStructure := DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt).value;
763759
&& Seq.Last(config.structuredEncryption.History.EncryptStructure).input.plaintextStructure
764760
== plaintextStructure
765761

762+
//= specification/dynamodb-encryption-client/encrypt-item.md#behavior
763+
//= type=implication
764+
//# - Crypto Schema MUST be a [Crypto Schema](../structured-encryption/structures.md#crypto-schema)
765+
//# analogous to the [configured Attribute Actions](./ddb-table-encryption-config.md#attribute-actions).
766+
&& ConfigToCryptoSchema(config, plaintextStructure).Success?
767+
&& Seq.Last(config.structuredEncryption.History.EncryptStructure).input.cryptoSchema
768+
== ConfigToCryptoSchema(config, plaintextStructure).value
769+
766770
//= specification/dynamodb-encryption-client/encrypt-item.md#behavior
767771
//= type=implication
768772
//# - Encryption Context MUST be this input Item's [DynamoDB Item Base Context](#dynamodb-item-base-context).
@@ -800,8 +804,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
800804
==>
801805
&& output.value.encryptedItem == input.plaintextItem
802806
&& output.value.parsedHeader == None
803-
804-
ensures output.Success? ==> |input.plaintextItem| <= MAX_ATTRIBUTE_COUNT
805807
{
806808
:- Need(
807809
&& config.partitionKeyName in input.plaintextItem
@@ -811,12 +813,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
811813
:- Need(ContextAttrsExist(config.attributeActionsOnEncrypt, input.plaintextItem),
812814
E(ContextMissingMsg(config.attributeActionsOnEncrypt, input.plaintextItem)));
813815

814-
if |input.plaintextItem| > MAX_ATTRIBUTE_COUNT {
815-
var actCount := String.Base10Int2String(|input.plaintextItem|);
816-
var maxCount := String.Base10Int2String(MAX_ATTRIBUTE_COUNT);
817-
return Failure(E("Item to encrypt had " + actCount + " attributes, but maximum allowed is " + maxCount));
818-
}
819-
820816
//= specification/dynamodb-encryption-client/encrypt-item.md#behavior
821817
//# If a [Legacy Policy](./ddb-table-encryption-config.md#legacy-policy) of
822818
//# `FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT` is specified,
@@ -839,10 +835,10 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
839835
return Success(passthroughOutput);
840836
}
841837

842-
var plaintextStructure :- DynamoToStruct.ItemToStructured(input.plaintextItem)
838+
var plaintextStructure :- DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt)
843839
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
844840
var context :- MakeEncryptionContextForEncrypt(config, plaintextStructure);
845-
var cryptoSchema :- ConfigToCryptoSchema(config, input.plaintextItem)
841+
var cryptoSchema :- ConfigToCryptoSchema(config, plaintextStructure)
846842
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
847843

848844
//= specification/dynamodb-encryption-client/encrypt-item.md#behavior
@@ -893,7 +889,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
893889
e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e)));
894890
var encryptedData := encryptVal.encryptedStructure;
895891
:- Need(forall k <- encryptedData :: DDB.IsValid_AttributeName(k), E(""));
896-
var ddbKey :- DynamoToStruct.StructuredToItem(encryptedData)
892+
var ddbKey :- DynamoToStruct.StructuredToItem2(encryptedData, input.plaintextItem, config.attributeActionsOnEncrypt)
897893
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
898894

899895
var parsedActions :- ConvertCryptoSchemaToAttributeActions(config, encryptVal.cryptoSchema);
@@ -957,21 +953,21 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
957953
&& (|config.structuredEncryption.History.DecryptStructure| == |old(config.structuredEncryption.History.DecryptStructure)| + 1)
958954
&& (Seq.Last(config.structuredEncryption.History.DecryptStructure).output.Success?)
959955

960-
//= specification/dynamodb-encryption-client/decrypt-item.md#behavior
961-
//= type=implication
962-
//# - Authenticate Schema MUST be a [Authenticate Schema](../structured-encryption/structures.md#crypto-schema)
963-
//# built with the following requirements:
964-
&& Seq.Last(config.structuredEncryption.History.DecryptStructure).input.authenticateSchema
965-
== ConfigToAuthenticateSchema(config, input.encryptedItem)
966-
967956
//= specification/dynamodb-encryption-client/decrypt-item.md#behavior
968957
//= type=implication
969958
//# - Encrypted Structured Data MUST be the Structured Data converted above.
970-
&& DynamoToStruct.ItemToStructured(input.encryptedItem).Success?
971-
&& var plaintextStructure := DynamoToStruct.ItemToStructured(input.encryptedItem).value;
959+
&& DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt).Success?
960+
&& var plaintextStructure := DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt).value;
972961
&& Seq.Last(config.structuredEncryption.History.DecryptStructure).input.encryptedStructure
973962
== plaintextStructure
974963

964+
//= specification/dynamodb-encryption-client/decrypt-item.md#behavior
965+
//= type=implication
966+
//# - Authenticate Schema MUST be a [Authenticate Schema](../structured-encryption/structures.md#crypto-schema)
967+
//# built with the following requirements:
968+
&& Seq.Last(config.structuredEncryption.History.DecryptStructure).input.authenticateSchema
969+
== ConfigToAuthenticateSchema(config, plaintextStructure)
970+
975971
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
976972
//= type=implication
977973
//# The item to be encrypted MUST have an attribute named `aws_dbe_head`.
@@ -1037,13 +1033,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
10371033
&& output.value.plaintextItem == input.encryptedItem
10381034
&& output.value.parsedHeader == None
10391035
{
1040-
var realCount := |set k <- input.encryptedItem | !(ReservedPrefix <= k)|;
1041-
if realCount > MAX_ATTRIBUTE_COUNT {
1042-
var actCount := String.Base10Int2String(realCount);
1043-
var maxCount := String.Base10Int2String(MAX_ATTRIBUTE_COUNT);
1044-
return Failure(E("Item to decrypt had " + actCount + " attributes, but maximum allowed is " + maxCount));
1045-
}
1046-
10471036
:- Need(
10481037
&& config.partitionKeyName in input.encryptedItem
10491038
&& (config.sortKeyName.None? || config.sortKeyName.value in input.encryptedItem)
@@ -1081,15 +1070,15 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
10811070
DynamoDbItemEncryptorException(
10821071
message := "Encrypted item missing expected header and footer attributes"));
10831072

1084-
var encryptedStructure :- DynamoToStruct.ItemToStructured(input.encryptedItem)
1073+
var encryptedStructure :- DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt)
10851074
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
10861075
:- Need(SE.HeaderField in input.encryptedItem, E("Header field, \"aws_dbe_head\", not in item."));
10871076
var header := input.encryptedItem[SE.HeaderField];
10881077
:- Need(header.B?, E("Header field, \"aws_dbe_head\", not binary"));
10891078
assert header.B?;
10901079
:- Need(0 < |header.B|, E("Unexpected empty header field."));
10911080
var context :- MakeEncryptionContextForDecrypt(config, header.B, encryptedStructure);
1092-
var authenticateSchema := ConfigToAuthenticateSchema(config, input.encryptedItem);
1081+
var authenticateSchema := ConfigToAuthenticateSchema(config, encryptedStructure);
10931082

10941083
//= specification/dynamodb-encryption-client/decrypt-item.md#behavior
10951084
//# This operation MUST create a
@@ -1123,7 +1112,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
11231112
e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e)));
11241113
var decryptedData := decryptVal.plaintextStructure;
11251114
:- Need(forall k <- decryptedData :: DDB.IsValid_AttributeName(k), E(""));
1126-
var ddbItem :- DynamoToStruct.StructuredToItem(decryptedData)
1115+
var ddbItem :- DynamoToStruct.StructuredToItem2(decryptedData, input.encryptedItem, decryptVal.cryptoSchema)
11271116
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
11281117

11291118
var schemaToConvert := decryptVal.cryptoSchema;

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ module DynamoDbItemEncryptorUtil {
1818
const ReservedPrefix := "aws_dbe_"
1919
const BeaconPrefix := ReservedPrefix + "b_"
2020
const VersionPrefix := ReservedPrefix + "v_"
21-
const MAX_ATTRIBUTE_COUNT := 100
2221
const UINT32_MAX : uint32 := 0xFFFF_FFFF
2322

2423
function method E(msg : string) : Error

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy

Lines changed: 2 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -605,10 +605,10 @@ module DynamoDbItemEncryptorTest {
605605
expect parsedHeader.value.selectorContext == map["bar" := DDB.AttributeValue.S("key")];
606606
}
607607

608-
method {:test} TestMaxRoundTrip() {
608+
method {:test} TestLargeRoundTrip() {
609609
var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")];
610610
var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY];
611-
for i := 0 to (MAX_ATTRIBUTE_COUNT-1) {
611+
for i := 0 to 500 {
612612
var str := String.Base10Int2String(i);
613613
expect DDB.IsValid_AttributeName(str);
614614
inputItem := inputItem[str := DDBS(str)];
@@ -649,26 +649,4 @@ module DynamoDbItemEncryptorTest {
649649
expect PublicKeyUtf8 in parsedHeader.value.storedEncryptionContext.Keys;
650650
expect |parsedHeader.value.encryptedDataKeys| == 1;
651651
}
652-
653-
method {:test} TestTooManyAttributes() {
654-
var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")];
655-
var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY];
656-
for i := 0 to MAX_ATTRIBUTE_COUNT {
657-
var str := String.Base10Int2String(i);
658-
expect DDB.IsValid_AttributeName(str);
659-
inputItem := inputItem[str := DDBS(str)];
660-
actions := actions[str := CSE.ENCRYPT_AND_SIGN];
661-
}
662-
var config := TestFixtures.GetEncryptorConfigFromActions(actions);
663-
var encryptor := TestFixtures.GetDynamoDbItemEncryptorFrom(config);
664-
665-
var encryptRes := encryptor.EncryptItem(
666-
Types.EncryptItemInput(
667-
plaintextItem:=inputItem
668-
)
669-
);
670-
671-
expect encryptRes.Failure?;
672-
expect encryptRes.error == E("Item to encrypt had 101 attributes, but maximum allowed is 100");
673-
}
674652
}

0 commit comments

Comments
 (0)