Merge branch 'main' into python-poc

Author: Lucas McDonald

DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy

@@ -10,10 +10,11 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
   import AlgorithmSuites
   import Header = StructuredEncryptionHeader
   import opened DynamoDbEncryptionUtil
+  import opened StandardLibrary.MemoryMath
 
-  const SALT_LENGTH := 16
-  const IV_LENGTH := 12
-  const VERSION_LENGTH := 16
+  const SALT_LENGTH : uint64 := 16
+  const IV_LENGTH : uint64 := 12
+  const VERSION_LENGTH : uint64 := 16
 
   predicate ValidInternalConfig?(config: InternalConfig)
   {true}
@@ -70,7 +71,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
     var list : EncryptedDataKeyDescriptionList := [];
     //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
     //# - For every Data Key in Data Keys, the operation MUST attempt to extract a description of the Data Key.
-    for i := 0 to |datakeys| {
+    for i : uint64 := 0 to |datakeys| as uint64 {
       var extractedKeyProviderId :- UTF8.Decode(datakeys[i].keyProviderId).MapFailure(e => E(e));
       var extractedKeyProviderIdInfo:= Option.None;
       var expectedBranchKeyVersion := Option.None;
@@ -91,7 +92,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
           var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH;
           var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH;
           :- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, E("Wrong branch key version index."));
-          :- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length."));
+          SequenceIsSafeBecauseItIsInMemory(providerWrappedMaterial);
+          :- Need(|providerWrappedMaterial| as uint64 >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length."));
           var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX];
           var maybeBranchKeyVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => E(e));
           expectedBranchKeyVersion := Some(maybeBranchKeyVersion);

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -23,6 +23,7 @@ module SearchConfigToInfo {
   import opened DynamoDbEncryptionUtil
   import opened TermLoc
   import opened StandardLibrary.String
+  import opened StandardLibrary.MemoryMath
   import MaterialProviders
   import SortedSets
 
@@ -757,15 +758,15 @@ module SearchConfigToInfo {
   function method MakeDefaultConstructor(
     parts : seq<CB.BeaconPart>,
     ghost allParts : seq<CB.BeaconPart>,
-    ghost numNon : nat,
+    ghost numNon : uint64,
     converted : seq<CB.ConstructorPart> := []
   )
     : (ret : Result<seq<CB.Constructor>, Error>)
     requires 0 < |parts| + |converted|
     requires |allParts| == |parts| + |converted|
     requires parts == allParts[|converted|..]
-    requires numNon <= |allParts|
-    requires CB.OrderedParts(allParts, numNon)
+    requires numNon as nat <= |allParts|
+    requires CB.OrderedParts(allParts, numNon as nat)
     requires forall i | 0 <= i < |converted| ::
                && converted[i].part == allParts[i]
                && converted[i].required
@@ -776,7 +777,7 @@ module SearchConfigToInfo {
                  //= type=implication
                  //# * This default constructor MUST be all of the signed parts,
                  //# followed by all the encrypted parts, all parts being required.
-              && CB.OrderedParts(allParts, numNon)
+              && CB.OrderedParts(allParts, numNon as nat)
               && (forall i | 0 <= i < |ret.value[0].parts| ::
                     && ret.value[0].parts[i].part == allParts[i]
                     && ret.value[0].parts[i].required)
@@ -887,13 +888,13 @@ module SearchConfigToInfo {
     constructors : Option<ConstructorList>,
     name : string,
     parts : seq<CB.BeaconPart>,
-    ghost numSigned : nat
+    ghost numSigned : uint64
   )
     : (ret : Result<seq<CB.Constructor>, Error>)
     requires 0 < |parts|
     requires constructors.Some? ==> 0 < |constructors.value|
-    requires numSigned <= |parts|
-    requires CB.OrderedParts(parts, numSigned)
+    requires numSigned as nat <= |parts|
+    requires CB.OrderedParts(parts, numSigned as nat)
     ensures ret.Success? ==>
               && (constructors.None? ==> |ret.value| == 1)
               && (constructors.Some? ==> |ret.value| == |constructors.value|)
@@ -1065,10 +1066,11 @@ module SearchConfigToInfo {
     :- Need(beacon.constructors.Some? || |signedParts| != 0 || |encryptedParts| != 0,
             E("Compound beacon " + beacon.name + " defines no constructors, and also no local parts. Cannot make a default constructor from global parts."));
 
-    var numNon := |signed|;
-    assert CB.OrderedParts(signed, numNon);
+    SequenceIsSafeBecauseItIsInMemory(signed);
+    var numNon := |signed| as uint64;
+    assert CB.OrderedParts(signed, numNon as nat);
     var allParts := signed + encrypted;
-    assert CB.OrderedParts(allParts, numNon);
+    assert CB.OrderedParts(allParts, numNon as nat);
 
     var isSignedBeacon := |encrypted| == 0;
     var _ :- BeaconNameAllowed(outer, virtualFields, beacon.name, "CompoundBeacon", isSignedBeacon);
@@ -1087,7 +1089,7 @@ module SearchConfigToInfo {
       ),
       beacon.split[0],
       allParts,
-      numNon,
+      numNon as nat,
       constructors
     )
   }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

@@ -19,6 +19,7 @@ module DynamoDBSupport {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened StandardLibrary.MemoryMath
   import opened DynamoDbEncryptionUtil
   import opened DdbVirtualFields
   import opened SearchableEncryptionInfo
@@ -33,23 +34,30 @@ module DynamoDBSupport {
   // At the moment, this means that no attribute names starts with "aws_dbe_",
   // as all other attribute names would need to be configured, and all the
   // other weird constraints were checked at configuration time.
-  function method IsWriteable(item : DDB.AttributeMap)
-    : (ret : Result<bool, string>)
+  method IsWriteable(item : DDB.AttributeMap)
+    returns (ret : Result<bool, string>)
     //= specification/dynamodb-encryption-client/ddb-support.md#writable
     //= type=implication
     //# Writeable MUST reject any item containing an attribute which begins with `aws_dbe_`.
     ensures ret.Success? ==> forall k <- item :: !(ReservedPrefix <= k)
   {
-    if forall k <- item :: !(ReservedPrefix <= k) then
-      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("")
-      else
-        Failure("Writing reserved attributes not allowed : " + Join(badSeq, "\n"))
+    var keys := SortedSets.ComputeSetToOrderedSequence2(item.Keys, CharLess);
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    var rp := ReservedPrefix; // because the constant ReservedPrefix is actual an expensive function call
+    for i : uint64 := 0 to |keys| as uint64
+      invariant forall j | 0 <= j < i :: !(ReservedPrefix <= keys[j])
+    {
+      if rp <= keys[i] {
+        var result := "Writing reserved attributes not allowed : ";
+        for j : uint64 := i to |keys| as uint64 {
+          if rp <= keys[i] {
+            result := result + keys[i] + "\n";
+          }
+        }
+        return Failure(result);
+      }
+    }
+    return Success(true);
   }
 
   function method GetEncryptedAttributes(
@@ -83,7 +91,8 @@ module DynamoDBSupport {
   {
     if expr.Some? then
       var attrs := GetEncryptedAttributes(actions, expr, attrNames);
-      if |attrs| == 0 then
+      SequenceIsSafeBecauseItIsInMemory(attrs);
+      if |attrs| as uint64 == 0 then
         Success(true)
       else
         Failure("Condition Expressions forbidden on encrypted attributes : " + Join(attrs, ","))
@@ -121,7 +130,8 @@ module DynamoDBSupport {
     if expr.Some? then
       var attrs := Update.ExtractAttributes(expr.value, attrNames);
       var encryptedAttrs := Seq.Filter(s => IsSigned(actions, s), attrs);
-      if |encryptedAttrs| == 0 then
+      SequenceIsSafeBecauseItIsInMemory(encryptedAttrs);
+      if |encryptedAttrs| as uint64 == 0 then
         Success(true)
       else
         Failure("Update Expressions forbidden on signed attributes : " + Join(encryptedAttrs, ","))
@@ -169,11 +179,13 @@ module DynamoDBSupport {
       //# if the constructed compound beacon does not match
       //# the existing attribute value AddSignedBeacons MUST fail.
       var badAttrs := set k <- newAttrs | k in item && item[k] != newAttrs[k] :: k;
-      :- Need(|badAttrs| == 0, E("Signed beacons have generated values different from supplied values."));
+      SetIsSafeBecauseItIsInMemory(badAttrs);
+      :- Need(|badAttrs| as uint64 == 0, E("Signed beacons have generated values different from supplied values."));
       var version : DDB.AttributeMap := map[VersionTag := DS(" ")];
       var both := newAttrs.Keys * item.Keys;
       var bad := set k <- both | newAttrs[k] != item[k];
-      if 0 < |bad| {
+      SetIsSafeBecauseItIsInMemory(bad);
+      if 0 < |bad| as uint64 {
         // 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, ", ")));
@@ -254,7 +266,8 @@ module DynamoDBSupport {
         req.FilterExpression,
         req.ExpressionAttributeNames,
         req.ExpressionAttributeValues);
-      :- Need(|newItems| < INT32_MAX_LIMIT, DynamoDbEncryptionUtil.E("This is impossible."));
+      SequenceIsSafeBecauseItIsInMemory(newItems);
+      :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible."));
       var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems);
       var count :=
         if resp.Count.Some? then
@@ -323,7 +336,8 @@ module DynamoDBSupport {
         req.FilterExpression,
         req.ExpressionAttributeNames,
         req.ExpressionAttributeValues);
-      :- Need(|newItems| < INT32_MAX_LIMIT, DynamoDbEncryptionUtil.E("This is impossible."));
+      SequenceIsSafeBecauseItIsInMemory(newItems);
+      :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible."));
       var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems);
       var count :=
         if resp.Count.Some? then
@@ -344,14 +358,15 @@ module DynamoDBSupport {
     requires forall x <- results :: x in bv.virtualFields
     ensures output.Success? ==> forall x <- output.value :: x in bv.virtualFields
   {
-    if |fields| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(fields);
+    if |fields| as uint64 == 0 then
       Success(results)
     else
-      var optValue :- GetVirtField(bv.virtualFields[fields[0]], item);
+      var optValue :- GetVirtField(bv.virtualFields[fields[0 as uint32]], item);
       if optValue.Some? then
-        GetVirtualFieldsLoop(fields[1..], bv, item, results[fields[0] := optValue.value])
+        GetVirtualFieldsLoop(fields[1 as uint32..], bv, item, results[fields[0 as uint32] := optValue.value])
       else
-        GetVirtualFieldsLoop(fields[1..], bv, item, results)
+        GetVirtualFieldsLoop(fields[1 as uint32..], bv, item, results)
   }
 
   method GetVirtualFields(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap)
@@ -371,18 +386,19 @@ module DynamoDBSupport {
     requires forall x <- results :: x in bv.beacons
     ensures output.Success? ==> forall x <- output.value :: x in bv.beacons
   {
-    if |fields| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(fields);
+    if |fields| as uint64  == 0 then
       Success(results)
     else
-      var beacon := bv.beacons[fields[0]];
+      var beacon := bv.beacons[fields[0 as uint32]];
       if beacon.Compound? then
         var optValue :- beacon.cmp.getNaked(item, bv.virtualFields);
         if optValue.Some? then
-          GetCompoundBeaconsLoop(fields[1..], bv, item, results[fields[0] := optValue.value])
+          GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results[fields[0] := optValue.value])
         else
-          GetCompoundBeaconsLoop(fields[1..], bv, item, results)
+          GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results)
       else
-        GetCompoundBeaconsLoop(fields[1..], bv, item, results)
+        GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results)
   }
 
   method GetCompoundBeacons(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap)