m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

@@ -9,6 +9,7 @@ include "DDBSupport.dfy"
 include "DynamoDbEncryptionBranchKeyIdSupplier.dfy"
 include "DynamoToStruct.dfy"
 include "FilterExpr.dfy"
+include "MemoryMath.dfy"
 include "NormalizeNumber.dfy"
 include "SearchInfo.dfy"
 include "TermLoc.dfy"

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy

@@ -0,0 +1,35 @@
+// When dealing with actual data in actual memory, we can be confident that
+// none of the numbers will exceed an exabyte, so we can use uint64, rather than nat.
+// To convince Dafny that this is true, we have the following functions
+// with assumptions as needed.
+
+
+include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy"
+
+module {:options "--function-syntax:4"} MemoryMath {
+
+  import opened BoundedInts
+
+
+  // This is safe because it is being held in memory
+  lemma {:axiom} ValueIsSafeBecauseItIsInMemory(value : nat)
+    ensures value < UINT64_MAX as nat
+
+  function {:opaque} Add(x : uint64, y : uint64) : (ret : uint64)
+    ensures ret < UINT64_MAX as uint64
+    ensures ret as nat == x as nat + y as nat
+  {
+    ValueIsSafeBecauseItIsInMemory(x as nat + y as nat);
+    x + y
+  }
+
+  function {:opaque} Add3(x : uint64, y : uint64, z : uint64) : (ret : uint64)
+    ensures ret < UINT64_MAX as uint64
+    ensures ret as nat == x as nat + y as nat + z as nat
+  {
+    ValueIsSafeBecauseItIsInMemory(x as nat + y as nat + z as nat);
+    x + y + z
+  }
+
+
+}

DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy

@@ -14,7 +14,7 @@ module DynamoDbEncryptionUtil {
   const BeaconPrefix := "aws_dbe_b_"
   const VersionPrefix := "aws_dbe_v_"
 
-  const MAX_STRUCTURE_DEPTH : uint32 := 32
+  const MAX_STRUCTURE_DEPTH : uint64 := 32
   const MAX_STRUCTURE_DEPTH_STR := "32"
 
   type HmacKeyMap = map<string, Bytes>

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy

@@ -14,11 +14,11 @@ module DynamoDbItemEncryptorUtil {
   import SortedSets
   import SE = StructuredEncryptionUtil
   import DynamoToStruct
+  import MemoryMath
 
   const ReservedPrefix := "aws_dbe_"
   const BeaconPrefix := ReservedPrefix + "b_"
   const VersionPrefix := ReservedPrefix + "v_"
-  const UINT32_MAX : uint32 := 0xFFFF_FFFF
 
   function method E(msg : string) : Error
   {
@@ -181,8 +181,8 @@ module DynamoDbItemEncryptorUtil {
       Success(value)
     else if legend == SE.LEGEND_BINARY then
       var terminal :- SE.DecodeTerminal(ecValue);
-      :- Need(|terminal.value| < UINT32_MAX as int, "LEGEND_BINARY too big");
-      var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32));
+      MemoryMath.ValueIsSafeBecauseItIsInMemory(|terminal.value|);
+      var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint64));
       Success(ddbAttrValue.val)
     else
       Failure("Encryption Context Legend has unexpected character : '" + [legend] + "'.")
@@ -237,8 +237,8 @@ module DynamoDbItemEncryptorUtil {
 
     // Obtain attribute value from EC kvPair value
     var terminal :- SE.DecodeTerminal(encodedAttrValue);
-    :- Need(|terminal.value| < UINT32_MAX as int, "Attribute Value too big");
-    var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32));
+    MemoryMath.ValueIsSafeBecauseItIsInMemory(|terminal.value|);
+    var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint64));
 
     // Add to our AttributeMap
     Success(attrMap[ddbAttrName := ddbAttrValue.val])