From 0c6ad76f7c654b759190c5e0938e03e58059c852 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 16 Jun 2026 15:41:44 -0700 Subject: [PATCH 1/3] fix: validate attribute name length by UTF-8 byte count Attribute name length was validated asymmetrically: encode only rejected keys that overflowed the 4-byte length field (~4.29 GB), while decode enforced the character-based IsValid_AttributeName (<= 65535 chars). Keys between 65,536 bytes and ~4.29 GB encrypted and persisted but were rejected on decode, making the data permanently unreadable. Add a byte-based check (1 <= |UTF8.Encode(key)| <= 65535) on both the encode (SerializeMapItem) and decode (DeserializeMapEntry) paths so over-long keys fail fast at encrypt time. The check is done in DB-ESDK rather than via IsValid_AttributeName, which is generated and inherently character-based. --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 8 +++++++ .../test/DynamoToStruct.dfy | 13 +++++++++++ .../test/PutItemTransform.dfy | 22 +++++++++++++++++++ 3 files changed, 43 insertions(+) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 8af15b5b75..682540c8ce 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -282,6 +282,10 @@ module DynamoToStruct { const LENGTH_LEN64 : uint64 := 4 // number of bytes in an encoded count or length const PREFIX_LEN64 : uint64 := 6 // number of bytes in a prefix, i.e. 2-byte type and 4-byte length + // Max bytes in a DynamoDB attribute name (UTF-8). Validated byte-based, not via the + // character-based IsValid_AttributeName, to match the real DynamoDB rule. + const MAX_ATTR_NAME_LEN64 : uint64 := 65535 + function method AttrToTypeId(a : AttributeValue) : TerminalTypeId { match a { @@ -946,6 +950,8 @@ module DynamoToStruct { var name :- UTF8.Encode(key); assert UTF8.Decode(name).Success?; SequenceIsSafeBecauseItIsInMemory(name); + // Attribute name length is validated on the UTF-8 byte length, not the character count. + :- Need(1 <= |name| as uint64 <= MAX_ATTR_NAME_LEN64, "Attribute name must be between 1 and 65535 UTF-8 bytes"); var len :- U32ToBigEndian64(|name| as uint64); //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries @@ -1263,6 +1269,8 @@ module DynamoToStruct { var len : uint64 :- BigEndianPosToU32As64(serialized, pos); var pos := pos + LENGTH_LEN64; :- Need(len <= serialized_size-pos, "Key of Map of Structured Data has too few bytes"); + // Attribute name length is validated on the UTF-8 byte length, not the character count. + :- Need(1 <= len <= MAX_ATTR_NAME_LEN64, "Attribute name must be between 1 and 65535 UTF-8 bytes"); var key :- UTF8.Decode(serialized[pos..pos+len]); var pos := pos + len; diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy index 223678b96a..2ae2c10ba1 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy @@ -568,4 +568,17 @@ module DynamoToStructTest { expect struct.Failure?; expect struct.error == E("Depth of attribute structure to serialize exceeds limit of 32"); } + + method {:test} TestAttributeNameTooLongBytes() { + // U+00E9 encodes to 2 UTF-8 bytes. + var twoByteChar := 0xE9 as char; + var longKey : string := seq(40000, i => twoByteChar); + var mapValue := AttributeValue.M(map[longKey := AttributeValue.BOOL(true)]); + var result := AttrToStructured(mapValue); + if !result.Failure? { + print "\nAttrToStructured should have failed for an over-long attribute name\n"; + } + expect result.Failure?; + expect result.error == "Attribute name must be between 1 and 65535 UTF-8 bytes"; + } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy index 8ee8feebf6..7cb0179c37 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy @@ -30,6 +30,28 @@ module PutItemTransformTest { const BasicItem : DDB.AttributeMap := map["bar" := DDB.AttributeValue.S("baz")] + method {:test} TestPutItemAttributeNameTooLongBytes() { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); + var tableName := GetTableName("foo"); + // U+00E9 encodes to 2 UTF-8 bytes; 40000 chars => 80000 bytes (> 65535), + // a valid AttributeName by character count but too long in bytes. + var twoByteChar := 0xE9 as char; + var longKey : DDB.AttributeName := seq(40000, i => twoByteChar); + var input := DDB.PutItemInput( + TableName := tableName, + Item := map[ + "bar" := DDB.AttributeValue.S("key"), + "encrypt" := DDB.AttributeValue.M(map[longKey := DDB.AttributeValue.S("x")]) + ] + ); + var transformed := middlewareUnderTest.PutItemInputTransform( + AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( + sdkInput := input + ) + ); + expect transformed.Failure?; + } + method TestPutItemInputMultiFail(plaintextOverride : Option) { assume {:axiom} false; var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMulti(plaintextOverride); From 0c1a839f28ec6237ec95de0ac4a2317c0df545e9 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 16 Jun 2026 15:49:41 -0700 Subject: [PATCH 2/3] test: tidy comment and assert error message in PutItem transform test --- .../dafny/DynamoDbEncryption/test/DynamoToStruct.dfy | 2 +- .../test/PutItemTransform.dfy | 9 +++++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy index 2ae2c10ba1..1b6c206292 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy @@ -570,7 +570,7 @@ module DynamoToStructTest { } method {:test} TestAttributeNameTooLongBytes() { - // U+00E9 encodes to 2 UTF-8 bytes. + // 0xE9 is a 2-byte UTF-8 char, so 40000 chars => 80000 bytes, exceeding the 65535-byte limit. var twoByteChar := 0xE9 as char; var longKey : string := seq(40000, i => twoByteChar); var mapValue := AttributeValue.M(map[longKey := AttributeValue.BOOL(true)]); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy index 7cb0179c37..5d5d03055b 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy @@ -33,8 +33,7 @@ module PutItemTransformTest { method {:test} TestPutItemAttributeNameTooLongBytes() { var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); var tableName := GetTableName("foo"); - // U+00E9 encodes to 2 UTF-8 bytes; 40000 chars => 80000 bytes (> 65535), - // a valid AttributeName by character count but too long in bytes. + // 0xE9 is a 2-byte UTF-8 char, so 40000 chars => 80000 bytes, exceeding the 65535-byte limit. var twoByteChar := 0xE9 as char; var longKey : DDB.AttributeName := seq(40000, i => twoByteChar); var input := DDB.PutItemInput( @@ -50,6 +49,12 @@ module PutItemTransformTest { ) ); expect transformed.Failure?; + expect transformed.error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor?; + var encErr := transformed.error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor; + expect encErr.AwsCryptographyDbEncryptionSdkDynamoDb?; + var ddbErr := encErr.AwsCryptographyDbEncryptionSdkDynamoDb; + expect ddbErr.DynamoDbEncryptionException?; + expect ddbErr.message == "Attribute name must be between 1 and 65535 UTF-8 bytes"; } method TestPutItemInputMultiFail(plaintextOverride : Option) { From 11c8ac57ead83eb8667377798ca63bc474327586 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Wed, 17 Jun 2026 09:46:40 -0700 Subject: [PATCH 3/3] test: add decode-path test for over-long attribute name --- .../DynamoDbEncryption/test/DynamoToStruct.dfy | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy index 1b6c206292..059d26e44a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy @@ -581,4 +581,19 @@ module DynamoToStructTest { expect result.Failure?; expect result.error == "Attribute name must be between 1 and 65535 UTF-8 bytes"; } + + method {:test} TestDecodeAttributeNameTooLongBytes() { + // Decode side: a serialized map whose key length field is 65536 bytes (one over the + // limit), with that many key bytes actually present so the length check is what fails. + var bigKey : seq := seq(65536, i => 0x41 as uint8); + // count=1 | key type id STRING (0,1) | key length 65536 (0x00010000) | key bytes | value type STRING (0,1) | value length 0 + var mapBytes : seq := [0, 0, 0, 1] + [0, 1] + [0, 1, 0, 0] + bigKey + [0, 1] + [0, 0, 0, 0]; + var data := StructuredDataTerminal(value := mapBytes, typeId := SE.MAP); + var result := StructuredToAttr(data); + if !result.Failure? { + print "\nStructuredToAttr should have failed for an over-long attribute name\n"; + } + expect result.Failure?; + expect result.error == "Attribute name must be between 1 and 65535 UTF-8 bytes"; + } }