m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

@@ -31,12 +31,12 @@ module DynamoToStruct {
     // var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();
     // return MakeError("Not valid attribute names : ");
 
-    var structuredMap := map k <- item | (k in actions && actions[k] != DO_NOTHING) || (ReservedPrefix <= k) :: k := AttrToStructured(item[k]);
+    var structuredMap := map k <- item | k !in actions || actions[k] != DO_NOTHING || ReservedPrefix <= k :: k := AttrToStructured(item[k]);
     MapKeysMatchItems(item);
     MapError(SimplifyMapValue(structuredMap))
   }
 
-  function method StructuredToItem2(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
+  function method StructuredToItemEncrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
   {
     var ddbMap := map k <- orig :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]);
     MapKeysMatchItems(orig);
@@ -49,6 +49,13 @@ module DynamoToStruct {
     Success(oldMap + newMap)
   }
 
+  function method StructuredToItemDecrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
+  {
+    var ddbMap := map k <- orig | !(ReservedPrefix <= k) :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]);
+    MapKeysMatchItems(orig);
+    MapError(SimplifyMapValue(ddbMap))
+  }
+
   // This file exists for these two functions : ItemToStructured and StructuredToItem
   // which provide conversion between an AttributeMap and a StructuredDataMap
 
@@ -405,7 +412,7 @@ module DynamoToStruct {
               && ListAttrToBytes(a.L, depth).Success?
               && ret.value[PREFIX_LEN..] == ListAttrToBytes(a.L, depth).value
               && ListAttrToBytes(a.L, depth).value[..LENGTH_LEN] == U32ToBigEndian(|a.L|).value
-              // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value
+                 // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value
               && (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN)
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-attribute

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

@@ -889,7 +889,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e)));
     var encryptedData := encryptVal.encryptedStructure;
     :- Need(forall k <- encryptedData :: DDB.IsValid_AttributeName(k), E(""));
-    var ddbKey :- DynamoToStruct.StructuredToItem2(encryptedData, input.plaintextItem, config.attributeActionsOnEncrypt)
+    var ddbKey :- DynamoToStruct.StructuredToItemEncrypt(encryptedData, input.plaintextItem, config.attributeActionsOnEncrypt)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
 
     var parsedActions :- ConvertCryptoSchemaToAttributeActions(config, encryptVal.cryptoSchema);
@@ -1112,7 +1112,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e)));
     var decryptedData := decryptVal.plaintextStructure;
     :- Need(forall k <- decryptedData :: DDB.IsValid_AttributeName(k), E(""));
-    var ddbItem :- DynamoToStruct.StructuredToItem2(decryptedData, input.encryptedItem, decryptVal.cryptoSchema)
+    var ddbItem :- DynamoToStruct.StructuredToItemDecrypt(decryptedData, input.encryptedItem, decryptVal.cryptoSchema)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
 
     var schemaToConvert := decryptVal.cryptoSchema;

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy

@@ -109,7 +109,6 @@ module DynamoDbItemEncryptorTest {
       "sign4" := DDB.AttributeValue.NULL(true),
       "nothing" := DDBS("baz")
     ];
-    var expectedOutputItem := inputItem["bar" := DDB.AttributeValue.N("1234")];
 
     var encryptRes := encryptor.EncryptItem(
       Types.EncryptItemInput(
@@ -122,7 +121,7 @@ module DynamoDbItemEncryptorTest {
     }
     expect encryptRes.Success?;
     expect encryptRes.value.encryptedItem.Keys == inputItem.Keys + {SE.HeaderField, SE.FooterField};
-    expect encryptRes.value.encryptedItem["bar"] == expectedOutputItem["bar"]; // because normalized
+    expect encryptRes.value.encryptedItem["bar"] == inputItem["bar"];
     expect encryptRes.value.encryptedItem["encrypt"] != inputItem["encrypt"];
     expect encryptRes.value.encryptedItem["sign"] == inputItem["sign"];
     expect encryptRes.value.encryptedItem["sign3"] == inputItem["sign3"];
@@ -142,11 +141,11 @@ module DynamoDbItemEncryptorTest {
       print "\n", decryptRes.error, "\n";
     }
     expect decryptRes.Success?;
-    if decryptRes.value.plaintextItem != expectedOutputItem {
-      print "\nexpectedOutputItem :\n", expectedOutputItem, "\n";
+    if decryptRes.value.plaintextItem != inputItem {
+      print "\ninputItem :\n", inputItem, "\n";
       print "\nOutput Item :\n", decryptRes.value.plaintextItem, "\n";
     }
-    expect decryptRes.value.plaintextItem == expectedOutputItem;
+    expect decryptRes.value.plaintextItem == inputItem;
 
     var parsedHeader := decryptRes.value.parsedHeader;
     expect parsedHeader.Some?;