fix: issue when a DynamoDB Set attribute is marked as SIGN_ONLY in th… (#560)

DB-ESDK for DynamoDB supports SIGN_ONLY and ENCRYPT_AND_SIGN attribute actions. In version 3.1.0 and below, when a Set type is assigned a SIGN_ONLY attribute action, there is a chance that signature validation of the record containing a Set will fail on read, even if the Set attributes contain the same values. The probability of a failure depends on the order of the elements in the Set combined with how DynamoDB returns this data, which is undefined.

This update addresses the issue by ensuring that any Set values are canonicalized in the same order while written to DynamoDB as when read back from DynamoDB.

See: https://github.com/aws/aws-database-encryption-sdk-dynamodb-java/tree/v3.1.1/DecryptWithPermute for additional details

Author: seebees

CHANGELOG.md

@@ -1,5 +1,18 @@
 # Changelog
 
+## 3.1.1 2023-11-07
+
+### Fix
+
+Issue when a DynamoDB Set attribute is marked as SIGN_ONLY in the AWS Database Encryption SDK (DB-ESDK) for DynamoDB.
+
+DB-ESDK for DynamoDB supports SIGN_ONLY and ENCRYPT_AND_SIGN attribute actions. In version 3.1.0 and below, when a Set type is assigned a SIGN_ONLY attribute action, there is a chance that signature validation of the record containing a Set will fail on read, even if the Set attributes contain the same values. The probability of a failure depends on the order of the elements in the Set combined with how DynamoDB returns this data, which is undefined.
+
+This update addresses the issue by ensuring that any Set values are canonicalized in the same order while written to DynamoDB as when read back from DynamoDB.
+
+See: https://github.com/aws/aws-database-encryption-sdk-dynamodb-java/tree/v3.1.1/DecryptWithPermute for additional details for additional details
+
+
 ## 3.1.0 2023-09-07
 
 ### Features

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -328,6 +328,7 @@ module SearchConfigToInfo {
     if |badNames| == 0 then
       None
     else
+      // We happen to order these values, but this ordering MUST NOT be relied upon.
       var badSeq := SortedSets.ComputeSetToOrderedSequence2(badNames, CharLess);
       Some(badSeq[0])
   }
@@ -399,6 +400,7 @@ module SearchConfigToInfo {
     if |badNames| == 0 then
       None
     else
+      // We happen to order these values, but this ordering MUST NOT be relied upon.
       var badSeq := SortedSets.ComputeSetToOrderedSequence2(badNames, CharLess);
       Some(badSeq[0])
   }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

@@ -44,6 +44,7 @@ module DynamoDBSupport {
       Success(true)
     else
       var bad := set k <- item | ReservedPrefix <= k;
+      // We happen to order these values, but this ordering MUST NOT be relied upon.
       var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, CharLess);
       if |badSeq| == 0 then
         Failure("")
@@ -173,6 +174,7 @@ module DynamoDBSupport {
       var both := newAttrs.Keys * item.Keys;
       var bad := set k <- both | newAttrs[k] != item[k];
       if 0 < |bad| {
+        // We happen to order these values, but this ordering MUST NOT be relied upon.
         var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, CharLess);
         return Failure(E("Supplied Beacons do not match calculated beacons : " + Join(badSeq, ", ")));
       }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

@@ -23,15 +23,8 @@ module DynamoToStruct {
   type StructuredDataTerminalType = x : StructuredData | x.content.Terminal? witness *
   type TerminalDataMap = map<AttributeName, StructuredDataTerminalType>
 
-//= specification/dynamodb-encryption-client/ddb-item-conversion.md#overview
-//= type=TODO
-//# The conversion from DDB Item to Structured Data must be lossless,
-//# meaning that converting a DDB Item to
-//# a Structured Data and back to a DDB Item again
-//# MUST result in the exact same DDB Item.
-
   // This file exists for these two functions : ItemToStructured and StructuredToItem
-  // which provide lossless conversion between an AttributeMap and a StructuredDataMap
+  // which provide conversion between an AttributeMap and a StructuredDataMap
 
   // Convert AttributeMap to StructuredDataMap
   //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-ddb-item-to-structured-data
@@ -107,6 +100,7 @@ module DynamoToStruct {
     else
       var badNames := set k <- s | !IsValid_AttributeName(k) :: k;
       OneBadKey(s, badNames, IsValid_AttributeName);
+      // We happen to order these values, but this ordering MUST NOT be relied upon.
       var orderedAttrNames := SetToOrderedSequence(badNames, CharLess);
       var attrNameList := Join(orderedAttrNames, ",");
       MakeError("Not valid attribute names : " + attrNameList)
@@ -317,7 +311,11 @@ module DynamoToStruct {
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#number
     //= type=implication
-    //# Number MUST be serialized as UTF-8 encoded bytes.
+    //# This value MUST be normalized in the same way as DynamoDB normalizes numbers.
+
+    //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#number
+    //= type=implication
+    //# This normalized value MUST then be serialized as UTF-8 encoded bytes.
     ensures a.N? && ret.Success? && !prefix ==>
       && Norm.NormalizeNumber(a.N).Success?
       && var nn := Norm.NormalizeNumber(a.N).value;
@@ -488,30 +486,52 @@ module DynamoToStruct {
   function method StringSetAttrToBytes(ss: StringSetAttributeValue): (ret: Result<seq<uint8>, string>)
     ensures ret.Success? ==> Seq.HasNoDuplicates(ss)
   {
-    :- Need(|Seq.ToSet(ss)| == |ss|, "String Set had duplicate values");
+    var asSet := Seq.ToSet(ss);
+    :- Need(|asSet| == |ss|, "String Set had duplicate values");
     Seq.LemmaNoDuplicatesCardinalityOfSet(ss);
-    var count :- U32ToBigEndian(|ss|);
-    var body :- CollectString(ss);
+
+    //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries
+    //# Entries in a String Set MUST be ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
+    var sortedList := SortedSets.ComputeSetToOrderedSequence2(asSet, CharLess);
+    var count :- U32ToBigEndian(|sortedList|);
+    var body :- CollectString(sortedList);
     Success(count + body)
   }
 
   function method NumberSetAttrToBytes(ns: NumberSetAttributeValue): (ret: Result<seq<uint8>, string>)
     ensures ret.Success? ==> Seq.HasNoDuplicates(ns)
   {
-    :- Need(|Seq.ToSet(ns)| == |ns|, "Number Set had duplicate values");
+    var asSet := Seq.ToSet(ns);
+    :- Need(|asSet| == |ns|, "Number Set had duplicate values");
     Seq.LemmaNoDuplicatesCardinalityOfSet(ns);
-    var count :- U32ToBigEndian(|ns|);
-    var body :- CollectString(ns);
+
+    var normList :- Seq.MapWithResult(n => Norm.NormalizeNumber(n), ns);
+    var asSet := Seq.ToSet(normList);
+    :- Need(|asSet| == |normList|, "Number Set had duplicate values after normalization.");
+
+    //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries
+    //# Entries in a Number Set MUST be ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
+
+    //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries
+    //# This ordering MUST be applied after normalization of the number value.
+    var sortedList := SortedSets.ComputeSetToOrderedSequence2(asSet, CharLess);
+    var count :- U32ToBigEndian(|sortedList|);
+    var body :- CollectString(sortedList);
     Success(count + body)
   }
 
   function method BinarySetAttrToBytes(bs: BinarySetAttributeValue): (ret: Result<seq<uint8>, string>)
     ensures ret.Success? ==> Seq.HasNoDuplicates(bs)
   {
-    :- Need(|Seq.ToSet(bs)| == |bs|, "Binary Set had duplicate values");
+    var asSet := Seq.ToSet(bs);
+    :- Need(|asSet| == |bs|, "Binary Set had duplicate values");
     Seq.LemmaNoDuplicatesCardinalityOfSet(bs);
-    var count :- U32ToBigEndian(|bs|);
-    var body :- CollectBinary(bs);
+
+    //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries
+    //# Entries in a Binary Set MUST be ordered lexicographically by their underlying bytes in ascending order.
+    var sortedList := SortedSets.ComputeSetToOrderedSequence2(asSet, ByteLess);
+    var count :- U32ToBigEndian(|sortedList|);
+    var body :- CollectBinary(sortedList);
     Success(count + body)
   }
 
@@ -749,6 +769,9 @@ module DynamoToStruct {
     ensures (ret.Success? && |mapToSerialize| == 0) ==> (ret.value == serialized)
     ensures (ret.Success? && |mapToSerialize| == 0) ==> (|ret.value| == |serialized|)
   {
+    //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
+    //# Entries in a serialized Map MUST be ordered by key value,
+    //# ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
     var keys := SortedSets.ComputeSetToOrderedSequence2(mapToSerialize.Keys, CharLess);
     CollectOrderedMapSubset(keys, mapToSerialize, serialized)
   }
@@ -1136,6 +1159,7 @@ module DynamoToStruct {
       OneBadResult(m);
       var badValues := FlattenErrors(m);
       assert(|badValues| > 0);
+      // We happen to order these values, but this ordering MUST NOT be relied upon.
       var badValueSeq := SetToOrderedSequence(badValues, CharLess);
       Failure(Join(badValueSeq, "\n"))
   }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -344,12 +344,6 @@ module SearchableEncryptionInfo {
       versions[currWrite].IsVirtualField(field)
     }
 
-    function method GenerateClosure(fields : seq<string>) : seq<string>
-      requires ValidState()
-    {
-      versions[currWrite].GenerateClosure(fields)
-    }
-
     method GeneratePlainBeacons(item : DDB.AttributeMap) returns (output : Result<DDB.AttributeMap, Error>)
       requires ValidState()
     {
@@ -559,6 +553,7 @@ module SearchableEncryptionInfo {
     requires version == 1
     requires keySource.ValidState()
   {
+    // We happen to order these values, but this ordering MUST NOT be relied upon.
     var beaconNames := SortedSets.ComputeSetToOrderedSequence2(beacons.Keys, CharLess);
     var stdKeys := Seq.Filter((k : string) => k in beacons && beacons[k].Standard?, beaconNames);
     FilterPreservesHasNoDuplicates((k : string) => k in beacons && beacons[k].Standard?, beaconNames);
@@ -575,6 +570,7 @@ module SearchableEncryptionInfo {
     keySource : KeySource,
     virtualFields : VirtualFieldMap,
     beacons : BeaconMap,
+    // The ordering of `beaconNames` MUST NOT be relied upon.
     beaconNames : seq<string>,
     stdNames : seq<string>,
     encryptedFields : set<string>
@@ -614,13 +610,6 @@ module SearchableEncryptionInfo {
         [field]
     }
 
-    function method GenerateClosure(fields : seq<string>) : seq<string>
-    {
-      var fieldLists := Seq.Map((s : string) => GetFields(s), fields);
-      var fieldSet := set f <- fieldLists, g <- f :: g;
-      SortedSets.ComputeSetToOrderedSequence2(fieldSet, CharLess)
-    }
-
     method getKeyMap(keyId : MaybeKeyId) returns (output : Result<MaybeKeyMap, Error>)
       requires ValidState()
       ensures ValidState()