fix: validate attribute name length by UTF-8 byte count

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;
 

DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy

@@ -568,4 +568,32 @@ module DynamoToStructTest {
     expect struct.Failure?;
     expect struct.error == E("Depth of attribute structure to serialize exceeds limit of 32");
   }
+
+  method {:test} TestAttributeNameTooLongBytes() {
+    // 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)]);
+    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";
+  }
+
+  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<uint8> := 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<uint8> := [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";
+  }
 }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy

@@ -30,6 +30,33 @@ module PutItemTransformTest {
 
   const BasicItem : DDB.AttributeMap := map["bar" := DDB.AttributeValue.S("baz")]
 
+  method {:test} TestPutItemAttributeNameTooLongBytes() {
+    var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms();
+    var tableName := GetTableName("foo");
+    // 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(
+      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?;
+    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<AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride>) {
     assume {:axiom} false;
     var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMulti(plaintextOverride);