From 5f79ef04f26e1ebf7e147b79bd3ec0ff0f637d8f Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 13 Nov 2024 12:09:37 -0800 Subject: [PATCH 1/7] test: add support for v1 and v2 manifests --- .../TestVectors/src/EsdkManifestOptions.dfy | 4 + .../TestVectors/src/EsdkTestManifests.dfy | 23 ++++ .../dafny/TestVectors/src/EsdkTestVectors.dfy | 42 +++++-- .../TestVectors/src/ParseEsdkJsonManifest.dfy | 104 +++++++++++++++++- 4 files changed, 163 insertions(+), 10 deletions(-) diff --git a/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy b/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy index fc8ab70f5..b392e7635 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy +++ b/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy @@ -11,6 +11,10 @@ module {:options "-functionSyntax:4"} EsdkManifestOptions { nameonly manifestPath: string, nameonly testName: Option := None ) + | V1Decrypt( + nameonly manifestPath: string, + nameonly keyPath: string + ) | Encrypt( nameonly manifestPath: string, nameonly manifest: string, diff --git a/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy b/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy index baa2667d6..f205faa3f 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy +++ b/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy @@ -29,6 +29,29 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { import opened EsdkTestVectors import WriteVectors + + method StartV1DecryptVectors( + op: EsdkManifestOptions.ManifestOptions + ) + returns (output: Result, string>) + requires op.V1Decrypt? + requires 0 < |op.manifestPath| && 0 < |op.keyPath| + requires Seq.Last(op.manifestPath) == '/' + requires Seq.Last(op.keyPath) == '/' + { + var decryptManifest :- expect GetManifest(op.manifestPath, "decrypt_message.json"); + :- Need(decryptManifest.DecryptManifest?, "Not a decrypt manifest"); + + var decryptVectors :- ParseEsdkJsonManifest.BuildV1DecryptTestVector( + op, + decryptManifest.version, + decryptManifest.keys, + decryptManifest.jsonTests + ); + + output := TestDecrypts(decryptManifest.keys, decryptVectors); + } + method StartDecryptVectors( op: EsdkManifestOptions.ManifestOptions ) diff --git a/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy b/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy index 808a064c3..a6291895a 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy +++ b/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 := None, + requiredEncryptionContextKeys: Option := None, + decryptDescriptions: KeyVectorsTypes.KeyDescription, + commitmentPolicy: mplTypes.ESDKCommitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT, + frameLength: Option, + algorithmSuiteId: Option, + description: string, + decryptionMethod: DecryptionMethod + ) datatype DecryptionMethod = | StreamingUnsignedOnly @@ -183,7 +198,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 +218,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 +237,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { } } - method DecryptVectorToDecryptTest( + method {:vcs_split_on_every_assert} DecryptVectorToDecryptTest( keys: KeyVectors.KeyVectorsClient, vector: EsdkDecryptTestVector ) @@ -233,14 +252,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( diff --git a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy index baeffb75e..efa1bf79e 100644 --- a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy +++ b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy @@ -37,6 +37,50 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { const encryptionContextJsonKey := "encryption-context" const reproducedEncryptionContextJsonKey := "reproduced-encryption-context" + function BuildV1DecryptTestVector( + op: EsdkManifestOptions.ManifestOptions, + version: SupportedDecryptVersion, + keys: KeyVectors.KeyVectorsClient, + obj: seq<(string, JSON)> + ) : Result, string> + requires op.V1Decrypt? + { + if |obj| == 0 then + Success([]) + else + var tail :- BuildV1DecryptTestVector(op, version, keys, obj[1..]); + var decryptVector :- ToDecryptTestVectors(op, version, keys, obj[0].0, obj[0].1); + Success([ decryptVector ] + tail) + } by method { + // This function ideally would be`{:tailrecursion}` + // but it is not simple to here is a method + // so that it does not explode with huge numbers of tests. + var i: nat := |obj|; + var vectors := []; + + while i != 0 + decreases i + invariant Success(vectors) == BuildV1DecryptTestVector(op, version, keys, obj[i..]) + { + i := i - 1; + var test := ToDecryptTestVectors(op, version, keys, obj[i].0, obj[i].1); + if test.Failure? { + ghost var j := i; + while j != 0 + decreases j + invariant Failure(test.error) == BuildV1DecryptTestVector(op, version, keys, obj[j..]) + { + j := j - 1; + } + return Failure(test.error); + } + + vectors := [test.value] + vectors; + } + + return Success(vectors); + } + function BuildDecryptTestVector( op: EsdkManifestOptions.ManifestOptions, version: SupportedDecryptVersion, @@ -82,20 +126,25 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { } - function ToDecryptTestVectors( + function {:vcs_split_on_every_assert} ToDecryptTestVectors( op: EsdkManifestOptions.ManifestOptions, version: SupportedDecryptVersion, keys: KeyVectors.KeyVectorsClient, name: string, json: JSON ) : Result - requires op.Decrypt? + requires op.Decrypt? || op.V1Decrypt? { :- Need(json.Object?, "Vector is not an object"); var obj := json.obj; match version - case 3 => V3ToDecryptTestVector(op, keys, name, obj, version) + case 3 => + :- Need(op.Decrypt?, "Err parsing manifest expected Decrypt"); + V3ToDecryptTestVector(op, keys, name, obj, version) + case 1 => + :- Need(op.V1Decrypt?, "Err parsing manifest expected V1Decrypt"); + V1ToDecryptTestVector(op, keys, name, obj, version) case _ => Failure("Version not supported") // case 1 => @@ -283,6 +332,40 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { } + function V1ToDecryptTestVector( + op: EsdkManifestOptions.ManifestOptions, + keys: KeyVectors.KeyVectorsClient, + name: string, + obj: seq<(string, JSON)>, + version: SupportedDecryptVersion + ) : Result + requires op.V1Decrypt? + { + var plaintextLoc :- GetString("plaintext", obj); + var ciphertextLoc :- GetString("ciphertext", obj); + :- Need( + && "file://" < ciphertextLoc + && "file://" < plaintextLoc, + "Invalid file prefix in test vector" + ); + var masterKeys :- GetArray("master-keys", obj); + var keyDescriptions :- GetKeyDescriptions(masterKeys, keys); + var keyDescription :- ToMultiKeyDescription(keyDescriptions); + + Success(PositiveV1DecryptTestVector( + id := name, + version := version, + manifestPath := op.manifestPath, + ciphertextPath := ciphertextLoc[|FILE_PREPEND|..], + plaintextPath := plaintextLoc[|FILE_PREPEND|..], + decryptDescriptions := keyDescription, + frameLength := None, + algorithmSuiteId := None, + description := name, + decryptionMethod := DecryptionMethod.OneShot + )) + } + function V3ToDecryptTestVector( op: EsdkManifestOptions.ManifestOptions, keys: KeyVectors.KeyVectorsClient, @@ -350,6 +433,21 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { Success([encryptDecryptKeyDescription.keyDescription] + tail) } + function ToMultiKeyDescription(keyDescriptions: seq) + : Result + { + if |keyDescriptions| == 1 then + Success(keyDescriptions[0]) + else + :- Need(|keyDescriptions| > 1, "Received invalid key description length"); + Success(KeyVectorsTypes.KeyDescription.Multi( + KeyVectorsTypes.MultiKeyring( + generator := Some(keyDescriptions[0]), + childKeyrings := keyDescriptions[1..] + ) + )) + } + function GetPath(key: string, obj: seq<(string, JSON)>) : Result { From c0a311b113932ed01a2e13f75fe2715a8b3eaa05 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 14 Nov 2024 12:16:12 -0800 Subject: [PATCH 2/7] test v1 vectors in net --- .../library_legacy_interop_test_vectors.yml | 133 ++++++++++++++++++ .github/workflows/pull.yml | 4 + TestVectors/Makefile | 10 +- .../TestVectors/src/EsdkManifestOptions.dfy | 5 +- .../TestVectors/src/EsdkTestManifests.dfy | 28 +--- .../dafny/TestVectors/src/EsdkTestVectors.dfy | 9 +- TestVectors/dafny/TestVectors/src/Index.dfy | 8 +- .../TestVectors/src/ParseEsdkJsonManifest.dfy | 90 ++++++------ .../dafny/TestVectors/test/RunMain.dfy | 16 ++- 9 files changed, 216 insertions(+), 87 deletions(-) create mode 100644 .github/workflows/library_legacy_interop_test_vectors.yml diff --git a/.github/workflows/library_legacy_interop_test_vectors.yml b/.github/workflows/library_legacy_interop_test_vectors.yml new file mode 100644 index 000000000..d26ad7324 --- /dev/null +++ b/.github/workflows/library_legacy_interop_test_vectors.yml @@ -0,0 +1,133 @@ +# 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, + ] + 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 + ] + # 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/setup-dafny-action@v1.6.1 + 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}}/ + run: | + if [${{matrix.legacy_zips}} == "aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5"]; then + MANIFEST_NAME=decrypt_message.json + else + MANIFEST_NAME=manifest.json + fi + + make test_decrypt_encrypt_vectors_net_v1 + \ No newline at end of file diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 93e6a04c5..da68f7fa4 100644 --- a/.github/workflows/pull.yml +++ b/.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' \ No newline at end of file diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 4ea5a76fe..c38e1c01d 100644 --- a/TestVectors/Makefile +++ b/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_v1: FRAMEWORK=net6.0 +test_decrypt_encrypt_vectors_net_v1: + 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" diff --git a/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy b/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy index b392e7635..85265a0eb 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy +++ b/TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy @@ -9,12 +9,9 @@ module {:options "-functionSyntax:4"} EsdkManifestOptions { datatype ManifestOptions = | Decrypt( nameonly manifestPath: string, + nameonly manifestFileName: string, nameonly testName: Option := None ) - | V1Decrypt( - nameonly manifestPath: string, - nameonly keyPath: string - ) | Encrypt( nameonly manifestPath: string, nameonly manifest: string, diff --git a/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy b/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy index f205faa3f..11f627e32 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy +++ b/TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy @@ -29,29 +29,6 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { import opened EsdkTestVectors import WriteVectors - - method StartV1DecryptVectors( - op: EsdkManifestOptions.ManifestOptions - ) - returns (output: Result, string>) - requires op.V1Decrypt? - requires 0 < |op.manifestPath| && 0 < |op.keyPath| - requires Seq.Last(op.manifestPath) == '/' - requires Seq.Last(op.keyPath) == '/' - { - var decryptManifest :- expect GetManifest(op.manifestPath, "decrypt_message.json"); - :- Need(decryptManifest.DecryptManifest?, "Not a decrypt manifest"); - - var decryptVectors :- ParseEsdkJsonManifest.BuildV1DecryptTestVector( - op, - decryptManifest.version, - decryptManifest.keys, - decryptManifest.jsonTests - ); - - output := TestDecrypts(decryptManifest.keys, decryptVectors); - } - method StartDecryptVectors( op: EsdkManifestOptions.ManifestOptions ) @@ -60,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( @@ -96,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; @@ -274,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); diff --git a/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy b/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy index a6291895a..bf72f9602 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy +++ b/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy @@ -179,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 diff --git a/TestVectors/dafny/TestVectors/src/Index.dfy b/TestVectors/dafny/TestVectors/src/Index.dfy index 520331216..5ca64c66f 100644 --- a/TestVectors/dafny/TestVectors/src/Index.dfy +++ b/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 )) } diff --git a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy index efa1bf79e..27aeefa84 100644 --- a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy +++ b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy @@ -37,50 +37,6 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { const encryptionContextJsonKey := "encryption-context" const reproducedEncryptionContextJsonKey := "reproduced-encryption-context" - function BuildV1DecryptTestVector( - op: EsdkManifestOptions.ManifestOptions, - version: SupportedDecryptVersion, - keys: KeyVectors.KeyVectorsClient, - obj: seq<(string, JSON)> - ) : Result, string> - requires op.V1Decrypt? - { - if |obj| == 0 then - Success([]) - else - var tail :- BuildV1DecryptTestVector(op, version, keys, obj[1..]); - var decryptVector :- ToDecryptTestVectors(op, version, keys, obj[0].0, obj[0].1); - Success([ decryptVector ] + tail) - } by method { - // This function ideally would be`{:tailrecursion}` - // but it is not simple to here is a method - // so that it does not explode with huge numbers of tests. - var i: nat := |obj|; - var vectors := []; - - while i != 0 - decreases i - invariant Success(vectors) == BuildV1DecryptTestVector(op, version, keys, obj[i..]) - { - i := i - 1; - var test := ToDecryptTestVectors(op, version, keys, obj[i].0, obj[i].1); - if test.Failure? { - ghost var j := i; - while j != 0 - decreases j - invariant Failure(test.error) == BuildV1DecryptTestVector(op, version, keys, obj[j..]) - { - j := j - 1; - } - return Failure(test.error); - } - - vectors := [test.value] + vectors; - } - - return Success(vectors); - } - function BuildDecryptTestVector( op: EsdkManifestOptions.ManifestOptions, version: SupportedDecryptVersion, @@ -133,7 +89,7 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { name: string, json: JSON ) : Result - requires op.Decrypt? || op.V1Decrypt? + requires op.Decrypt? { :- Need(json.Object?, "Vector is not an object"); var obj := json.obj; @@ -142,8 +98,12 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { case 3 => :- Need(op.Decrypt?, "Err parsing manifest expected Decrypt"); V3ToDecryptTestVector(op, keys, name, obj, version) + // Case 2 Needs negative test vectors.. + // case 2 => + // :- Need(op.V1Decrypt?, "Err parsing manifest expected V1Decrypt"); + // V2ToDecryptTestVector(op, keys, name, obj, version) case 1 => - :- Need(op.V1Decrypt?, "Err parsing manifest expected V1Decrypt"); + :- Need(op.Decrypt?, "Err parsing manifest expected Decrypt"); V1ToDecryptTestVector(op, keys, name, obj, version) case _ => Failure("Version not supported") @@ -339,7 +299,7 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { obj: seq<(string, JSON)>, version: SupportedDecryptVersion ) : Result - requires op.V1Decrypt? + requires op.Decrypt? { var plaintextLoc :- GetString("plaintext", obj); var ciphertextLoc :- GetString("ciphertext", obj); @@ -365,6 +325,42 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { decryptionMethod := DecryptionMethod.OneShot )) } + + // function V2ToDecryptTestVector( + // op: EsdkManifestOptions.ManifestOptions, + // keys: KeyVectors.KeyVectorsClient, + // name: string, + // obj: seq<(string, JSON)>, + // version: SupportedDecryptVersion + // ) : Result + // requires op.V1Decrypt? + // { + // var resultLoc :- GetObject("result", obj); + // var outputLoc :- GetObject("output", resultLoc); + // var plaintextLoc :- GetString("plaintext", outputLoc); + // var ciphertextLoc :- GetString("ciphertext", obj); + // :- Need( + // && "file://" < ciphertextLoc + // && "file://" < plaintextLoc, + // "Invalid file prefix in test vector" + // ); + // var masterKeys :- GetArray("master-keys", obj); + // var keyDescriptions :- GetKeyDescriptions(masterKeys, keys); + // var keyDescription :- ToMultiKeyDescription(keyDescriptions); + + // Success(PositiveV1DecryptTestVector( + // id := name, + // version := version, + // manifestPath := op.manifestPath, + // ciphertextPath := ciphertextLoc[|FILE_PREPEND|..], + // plaintextPath := plaintextLoc[|FILE_PREPEND|..], + // decryptDescriptions := keyDescription, + // frameLength := None, + // algorithmSuiteId := None, + // description := name, + // decryptionMethod := DecryptionMethod.OneShot + // )) + // } function V3ToDecryptTestVector( op: EsdkManifestOptions.ManifestOptions, diff --git a/TestVectors/dafny/TestVectors/test/RunMain.dfy b/TestVectors/dafny/TestVectors/test/RunMain.dfy index d39f7634a..d9cc11e27 100644 --- a/TestVectors/dafny/TestVectors/test/RunMain.dfy +++ b/TestVectors/dafny/TestVectors/test/RunMain.dfy @@ -20,10 +20,17 @@ module {:extern} TestWrappedESDKMain { method {:extern} GetTestVectorExecutionDirectory() returns (res: string) // method {:test} TestV1Vectors() { - // var _ :- expect EsdkTestManifests.StartV1DecryptVectors( - // "aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5/decrypt_message.json", - // "aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5/keys.json" + // var directory := GetTestVectorExecutionDirectory(); + // var result := EsdkTestManifests.StartDecryptVectors( + // EsdkManifestOptions.Decrypt( + // manifestPath := directory + "aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.8/", + // manifestFileName := "manifest.json" + // ) // ); + // if result.Failure? { + // print result.error; + // } + // expect result.Success?; // } @@ -82,7 +89,8 @@ module {:extern} TestWrappedESDKMain { var directory := GetTestVectorExecutionDirectory(); var result := EsdkTestManifests.StartDecryptVectors( EsdkManifestOptions.Decrypt( - manifestPath := directory + "dafny/TestVectors/test/" + manifestPath := directory + "dafny/TestVectors/test/", + manifestFileName := "decrypt-manifest.json" ) ); From 783c9b90304d082af2e8bdcf2f53b6abee0d0be2 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 14 Nov 2024 12:22:38 -0800 Subject: [PATCH 3/7] update --- .github/workflows/library_legacy_interop_test_vectors.yml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/library_legacy_interop_test_vectors.yml b/.github/workflows/library_legacy_interop_test_vectors.yml index d26ad7324..1d8e34ad4 100644 --- a/.github/workflows/library_legacy_interop_test_vectors.yml +++ b/.github/workflows/library_legacy_interop_test_vectors.yml @@ -122,11 +122,12 @@ jobs: working-directory: ./${{matrix.library}} env: MANIFEST_PATH: ${{matrix.legacy_zips}}/ + MANIFEST_NAME: run: | - if [${{matrix.legacy_zips}} == "aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5"]; then - MANIFEST_NAME=decrypt_message.json + if [${{matrix.legacy_zips}} == aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5]; then + export MANIFEST_NAME=decrypt_message.json else - MANIFEST_NAME=manifest.json + export MANIFEST_NAME=manifest.json fi make test_decrypt_encrypt_vectors_net_v1 From 48964a4177eab75ed4578decccbccdf28ca164fd Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 14 Nov 2024 12:29:00 -0800 Subject: [PATCH 4/7] update --- .github/workflows/library_legacy_interop_test_vectors.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/library_legacy_interop_test_vectors.yml b/.github/workflows/library_legacy_interop_test_vectors.yml index 1d8e34ad4..a76fccf02 100644 --- a/.github/workflows/library_legacy_interop_test_vectors.yml +++ b/.github/workflows/library_legacy_interop_test_vectors.yml @@ -122,9 +122,8 @@ jobs: working-directory: ./${{matrix.library}} env: MANIFEST_PATH: ${{matrix.legacy_zips}}/ - MANIFEST_NAME: run: | - if [${{matrix.legacy_zips}} == aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5]; then + if ["${{matrix.legacy_zips}}" == "aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5"]; then export MANIFEST_NAME=decrypt_message.json else export MANIFEST_NAME=manifest.json From d51d649cf1914d02ab24dfe10038bbd6ad1c2b65 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Thu, 14 Nov 2024 12:45:02 -0800 Subject: [PATCH 5/7] try --- .github/workflows/library_legacy_interop_test_vectors.yml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/.github/workflows/library_legacy_interop_test_vectors.yml b/.github/workflows/library_legacy_interop_test_vectors.yml index a76fccf02..3ef7929d6 100644 --- a/.github/workflows/library_legacy_interop_test_vectors.yml +++ b/.github/workflows/library_legacy_interop_test_vectors.yml @@ -122,12 +122,7 @@ jobs: 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: | - if ["${{matrix.legacy_zips}}" == "aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5"]; then - export MANIFEST_NAME=decrypt_message.json - else - export MANIFEST_NAME=manifest.json - fi - make test_decrypt_encrypt_vectors_net_v1 \ No newline at end of file From c33924f741562bd638eabdd5448219834e7b9fad Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Fri, 15 Nov 2024 10:42:42 -0800 Subject: [PATCH 6/7] add v2 --- .../library_legacy_interop_test_vectors.yml | 13 +- TestVectors/Makefile | 4 +- .../TestVectors/src/ParseEsdkJsonManifest.dfy | 192 +++++++----------- .../dafny/TestVectors/test/RunMain.dfy | 31 --- 4 files changed, 83 insertions(+), 157 deletions(-) diff --git a/.github/workflows/library_legacy_interop_test_vectors.yml b/.github/workflows/library_legacy_interop_test_vectors.yml index 3ef7929d6..75257db64 100644 --- a/.github/workflows/library_legacy_interop_test_vectors.yml +++ b/.github/workflows/library_legacy_interop_test_vectors.yml @@ -25,11 +25,18 @@ jobs: 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-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"] @@ -124,5 +131,5 @@ jobs: 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_v1 - \ No newline at end of file + make test_decrypt_encrypt_vectors_net_legacy + diff --git a/TestVectors/Makefile b/TestVectors/Makefile index c38e1c01d..09674351c 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -107,8 +107,8 @@ test_decrypt_encrypt_vectors_net: dotnet build runtimes/net dotnet run --project runtimes/net --framework $(FRAMEWORK) decrypt --manifest-path runtimes/net --manifest-name decrypt-manifest.json -test_decrypt_encrypt_vectors_net_v1: FRAMEWORK=net6.0 -test_decrypt_encrypt_vectors_net_v1: +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) diff --git a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy index 27aeefa84..8fc701a05 100644 --- a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy +++ b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy @@ -36,8 +36,10 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { const frameSizeJsonKey := "frame-size" const encryptionContextJsonKey := "encryption-context" const reproducedEncryptionContextJsonKey := "reproduced-encryption-context" + const buildTestVectorError := "Error other than negative test vector found thrown" + const negativeTestVectorFound := "Negative test vector found; not supported yet." - function BuildDecryptTestVector( + function {:vcs_split_on_every_assert} BuildDecryptTestVector( op: EsdkManifestOptions.ManifestOptions, version: SupportedDecryptVersion, keys: KeyVectors.KeyVectorsClient, @@ -49,8 +51,12 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { Success([]) else var tail :- BuildDecryptTestVector(op, version, keys, obj[1..]); - var encryptVector :- ToDecryptTestVectors(op, version, keys, obj[0].0, obj[0].1); - Success([ encryptVector ] + tail) + var encryptVector? := ToDecryptTestVectors(op, version, keys, obj[0].0, obj[0].1); + if encryptVector?.Success? then + Success([ encryptVector?.value ] + tail) + else + :- Need(encryptVector?.error == negativeTestVectorFound, buildTestVectorError); + Success(tail) } by method { // This function ideally would be`{:tailrecursion}` // but it is not simple to here is a method @@ -64,20 +70,27 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { { i := i - 1; var test := ToDecryptTestVectors(op, version, keys, obj[i].0, obj[i].1); - if test.Failure? { - ghost var j := i; + if test.Failure? && test.error != negativeTestVectorFound { + assert Failure(buildTestVectorError) == BuildDecryptTestVector(op, version, keys, obj[i..]); + ghost var j: nat := i; while j != 0 decreases j - invariant Failure(test.error) == BuildDecryptTestVector(op, version, keys, obj[j..]) + invariant Failure(buildTestVectorError) == BuildDecryptTestVector(op, version, keys, obj[j..]) { j := j - 1; + assert obj[j..][1..] == obj[j+1..]; } - return Failure(test.error); + assert Failure(buildTestVectorError) == BuildDecryptTestVector(op, version, keys, obj); + return Failure(buildTestVectorError); } - vectors := [test.value] + vectors; + if test.Success? { + vectors := [test.value] + vectors; + } + if test.Failure? && test.error == negativeTestVectorFound { + vectors := vectors; + } } - return Success(vectors); } @@ -98,57 +111,14 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { case 3 => :- Need(op.Decrypt?, "Err parsing manifest expected Decrypt"); V3ToDecryptTestVector(op, keys, name, obj, version) - // Case 2 Needs negative test vectors.. - // case 2 => - // :- Need(op.V1Decrypt?, "Err parsing manifest expected V1Decrypt"); - // V2ToDecryptTestVector(op, keys, name, obj, version) + case 2 => + // Case 2 Needs negative test vectors.. + :- Need(op.Decrypt?, "Err parsing manifest expected Decrypt"); + V2ToDecryptTestVector(op, keys, name, obj, version) case 1 => :- Need(op.Decrypt?, "Err parsing manifest expected Decrypt"); V1ToDecryptTestVector(op, keys, name, obj, version) - case _ => Failure("Version not supported") - - // case 1 => - // var plaintextPath :- GetPath(ciphertextJsonKey, obj); - // Success(PositiveDecryptTestVector( - // name := name, - // version := version, - // manifestPath := op.manifestPath, - // plaintextPath := plaintextPath, - // ciphertextPath := ciphertextPath, - // decryptDescriptions := decryptDescriptions, - // decryptionMethod := decryptionMethod - // )) - // case 2 => - // var result :- GetObject("result", obj); - // :- Need(|result| == 1 && Result?(result[0].0), "Unexpected result"); - // match result[0].0 - // case "output" => - // var output :- GetObject("output", result); - // var plaintextPath :- GetPath("plaintext", output); - - // Success(PositiveDecryptTestVector( - // name := name, - // version := version, - // manifestPath := op.manifestPath, - // plaintextPath := plaintextPath, - // ciphertextPath := ciphertextPath, - // decryptDescriptions := decryptDescriptions, - // decryptionMethod := decryptionMethod - // )) - // case "error" => - // var output :- GetObject("error", result); - // var errorDescription :- GetString("error-description", output); - - // Success(NegativeDecryptTestVector( - // name := name, - // version := version, - // manifestPath := op.manifestPath, - // errorDescription := errorDescription, - // ciphertextPath := ciphertextPath, - // decryptDescriptions := decryptDescriptions, - // decryptionMethod := decryptionMethod - // )) - + case _ => Failure("Version not supported\n") } function BuildEncryptTestVector( @@ -214,35 +184,6 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { case _ => Failure("Version not supported") } - // function V1ToEncryptTestVector( - // op: EsdkManifestOptions.ManifestOptions, - // keys: KeyVectors.KeyVectorsClient, - // name: string, - // obj: seq<(string, JSON)> - // ) : Result - // requires op.Encrypt? - // { - // var plaintextLoc :- GetString(plaintextJsonKey, obj); - // var algorithmSuite :- ParseJsonManifests.GetAlgorithmSuiteInfo(obj); - // :- Need(algorithmSuite.id.ESDK?, "Unsupported algorithmSuite"); - // var frameLength :- GetOptionalPositiveLong(frameSizeJsonKey, obj); - // var encryptionContext :- SmallObjectToStringStringMap(encryptionContextJsonKey, obj); - // var masterKeyArray :- GetArray(masterKeysJsonKey, obj); - // var keyDescriptions :- GetKeyDescriptions(masterKeyArray, keys); - - // Success(PositiveEncryptTestVector( - // name := name, - // version := 1, - // manifestPath := op.manifestPath, - // decryptManifestPath := op.decryptManifestOutput, - // plaintextPath := plaintextLoc, - // encryptDescriptions := keyDescriptions, - // decryptDescriptions := keyDescriptions, - // frameLength := frameLength, - // algorithmSuiteId := Some(algorithmSuite) - // )) - // } - function V5ToEncryptTestVector( op: EsdkManifestOptions.ManifestOptions, keys: KeyVectors.KeyVectorsClient, @@ -326,41 +267,50 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { )) } - // function V2ToDecryptTestVector( - // op: EsdkManifestOptions.ManifestOptions, - // keys: KeyVectors.KeyVectorsClient, - // name: string, - // obj: seq<(string, JSON)>, - // version: SupportedDecryptVersion - // ) : Result - // requires op.V1Decrypt? - // { - // var resultLoc :- GetObject("result", obj); - // var outputLoc :- GetObject("output", resultLoc); - // var plaintextLoc :- GetString("plaintext", outputLoc); - // var ciphertextLoc :- GetString("ciphertext", obj); - // :- Need( - // && "file://" < ciphertextLoc - // && "file://" < plaintextLoc, - // "Invalid file prefix in test vector" - // ); - // var masterKeys :- GetArray("master-keys", obj); - // var keyDescriptions :- GetKeyDescriptions(masterKeys, keys); - // var keyDescription :- ToMultiKeyDescription(keyDescriptions); - - // Success(PositiveV1DecryptTestVector( - // id := name, - // version := version, - // manifestPath := op.manifestPath, - // ciphertextPath := ciphertextLoc[|FILE_PREPEND|..], - // plaintextPath := plaintextLoc[|FILE_PREPEND|..], - // decryptDescriptions := keyDescription, - // frameLength := None, - // algorithmSuiteId := None, - // description := name, - // decryptionMethod := DecryptionMethod.OneShot - // )) - // } + function V2ToDecryptTestVector( + op: EsdkManifestOptions.ManifestOptions, + keys: KeyVectors.KeyVectorsClient, + name: string, + obj: seq<(string, JSON)>, + version: SupportedDecryptVersion + ) : Result + requires op.Decrypt? + { + var resultLoc :- GetObject("result", obj); + var errorLoc? := GetObject("error", resultLoc); + // TODO build negative test vectors appropriately instead of not + // accepting any. + // Return early if we have a negative test vector + if errorLoc?.Success? then + Failure(negativeTestVectorFound) + else + + var outputLoc :- GetObject("output", resultLoc); + + var plaintextLoc :- GetString("plaintext", outputLoc); + var ciphertextLoc :- GetString("ciphertext", obj); + :- Need( + && "file://" < ciphertextLoc + && "file://" < plaintextLoc, + "Invalid file prefix in test vector" + ); + var masterKeys :- GetArray("master-keys", obj); + var keyDescriptions :- GetKeyDescriptions(masterKeys, keys); + var keyDescription :- ToMultiKeyDescription(keyDescriptions); + + Success(PositiveV1DecryptTestVector( + id := name, + version := version, + manifestPath := op.manifestPath, + ciphertextPath := ciphertextLoc[|FILE_PREPEND|..], + plaintextPath := plaintextLoc[|FILE_PREPEND|..], + decryptDescriptions := keyDescription, + frameLength := None, + algorithmSuiteId := None, + description := name, + decryptionMethod := DecryptionMethod.OneShot + )) + } function V3ToDecryptTestVector( op: EsdkManifestOptions.ManifestOptions, diff --git a/TestVectors/dafny/TestVectors/test/RunMain.dfy b/TestVectors/dafny/TestVectors/test/RunMain.dfy index d9cc11e27..2e10ad8a1 100644 --- a/TestVectors/dafny/TestVectors/test/RunMain.dfy +++ b/TestVectors/dafny/TestVectors/test/RunMain.dfy @@ -19,37 +19,6 @@ module {:extern} TestWrappedESDKMain { // Runtime should define an extern to return the expected test execution directory. method {:extern} GetTestVectorExecutionDirectory() returns (res: string) - // method {:test} TestV1Vectors() { - // var directory := GetTestVectorExecutionDirectory(); - // var result := EsdkTestManifests.StartDecryptVectors( - // EsdkManifestOptions.Decrypt( - // manifestPath := directory + "aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.8/", - // manifestFileName := "manifest.json" - // ) - // ); - // if result.Failure? { - // print result.error; - // } - // expect result.Success?; - // } - - - // method {:test} TestV2Vectors() { - // var _ :- expect EsdkTestManifests.StartDecryptVectors( - // EsdkManifestOptions.Decrypt( - // manifestPath := "aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-2.3.0/" - // ) - // ); - // } - - // method {:test} TestV2Vectors() { - // TestEsdkManifests.StartV1Vectors( - // "dafny/ESDK/test/python-2.3.0/manifest.json", - // "dafny/ESDK/test/python-2.3.0/keys.json" - // ); - - // } - method {:test} RunManifestTests() { TestGenerateEncryptManifest(); TestEncryptManifest(); From 05d4236f051d48e5d623d43d895d0c4b2c486eff Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Fri, 15 Nov 2024 11:29:41 -0800 Subject: [PATCH 7/7] rename --- TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy | 8 ++++---- .../dafny/TestVectors/src/ParseEsdkJsonManifest.dfy | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy b/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy index bf72f9602..15dedc325 100644 --- a/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy +++ b/TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy @@ -151,7 +151,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { description: string, decryptionMethod: DecryptionMethod ) - | PositiveV1DecryptTestVector( + | PositiveV1OrV2DecryptTestVector( id: string, version: SupportedDecryptVersion, manifestPath: string, @@ -201,7 +201,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { var ciphertext :- expect ReadVectorsFile(test.vector.manifestPath + test.vector.ciphertextPath); var plaintext; - if test.vector.PositiveDecryptTestVector? || test.vector.PositiveV1DecryptTestVector? { + if test.vector.PositiveDecryptTestVector? || test.vector.PositiveV1OrV2DecryptTestVector? { plaintext :- expect ReadVectorsFile(test.vector.manifestPath + test.vector.plaintextPath); } @@ -222,12 +222,12 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { case NegativeDecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_) => && result.Failure? - case PositiveV1DecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_) + case PositiveV1OrV2DecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_) => && result.Success? && result.value.plaintext == plaintext; if !output { - if (test.vector.PositiveDecryptTestVector? || test.vector.PositiveV1DecryptTestVector?) && result.Failure? { + if (test.vector.PositiveDecryptTestVector? || test.vector.PositiveV1OrV2DecryptTestVector?) && result.Failure? { print result.error, "\n"; if && result.error.AwsCryptographyMaterialProviders? diff --git a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy index 8fc701a05..24605007b 100644 --- a/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy +++ b/TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy @@ -253,7 +253,7 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { var keyDescriptions :- GetKeyDescriptions(masterKeys, keys); var keyDescription :- ToMultiKeyDescription(keyDescriptions); - Success(PositiveV1DecryptTestVector( + Success(PositiveV1OrV2DecryptTestVector( id := name, version := version, manifestPath := op.manifestPath, @@ -298,7 +298,7 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { var keyDescriptions :- GetKeyDescriptions(masterKeys, keys); var keyDescription :- ToMultiKeyDescription(keyDescriptions); - Success(PositiveV1DecryptTestVector( + Success(PositiveV1OrV2DecryptTestVector( id := name, version := version, manifestPath := op.manifestPath,