feat: more test vectors (#959)

* feat(TestVectors): extensive configuration coverage

Author: ajewellamz

.github/workflows/ci_todos.yml

@@ -17,8 +17,8 @@ jobs:
         shell: bash
         # TODOs may be committed as long as the same line contains a link to a Github Issue or refers to a CrypTool SIM.
         run: |
-          ALL_TODO_COUNT=$( { grep -r "TODO" . --exclude-dir=./submodules --exclude-dir=./.git --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
-          GOOD_TODO_COUNT=$( { grep -r "TODO.*\(github.com\/.*issues.*\/[1-9][0-9]*\|CrypTool-[1-9][0-9]*\)" . --exclude-dir=./submodules --exclude-dir=./.git  --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
+          ALL_TODO_COUNT=$( { grep -r "TODO" . --exclude-dir=./TestVectors/runtimes --exclude-dir=./submodules --exclude-dir=./.git --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
+          GOOD_TODO_COUNT=$( { grep -r "TODO.*\(github.com\/.*issues.*\/[1-9][0-9]*\|CrypTool-[1-9][0-9]*\)" . --exclude-dir=./submodules --exclude-dir=./.git  --exclude-dir=./TestVectors/runtimes --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
           if [ "$ALL_TODO_COUNT" != "$GOOD_TODO_COUNT" ]; then
             exit 1;
           fi

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, \"aws_dbe_head\", not in item."));
+    var header := input.encryptedItem[SE.HeaderField];
+    :- Need(header.B?, E("Header field, \"aws_dbe_head\", 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/README.md

@@ -18,6 +18,28 @@ This validates the Database Encryption SDK's cross-version compatibility.
 1. Start in the root `./TestVectors` directory
 2. Run `make build_java`
 3. Run `make test_java`
+4. Run `make transpile_net`
+5. Run `cd runtimes/net`
+6. Run `dotnet run --framework net6.0`
+
+### Saving results for later
+
+Running the above commands will create `runtimes/java/decrypt.json` and `runtimes/net/decrypt.json`.
+
+These files should be permanently saved before a release.
+
+For example, if we're on version 3.4 and are getting close to a new release, we would
+
+`cp runtimes/java/decrypt.json runtimes/java/decrypt_java_34.json`
+
+`cp runtimes/net/decrypt.json runtimes/java/decrypt_dotnet_34.json`
+
+and then modify `RunAllTests` in `dafny/DDBEncryption/src/TestVectors.dfy` to explicitly check these two files.
+
+As other languages are supported, we will also deal with runtimes/XXX/decrypt.json and runtimes/java/decrypt_XXX_34.json
+in a simlar manner.
+
+This ensures that records written in any version in any language can be read by the current version in any language.
 
 ## Security
 

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,7 @@ 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";