test: add support for legacy test vectors

.github/workflows/library_legacy_interop_test_vectors.yml

@@ -0,0 +1,135 @@
+# This workflow performs legacy test vector tests across the supported runtimes of the ESDK Dafny
+name: Library Interoperability Dafny TestVectors
+
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to use"
+        required: true
+        type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
+
+jobs:
+  decryptEncryptVectors:
+    strategy:
+      matrix:
+        library: [TestVectors]
+        os: [
+            # https://taskei.amazon.dev/tasks/CrypTool-5283
+            # windows-latest,
+            ubuntu-latest,
+            macos-13,
+          ]
+        # java struggles with the json parsing
+        # however; the native java esdk already runs a subset of these decrypt
+        # vectors. More important for the dafny-x implementations to be able
+        # to decrypt these
+        language: [net]
+        legacy_zips: [
+          aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5,
+          aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.7,
+          aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.8,
+          aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-2.0.0,
+          aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-2.2.0,
+          aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-2.3.0
+        ]
+        # https://taskei.amazon.dev/tasks/CrypTool-5284
+        dotnet-version: ["6.0.x"]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+
+    steps:
+        - name: Support longpaths on Git checkout
+          run: |
+            git config --global core.longpaths true
+
+        - uses: actions/checkout@v3
+          with:
+            submodules: true
+        #  Not all submodules are needed.
+        # We manually pull the submodule we DO need.
+        - run: git submodule update --init libraries
+        - run: git submodule update --init --recursive mpl
+
+        # Set up runtimes
+        - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
+          if: matrix.language == 'net'
+          uses: actions/setup-dotnet@v3
+          with:
+            dotnet-version: ${{ matrix.dotnet-version }}
+
+        - name: Setup Java 17
+          if: matrix.language == 'java'
+          uses: actions/setup-java@v3
+          with:
+            distribution: "corretto"
+            java-version: 17
+
+        - name: Setup Dafny
+          uses: dafny-lang/[email protected]
+          with:
+            dafny-version: ${{ inputs.dafny }}
+
+        - name: Regenerate code using smithy-dafny if necessary
+          if: ${{ inputs.regenerate-code }}
+          uses: ./.github/actions/polymorph_codegen
+          with:
+            dafny: ${{ inputs.dafny }}
+            library: ${{ matrix.library }}
+            diff-generated-code: false
+
+        # Build implementation for each runtime
+        - name: Build ${{ matrix.library }} implementation in Java
+          if: matrix.language == 'java'
+          shell: bash
+          working-directory: ./${{ matrix.library }}
+          run: |
+            # This works because `node` is installed by default on GHA runners
+            CORES=$(node -e 'console.log(os.cpus().length)')
+            make build_java CORES=$CORES
+
+        - name: Build ${{ matrix.library }} implementation in .NET
+          if: matrix.language == 'net'
+          shell: bash
+          working-directory: ./${{ matrix.library }}
+          run: |
+            # This works because `node` is installed by default on GHA runners
+            CORES=$(node -e 'console.log(os.cpus().length)')
+            make transpile_net
+
+        - name: Setup gradle
+          if: matrix.language == 'java'
+          uses: gradle/gradle-build-action@v2
+          with:
+            gradle-version: 7.2
+
+        # TestVectors will call KMS
+        - name: Configure AWS Credentials
+          uses: aws-actions/configure-aws-credentials@v2
+          with:
+            aws-region: us-west-2
+            role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 
+            role-session-name: LegacyInterOpTests
+
+        # Extract test vector zips
+        - name: Unzip legacy test vectors
+          working-directory: ./${{matrix.library}}
+          run: |
+            unzip ${{matrix.legacy_zips}}.zip -d ${{matrix.legacy_zips}}
+
+        # Test Legacy Vectors
+        - name: Test legacy vectors via CLI
+          working-directory: ./${{matrix.library}}
+          env:
+            MANIFEST_PATH: ${{matrix.legacy_zips}}/
+            MANIFEST_NAME: ${{ matrix.legacy_zips == 'aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5' && 'decrypt_message.json' || 'manifest.json'}}
+          run: |
+            make test_decrypt_encrypt_vectors_net_legacy
+

.github/workflows/pull.yml

@@ -29,3 +29,7 @@ jobs:
     uses: ./.github/workflows/library_interop_test_vectors.yml
     with:
       dafny: '4.8.1'
+  pr-dafny-legacy-test-vectors:
+    uses: ./.github/workflows/library_legacy_interop_test_vectors.yml
+    with:
+      dafny: '4.8.1'

TestVectors/Makefile

@@ -99,13 +99,19 @@ test_encrypt_vectors_net:
 	dotnet run --project runtimes/net --framework $(FRAMEWORK) encrypt --manifest-path runtimes/net --decrypt-manifest-path runtimes/net
 
 test_decrypt_encrypt_vectors_java:
-	gradle -p runtimes/java run --args="decrypt --manifest-path ."
+	gradle -p runtimes/java run --args="decrypt --manifest-path . --manifest-name decrypt-manifest.json"
 
 test_decrypt_encrypt_vectors_net: FRAMEWORK=net6.0
 test_decrypt_encrypt_vectors_net:
 	dotnet restore runtimes/net
 	dotnet build runtimes/net
-	dotnet run --project runtimes/net --framework $(FRAMEWORK) decrypt --manifest-path runtimes/net
+	dotnet run --project runtimes/net --framework $(FRAMEWORK) decrypt --manifest-path runtimes/net --manifest-name decrypt-manifest.json
+
+test_decrypt_encrypt_vectors_net_legacy: FRAMEWORK=net6.0
+test_decrypt_encrypt_vectors_net_legacy:
+	dotnet restore runtimes/net
+	dotnet build runtimes/net
+	dotnet run --project runtimes/net --framework $(FRAMEWORK) decrypt --manifest-path $(MANIFEST_PATH) --manifest-name $(MANIFEST_NAME)
 
 _polymorph_dependencies:
 	@echo "No polymorphing of dependency"

TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy

@@ -9,6 +9,7 @@ module {:options "-functionSyntax:4"} EsdkManifestOptions {
   datatype ManifestOptions =
     | Decrypt(
         nameonly manifestPath: string,
+        nameonly manifestFileName: string,
         nameonly testName: Option<string> := None
       )
     | Encrypt(

TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy

@@ -37,7 +37,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
     requires 0 < |op.manifestPath|
     requires Seq.Last(op.manifestPath) == '/'
   {
-    var decryptManifest :- expect GetManifest(op.manifestPath, "decrypt-manifest.json");
+    var decryptManifest :- expect GetManifest(op.manifestPath, op.manifestFileName);
     :- Need(decryptManifest.DecryptManifest?, "Not a decrypt manifest");
 
     var decryptVectors :- ParseEsdkJsonManifest.BuildDecryptTestVector(
@@ -73,7 +73,6 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
     {
       var vector := vectors[i];
       if TestDecryptVector?(vector) {
-        :- Need(vector.algorithmSuiteId.Some?, "Vector without algorithm suite defined.");
         var pass := EsdkTestVectors.TestDecrypt(keys, vector);
         if !pass {
           hasFailure := true;
@@ -251,7 +250,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
     var decryptManifestBv :- FileIO.ReadBytesFromFile(manifestPath + manifestFileName);
     var decryptManifestBytes := BvToBytes(decryptManifestBv);
     var manifestJson :- API.Deserialize(decryptManifestBytes)
-    .MapFailure(( e: Errors.DeserializationError ) => e.ToString());
+      .MapFailure(( e: Errors.DeserializationError ) => e.ToString());
     :- Need(manifestJson.Object?, "Not a JSON object");
 
     var manifest :- GetObject("manifest", manifestJson.obj);

TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy

@@ -55,7 +55,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
     || v == 4
   }
 
-  type SupportedEncryptVersion = v: nat | SupportedEncryptVersion?(v)  witness 4
+  type SupportedEncryptVersion = v: nat | SupportedEncryptVersion?(v)  witness 1
   predicate SupportedEncryptVersion?(v: nat)
   {
     || v == 1
@@ -151,6 +151,21 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
         description: string,
         decryptionMethod: DecryptionMethod
       )
+    | PositiveV1DecryptTestVector(
+        id: string,
+        version: SupportedDecryptVersion,
+        manifestPath: string,
+        ciphertextPath: string,
+        plaintextPath: string,
+        reproducedEncryptionContext: Option<mplTypes.EncryptionContext> := None,
+        requiredEncryptionContextKeys: Option<mplTypes.EncryptionContextKeys> := None,
+        decryptDescriptions: KeyVectorsTypes.KeyDescription,
+        commitmentPolicy: mplTypes.ESDKCommitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT,
+        frameLength: Option<int64>,
+        algorithmSuiteId: Option<mplTypes.AlgorithmSuiteInfo>,
+        description: string,
+        decryptionMethod: DecryptionMethod
+      )
 
   datatype DecryptionMethod =
     | StreamingUnsignedOnly
@@ -164,10 +179,13 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
     requires keys.ValidState()
     modifies keys.Modifies
     ensures keys.ValidState()
-    requires vector.algorithmSuiteId.Some?
   {
-    var id := AllAlgorithmSuites.ToHex(vector.algorithmSuiteId.value);
-    print "\nTEST-DECRYPT===> ", vector.id, "\n", id, " ", vector.description, "\n";
+    if vector.algorithmSuiteId.Some? {
+      var id := AllAlgorithmSuites.ToHex(vector.algorithmSuiteId.value);
+      print "\nTEST-DECRYPT===> ", vector.id, "\n", id, " ", vector.description, "\n";
+    } else {
+      print "\nTEST-DECRYPT===> ", vector.id, "\n", vector.description, "\n";
+    }
 
     // The decrypt test vectors also test initialization
     // This is because they were developed when the MPL
@@ -183,7 +201,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
 
     var ciphertext :- expect ReadVectorsFile(test.vector.manifestPath + test.vector.ciphertextPath);
     var plaintext;
-    if test.vector.PositiveDecryptTestVector? {
+    if test.vector.PositiveDecryptTestVector? || test.vector.PositiveV1DecryptTestVector? {
       plaintext :- expect ReadVectorsFile(test.vector.manifestPath + test.vector.plaintextPath);
     }
 
@@ -203,9 +221,13 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
         && result.value.plaintext == plaintext
       case NegativeDecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_)
         =>
-        && result.Failure?;
+        && result.Failure?
+      case PositiveV1DecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_)
+        =>
+        && result.Success?
+        && result.value.plaintext == plaintext;
     if !output {
-      if test.vector.PositiveDecryptTestVector? && result.Failure? {
+      if (test.vector.PositiveDecryptTestVector? || test.vector.PositiveV1DecryptTestVector?) && result.Failure? {
         print result.error, "\n";
         if
           && result.error.AwsCryptographyMaterialProviders?
@@ -218,7 +240,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
     }
   }
 
-  method DecryptVectorToDecryptTest(
+  method {:vcs_split_on_every_assert} DecryptVectorToDecryptTest(
     keys: KeyVectors.KeyVectorsClient,
     vector: EsdkDecryptTestVector
   )
@@ -233,14 +255,23 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
               && fresh(output.value.cmm.Modifies - keys.Modifies)
               && fresh(output.value.client.Modifies)
   {
+    :- Need(
+      !vector.NegativeDecryptTestVector?,
+      KeyVectorsTypes.KeyVectorException(message := "Negative Test Vectors not supported at this time")
+    );
     var cmm :- keys.CreateWrappedTestVectorCmm(
       KeyVectorsTypes.TestVectorCmmInput(
         keyDescription := vector.decryptDescriptions,
         forOperation := KeyVectorsTypes.DECRYPT
       ));
 
-    :- Need(vector.algorithmSuiteId.Some?, KeyVectorsTypes.KeyVectorException(message := "Missing AlgorithmSuiteId in test vector"));
-    var commitmentPolicy := AllAlgorithmSuites.GetCompatibleCommitmentPolicy(vector.algorithmSuiteId.value);
+    var commitmentPolicy := if vector.algorithmSuiteId.Some? then
+      AllAlgorithmSuites.GetCompatibleCommitmentPolicy(vector.algorithmSuiteId.value)
+    else
+      // If the manifest does not contain a field for the algorithm suite then we default the
+      // commitment policy to FORBID_ENCRYPT_ALLOW_DECRYPT. This is currently only triggered
+      // when we read v1 manifests.
+      mplTypes.CommitmentPolicy.ESDK(mplTypes.ESDKCommitmentPolicy.FORBID_ENCRYPT_ALLOW_DECRYPT);
     :- Need(commitmentPolicy.ESDK?, KeyVectorsTypes.KeyVectorException(message := "Compatible commitment policy is not for ESDK"));
 
     var config := WrappedESDK.WrappedAwsEncryptionSdkConfigWithSuppliedCommitment(

TestVectors/dafny/TestVectors/src/Index.dfy

@@ -21,6 +21,7 @@ module {:options "-functionSyntax:4"} WrappedESDKMain {
                                    Param.Command(Options("decrypt", "decrypt command for test-vectors",
                                                          [
                                                            Param.Opt("manifest-path", "relative path to the location of the manifest", unused := Required),
+                                                           Param.Opt("manifest-name", "name of file that contains the decrypt vectors file", unused := Required),
                                                            Param.Opt("test-name", "id of the test to run")
                                                          ])),
                                    Param.Command(Options("encrypt", "encrypt command for test-vectors",
@@ -50,7 +51,7 @@ module {:options "-functionSyntax:4"} WrappedESDKMain {
       if op?.Success? {
         var op := op?.value;
         match op
-        case Decrypt(_, _) =>
+        case Decrypt(_, _, _) =>
           var result := EsdkTestManifests.StartDecryptVectors(op);
           if result.Failure? {
             print result.error;
@@ -97,12 +98,17 @@ module {:options "-functionSyntax:4"} WrappedESDKMain {
   {
     var manifestPath? := OptValue(params, "manifest-path");
     var testName? := OptValue(params, "test-name");
+    var manifestFileName? := OptValue(params, "manifest-name");
 
     var manifestPath := if manifestPath?.Some? then manifestPath?.value else ".";
     :- Need(0 < |manifestPath|, "Invalid manifest path length\n");
 
+    :- Need(manifestFileName?.Some?, "Must supply manifest file name");
+    var manifestFileName := manifestFileName?.value;
+
     Success(EsdkManifestOptions.Decrypt(
               manifestPath := if Seq.Last(manifestPath) == '/' then manifestPath else manifestPath + "/",
+              manifestFileName := manifestFileName,
               testName := if testName?.Some? then testName?  else None
             ))
   }