feat: more test vectors

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

@@ -160,7 +160,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     DDBEncode(SE.ATTR_PREFIX + k)
   }
 
-  function method MakeEncryptionContext(
+  function method MakeEncryptionContextForEncrypt(
     config : InternalConfig,
     item : DynamoToStruct.TerminalDataMap)
     : (ret : Result<CMP.EncryptionContext, Error>)
@@ -179,6 +179,36 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       MakeEncryptionContextV1(config, item)
   }
 
+  function method MakeEncryptionContextForDecrypt(
+    config : InternalConfig,
+    header : seq<uint8>,
+    item : DynamoToStruct.TerminalDataMap)
+    : (ret : Result<CMP.EncryptionContext, Error>)
+    requires 0 < |header|
+    ensures ret.Success? ==>
+              //= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
+              //= type=implication
+              //# If the Version Number is 2, then the base context MUST be the [version 2](./encrypt-item.md#dynamodb-item-base-context-version-2) context.
+              && (header[0] == 2 ==> ret == MakeEncryptionContextV2(config, item))
+                 //= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
+                 //= type=implication
+                 //# If the Version Number is 1, the base context MUST be the [version 1](./encrypt-item.md#dynamodb-item-base-context-version-1) context.
+              && (header[0] == 1 ==> ret == MakeEncryptionContextV1(config, item))
+              && ((header[0] == 1) || (header[0] == 2))
+
+    //= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
+    //= type=implication
+    //# If the Version Number is not 1 or 2, the operation MUST return an error.
+    ensures ((header[0] != 1) && (header[0] != 2)) ==> ret.Failure?
+  {
+    if header[0] == 2 then
+      MakeEncryptionContextV2(config, item)
+    else if header[0] == 1 then
+      MakeEncryptionContextV1(config, item)
+    else
+      Failure(E("Header attribute has unexpected version number"))
+  }
+
   function method {:opaque} {:vcs_split_on_every_assert} MakeEncryptionContextV1(
     config : InternalConfig,
     item : DynamoToStruct.TerminalDataMap)
@@ -770,9 +800,9 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
         //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
         //= type=implication
         //# - Encryption Context MUST be this input Item's [DynamoDB Item Base Context](#dynamodb-item-base-context).
-        && MakeEncryptionContext(config, plaintextStructure).Success?
+        && MakeEncryptionContextForEncrypt(config, plaintextStructure).Success?
         && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.encryptionContext
-           == Some(MakeEncryptionContext(config, plaintextStructure).value)
+           == Some(MakeEncryptionContextForEncrypt(config, plaintextStructure).value)
 
         && output.value.parsedHeader.Some?
         && var structuredEncParsed := Seq.Last(config.structuredEncryption.History.EncryptStructure).output.value.parsedHeader;
@@ -847,7 +877,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
 
     var plaintextStructure :- DynamoToStruct.ItemToStructured(input.plaintextItem)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
-    var context :- MakeEncryptionContext(config, plaintextStructure);
+    var context :- MakeEncryptionContextForEncrypt(config, plaintextStructure);
     var cryptoSchema :- ConfigToCryptoSchema(config, input.plaintextItem)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
     var wrappedStruct := CSE.StructuredData(
@@ -977,12 +1007,25 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
                 content := CSE.StructuredDataContent.DataMap(plaintextStructure),
                 attributes := None)
 
+        //= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
+        //= type=implication
+        //# The item to be encrypted MUST have an attribute named `aws_dbe_head`.
+        && SE.HeaderField in input.encryptedItem
+        && var header := input.encryptedItem[SE.HeaderField];
+
+        //= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
+        //= type=implication
+        //# The attribute named `aws_dbe_head` MUST be of type `B` Binary.
+        && header.B?
+        && 0 < |header.B|
+
         //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
         //= type=implication
         //# - Encryption Context MUST be the input Item's [DynamoDB Item Base Context](./encrypt-item.md#dynamodb-item-base-context).
-        && MakeEncryptionContext(config, plaintextStructure).Success?
+        && MakeEncryptionContextForDecrypt(config, header.B, plaintextStructure).Success?
+
         && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.encryptionContext
-           == Some(MakeEncryptionContext(config, plaintextStructure).value)
+           == Some(MakeEncryptionContextForDecrypt(config, header.B, plaintextStructure).value)
 
         //= specification/dynamodb-encryption-client/decrypt-item.md#output
         //= type=implication
@@ -1077,7 +1120,12 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
 
     var encryptedStructure :- DynamoToStruct.ItemToStructured(input.encryptedItem)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
-    var context :- MakeEncryptionContext(config, encryptedStructure);
+    :- Need(SE.HeaderField in input.encryptedItem, E("header field not in item."));
+    var header := input.encryptedItem[SE.HeaderField];
+    :- Need(header.B?, E("Header field not binary"));
+    assert header.B?;
+    :- Need(0 < |header.B|, E("Unexpected empty header field."));
+    var context :- MakeEncryptionContextForDecrypt(config, header.B, encryptedStructure);
     var authenticateSchema := ConfigToAuthenticateSchema(config, input.encryptedItem);
     var wrappedStruct := CSE.StructuredData(
       content := CSE.StructuredDataContent.DataMap(encryptedStructure),
@@ -1088,7 +1136,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     //# [Required Encryption Context CMM](https://github.com/awslabs/private-aws-encryption-sdk-specification-staging/blob/dafny-verified/framework/required-encryption-context-cmm.md)
     //# with the following inputs:
     //# - This item encryptor's [CMM](./ddb-table-encryption-config.md#cmm) as the underlying CMM.
-    //# - The keys from the [DynamoDB Item Base Context](./encrypt-item.md#dynamodb-item-base-context).
+    //# - The keys from the [DynamoDB Item Base Context](#dynamodb-item-base-context).
 
     var reqCMMR := config.cmpClient.CreateRequiredEncryptionContextCMM(
       CMP.CreateRequiredEncryptionContextCMMInput(

TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy

@@ -53,7 +53,6 @@ module {:options "-functionSyntax:4"} DecryptManifest {
   method OneTest(name : string, value : JSON) returns (output : Result<bool, string>)
   {
     :- Need(value.Object?, "Test must be an object");
-    print "Decrypting ", name, "\n";
 
     var types : Option<string> := None;
     var description : Option<string> := None;
@@ -99,6 +98,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
 
   method Decrypt(inFile : string) returns (output : Result<bool, string>)
   {
+    print "Decrypt : ", inFile, "\n";
     var configBv :- expect FileIO.ReadBytesFromFile(inFile);
     var configBytes := BvToBytes(configBv);
     var json :- expect API.Deserialize(configBytes);

TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy

@@ -82,7 +82,6 @@ module {:options "-functionSyntax:4"} EncryptManifest {
   method OneTest(name : string, value : JSON) returns (output : Result<Option<(string, JSON)>, string>)
   {
     :- Need(value.Object?, "Test must be an object");
-    print "Examining ", name, "\n";
 
     var types : Option<string> := None;
     var description : Option<string> := None;
@@ -132,6 +131,8 @@ module {:options "-functionSyntax:4"} EncryptManifest {
 
   method Encrypt(inFile : string, outFile : string, lang : string, version : string) returns (output : Result<bool, string>)
   {
+    print "Encrypt : ", inFile, "\n";
+
     var configBv :- expect FileIO.ReadBytesFromFile(inFile);
     var configBytes := BvToBytes(configBv);
     var json :- expect API.Deserialize(configBytes);

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

@@ -90,8 +90,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json");
       var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json");
       var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json");
+      var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json");
+      var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json");
       var _ :- expect WriteManifest.Write("encrypt.json");
-      var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.2");
+      var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3");
       var _ :- expect DecryptManifest.Decrypt("decrypt.json");
       if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
         print "\nRunning no tests\n";

TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy

@@ -98,14 +98,24 @@ module {:options "-functionSyntax:4"} WriteManifest {
         },
         ""allowedUnsignedAttributes"" : [""Stuff"", ""Junk""]
       }"
-    
+
   method TextToJson(x: string) returns (output : JSON)
   {
     var str :- expect UTF8.Encode(x);
     var json :- expect API.Deserialize(str);
     return json;
   }
 
+  const QUOTE : string := "\""
+
+  const ConfigRecord :=
+    "{\"RecNum\": 1,"
+    +  QUOTE + Attr1 + QUOTE + ": \"aaa\","
+    +  QUOTE + Attr2 + QUOTE + ": {\"M\" : {\"A\":\"B\", \"C\":\"D\"}},"
+    +  QUOTE + Attr3 + QUOTE + ":  {\"L\" : [{\"M\" : {\"A\":\"B\", \"C\":\"D\"}}, {\"NS\":[\"00.0011\", \"0000\", \"2000.000\", \"10.01\"]}, {\"SS\":[\"00.0011\", \"0000\", \"2000.000\", \"10.01\"]}]},"
+    +  QUOTE + Attr4 + QUOTE + ": {\"SS\":[\"00.0011\", \"0000\", \"2000.000\", \"10.01\"]},"
+    +  QUOTE + Attr5 + QUOTE + ": {\"NS\":[\"00.0011\", \"0000\", \"2000.000\", \"10.01\"]}}"
+
   const BasicRecord := @"{
           ""RecNum"": 1,
           ""Stuff"": ""StuffData"",
@@ -122,11 +132,11 @@ module {:options "-functionSyntax:4"} WriteManifest {
         }"
 
   method MakeTest(
-    name : string, 
-    typ : string, 
-    desc : string, 
-    configJson : string, 
-    recordJson : string, 
+    name : string,
+    typ : string,
+    desc : string,
+    configJson : string,
+    recordJson : string,
     decryptConfigJson : Option<string> :=  None) returns (output : (string, JSON))
   {
     var config := TextToJson(configJson);
@@ -145,8 +155,164 @@ module {:options "-functionSyntax:4"} WriteManifest {
     return(name, Object(result));
   }
 
+  type CryptoAction = x : int | 0 <= x < 4
+  type CryptoActions = x : seq<CryptoAction> | |x| == 6 witness [0,0,0,0,0,0]
+  const CryptoActionStr : seq<string> := ["0", "1", "2", "3"]
+  const MyActionNames : seq<string> := ["ENCRYPT_AND_SIGN", "SIGN_ONLY", "SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT", "DO_NOTHING"]
+  const Encrypt : CryptoAction := 0
+  const SignOnly : CryptoAction := 1
+  const SignInclude : CryptoAction := 2
+  const DoNothing : CryptoAction := 3
+
+  const A : string := "A"
+  const B : string := "퀀" // Ud000"
+  const C : string := "﹌" // Ufe4c"
+  const D : string := "𐀁" // U10001
+  const E : string := "𐀂" // U10002 - same high surrogate as D
+  const F : string := "𠀂" // U20002 - different high surrogate as D
+
+  lemma CheckLengths()
+    ensures |A| == 1
+    ensures |B| == 1
+    ensures |C| == 1
+    ensures |D| == 2
+    ensures |E| == 2
+    ensures |F| == 2
+  {}
+
+  // Let's make attribute names with complex characters.
+  // It shouldn't matter, but let's make sure
+  const Attr1 : string  := F+D
+  const Attr2 : string  := A+B+C+D
+  const Attr3 : string  := E+D
+  const Attr4 : string  := C+D
+  const Attr5 : string  := D+C+B+A
+  const MyAttrNames : seq<string> := ["RecNum", Attr1, Attr2, Attr3, Attr4, Attr5]
+
+
+  method MakeConfig(actions : CryptoActions) returns (output : JSON)
+    ensures output.Object?
+  {
+    var configActions : seq<(string, JSON)> := [];
+    var notSigned : seq<JSON> := [];
+    for i := 0 to 6 {
+      var myAction : CryptoAction := actions[i];
+      configActions := configActions + [(MyAttrNames[i], String(MyActionNames[myAction]))];
+      if myAction == DoNothing {
+        notSigned := notSigned + [String(MyAttrNames[i])];
+      }
+    }
+    var result : seq<(string, JSON)> := [
+      ("attributeActionsOnEncrypt", Object(configActions)),
+      ("allowedUnsignedAttributes", Array(notSigned))
+    ];
+
+    return Object(result);
+  }
+
+  method MakeConfigTest(
+    name : string,
+    config : JSON,
+    record : JSON,
+    decryptConfigJson : Option<JSON> :=  None) returns (output : (string, JSON))
+  {
+    var result : seq<(string, JSON)> :=
+      [
+        ("type", String("positive-encrypt")),
+        ("description", String("config test")),
+        ("config", config),
+        ("record", record)
+      ];
+    if decryptConfigJson.Some? {
+      var decryptConfig := decryptConfigJson.value;
+      result := result + [("decryptConfig", decryptConfig)];
+    }
+    return(name, Object(result));
+  }
+
+  function Increment(x : CryptoActions) : CryptoActions
+  {
+    if x[5] < 3 then
+      [x[0], x[1], x[2], x[3], x[4], x[5]+1]
+    else if x[4] < 3 then
+      [x[0], x[1], x[2], x[3], x[4]+1, 0]
+    else if x[3] < 3 then
+      [x[0], x[1], x[2], x[3]+1, 0, 0]
+    else if x[2] < 3 then
+      [x[0], x[1], x[2]+1, 0, 0, 0]
+    else if x[1] < 3 then
+      [x[0], x[1]+1, 0, 0, 0, 0]
+    else if x[0] < 3 then
+      [x[0]+1, 0, 0, 0, 0, 0]
+    else
+      [0, 0, 0, 0, 0, 0]
+  }
+
+  predicate IsConsistent(actions : CryptoActions)
+  {
+    if actions[0] in [DoNothing, Encrypt] then
+      false
+    else if actions[0] == SignOnly && (exists x | x in actions :: x == SignInclude) then
+      false
+    else
+      true
+  }
+
+  predicate IsConsistentWith(oldActions : CryptoActions, newActions : CryptoActions)
+  {
+    if !IsConsistent(oldActions) || !IsConsistent(newActions) then
+      false
+    else
+      !exists i | 0 <= i < 6 :: (oldActions[i] == DoNothing) != (newActions[i] == DoNothing)
+  }
+
+  // make a test for every valid combination of Crypto Actions
+  method MakeConfigTests() returns (output : seq<(string, JSON)>)
+  {
+    var actions : CryptoActions := [0,0,0,0,0,0];
+    var result : seq<(string, JSON)> := [];
+    var record := TextToJson(ConfigRecord);
+    var actionWrittenOuter := 0;
+    var actionWrittenInner := 0;
+    for i := 0 to 4096 {
+      actions := Increment(actions);
+      if IsConsistent(actions) {
+        var name := "ConfigTest_";
+        for j := 0 to 6 {
+          name := name + CryptoActionStr[actions[j]];
+        }
+        var config := MakeConfig(actions);
+        var theTest := MakeConfigTest(name, config, record);
+        result := result + [theTest];
+        actionWrittenOuter := actionWrittenOuter + 1;
+
+        // for a subset of these,
+        // make a test to decrypt with every possible valid combination of Crypto Actions
+        if (actionWrittenOuter % 100) == 0 {
+          var otherActions : CryptoActions := [0,0,0,0,0,0];
+          for j := 0 to 4096 {
+            otherActions := Increment(otherActions);
+            if IsConsistentWith(actions, otherActions) {
+              var newConfig := MakeConfig(otherActions);
+              var newName := name + "_";
+              for k := 0 to 6 {
+                newName := newName + CryptoActionStr[otherActions[k]];
+              }
+              var newTest := MakeConfigTest(newName, config, record, Some(newConfig));
+              result := result + [newTest];
+              actionWrittenInner := actionWrittenInner + 1;
+            }
+          }
+        }
+      }
+    }
+    print "MakeConfigTests : ", actionWrittenOuter, " outer and ", actionWrittenInner, " inner for ", |result|, " total.\n";
+    return result;
+  }
+
   method Write(fileName : string) returns (output : Result<bool, string>)
   {
+    print "Write : ", fileName, "\n";
     var result : seq<(string, JSON)> :=
       [Manifest(), ("keys", String("file://keys.json"))];
 
@@ -163,7 +329,8 @@ module {:options "-functionSyntax:4"} WriteManifest {
     var test11 := MakeTest("11", "positive-encrypt", "Basic encrypt V2", BasicV2Config, BasicRecord);
     var test12 := MakeTest("12", "positive-encrypt", "Basic encrypt V2 switching1", LongerV2Config1, BasicRecord, Some(LongerV2Config2));
     var test13 := MakeTest("13", "positive-encrypt", "Basic encrypt V2 switching2", LongerV2Config2, BasicRecord, Some(LongerV2Config1));
-    var tests : seq<(string, JSON)> := [test1, test2, test3, test4, test5, test6, test7, test8, test9, test10, test11, test12, test13];
+    var configTests := MakeConfigTests();
+    var tests : seq<(string, JSON)> := [test1, test2, test3, test4, test5, test6, test7, test8, test9, test10, test11, test12, test13] + configTests;
     var final := Object(result + [("tests", Object(tests))]);
 
     var jsonBytes :- expect API.Serialize(final);