feat: Merge changes from 3.1.2

CHANGELOG.md

@@ -1,5 +1,26 @@
 # Changelog
 
+## 3.1.2 2023-11-13
+
+### Fix
+
+Fixed an issue where, when using the DynamoDbEncryptionInterceptor,
+an encrypted item in the Attributes field of a DeleteItem, PutItem, or UpdateItem
+response was passed through unmodified instead of being decrypted.
+
+## 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/DecryptWithPermute/README.md 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()