From cb84e9a68f02599803886c23a30db5326a5edb12 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 21 Aug 2024 20:33:09 -0700 Subject: [PATCH] chore(GHA): add dafny interoperability action --- .github/workflows/dafny_interop.yml | 35 ++ .github/workflows/dafny_interop_test_net.yml | 253 ++++++++++++++ .../dafny_interop_test_vector_net.yml | 308 ++++++++++++++++++ 3 files changed, 596 insertions(+) create mode 100644 .github/workflows/dafny_interop.yml create mode 100644 .github/workflows/dafny_interop_test_net.yml create mode 100644 .github/workflows/dafny_interop_test_vector_net.yml diff --git a/.github/workflows/dafny_interop.yml b/.github/workflows/dafny_interop.yml new file mode 100644 index 000000000..3fa0800c9 --- /dev/null +++ b/.github/workflows/dafny_interop.yml @@ -0,0 +1,35 @@ +# This workflow is for testing backwards compatibility of a dafny version +# and tests if a project that consumes the mpl will be backwards compatible with +# a newer version of Dafny +name: Dafny Interoperability Test + +on: + workflow_dispatch: + inputs: + mpl-dafny: + description: "The Dafny version to compile the MPL with (4.2.0, nightly-latest, etc..)" + required: true + type: string + mpl-commit: + description: "The MPL branch/commit to use" + required: false + default: "main" + type: string + esdk-dafny: + description: "The Dafny version to compile the DBESDK with (4.2.0, nightly-latest, etc..)" + required: true + type: string + +jobs: + dafny-interop-net: + uses: ./.github/workflows/dafny_interop_test_net.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + esdk-dafny: ${{inputs.esdk-dafny}} + dafny-interop-net-test-vectors: + uses: ./.github/workflows/dafny_interop_test_vector_net.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + esdk-dafny: ${{inputs.esdk-dafny}} diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml new file mode 100644 index 000000000..7c4b447a2 --- /dev/null +++ b/.github/workflows/dafny_interop_test_net.yml @@ -0,0 +1,253 @@ +# This workflow performs tests in DotNet with MPL nightly latest. +name: Library DotNet Backwards Interop Tests + +on: + workflow_call: + inputs: + mpl-dafny: + description: "The Dafny version to compile the MPL with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + mpl-commit: + description: "The MPL commit to use" + required: false + default: "main" + type: string + esdk-dafny: + description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + +jobs: + testDotNet: + strategy: + fail-fast: false + matrix: + os: [ + windows-latest, + ubuntu-latest, + macos-12, + ] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + env: + DOTNET_CLI_TELEMETRY_OPTOUT: 1 + DOTNET_NOLOGO: 1 + steps: + - name: Support longpaths on Git checkout + run: | + git config --global core.longpaths true + - uses: actions/checkout@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup .NET Core SDK 6 + uses: actions/setup-dotnet@v3 + with: + dotnet-version: '6.0.x' + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Download Dependencies + working-directory: AwsEncryptionSDK + run: make setup_net + + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v4 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 + role-session-name: DDBEC-Dafny-Net-Tests + + - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} + shell: bash + working-directory: mpl + run: | + make setup_net + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_net CORES=$CORES + + - name: Setup ESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.esdk-dafny}} + + - name: Build ESDK implementation + shell: bash + working-directory: AwsEncryptionSDK + run: | + # This works because `node` is installed by default on GHA runners + make transpile_implementation_net + make transpile_test_net + + - name: Test .NET Framework net48 + working-directory: ./AwsEncryptionSDK + if: matrix.os == 'windows-latest' + shell: bash + run: | + make test_net FRAMEWORK=net48 + + - name: Test .NET net6.0 + working-directory: ./AwsEncryptionSDK + shell: bash + run: | + if [ "$RUNNER_OS" == "macOS" ]; then + make test_net_mac_intel FRAMEWORK=net6.0 + else + make test_net FRAMEWORK=net6.0 + fi + + - name: Test Examples on .NET Framework net48 + working-directory: ./AwsEncryptionSDK + if: matrix.os == 'windows-latest' + shell: bash + run: | + dotnet test \ + runtimes/net/Examples \ + --framework net48 + + - name: Test Examples on .NET net6.0 + working-directory: ./AwsEncryptionSDK + shell: bash + run: | + if [ "$RUNNER_OS" == "macOS" ]; then + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" + dotnet test \ + runtimes/net/Examples \ + --framework net6.0 + else + dotnet test \ + runtimes/net/Examples \ + --framework net6.0 + fi + + - name: Unzip ESDK-NET @ v4.0.0 Valid Vectors + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources + shell: bash + run: | + NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors + mkdir -p $NET_400_VALID_VECTORS + DOWNLOAD_NAME=valid-Net-4.0.0.zip + unzip -o -qq $DOWNLOAD_NAME -d $NET_400_VALID_VECTORS + + - name: Run ESDK-NET @ v4.0.0 Valid Vectors expect success + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + continue-on-error: true + shell: bash + run: | + NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \ + dotnet test --framework net48 + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + + - name: Unzip ESDK-NET @ v4.0.0 Invalid Vectors + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources + shell: bash + run: | + NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors + mkdir -p $NET_400_INVALID_VECTORS + DOWNLOAD_NAME=invalid-Net-4.0.0.zip + unzip -o -qq $DOWNLOAD_NAME -d $NET_400_INVALID_VECTORS + + - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 48 expect failure + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + continue-on-error: true + shell: bash + run: | + NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + dotnet test --framework net48 + # Dotnet test returns 1 for failure. + TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi; + # We want this to fail, so if it returned 1, step passes, else it fails + # TODO Post-#619: Refactor Test Vectors to expect failure, + # as I doubt this true false logic works + + - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 6.0 expect failure + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + continue-on-error: true + shell: bash + run: | + NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors + if [ "$RUNNER_OS" == "macOS" ]; then + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" \ + dotnet test --framework net6.0 + else + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + dotnet test --framework net6.0 + fi + # Dotnet test returns 1 for failure. + TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi; + # We want this to fail, so if it returned 1, step passes, else it fails + # TODO Post-#619: Refactor Test Vectors to expect failure, + # as I doubt this true false logic works + + - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET expect Success + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + shell: bash + run: | + NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + dotnet test --framework net48 --logger "console;verbosity=quiet" + if [ "$RUNNER_OS" == "macOS" ]; then + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + else + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + fi + + - name: Unzip ESDK-NET @ v4.0.1 Vectors + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources + shell: bash + run: | + NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors + mkdir -p $NET_401_VECTORS + DOWNLOAD_NAME=v4-Net-4.0.1.zip + unzip -o -qq $DOWNLOAD_NAME -d $NET_401_VECTORS + + - name: Run ESDK-NET @ v4.0.1 Vectors expect success + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + shell: bash + run: | + NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors + # We expect net48 to run only for Windows + if [ "$RUNNER_OS" == "Windows" ]; then + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \ + dotnet test --framework net48 + fi + if [ "$RUNNER_OS" == "macOS" ]; then + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" \ + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + else + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + fi diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml new file mode 100644 index 000000000..7343e363d --- /dev/null +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -0,0 +1,308 @@ +# This workflow performs tests in DotNet with MPL nightly latest. +name: Library DotNet Backwards Interop Test Vectors + +on: + workflow_call: + inputs: + mpl-dafny: + description: "The Dafny version to compile the MPL with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + mpl-commit: + description: "The MPL commit to use" + required: false + default: "main" + type: string + esdk-dafny: + description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + +env: + # Used in examples + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_KEY_ID: arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_KEY_ID_2: arn:aws:kms:eu-central-1:658956600833:key/75414c93-5285-4b57-99c9-30c1cf0a22c2 + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_MRK_KEY_ID: arn:aws:kms:us-east-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7 + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_MRK_KEY_ID_2: arn:aws:kms:eu-west-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7 + AWS_ENCRYPTION_SDK_EXAMPLE_LIMITED_ROLE_ARN_US_EAST_1: arn:aws:iam::370957321024:role/GitHub-CI-ESDK-Dafny-Role-us-west-2 + AWS_ENCRYPTION_SDK_EXAMPLE_LIMITED_ROLE_ARN_EU_WEST_1: arn:aws:iam::370957321024:role/GitHub-CI-ESDK-Dafny-Role-us-west-2 + # Used for Test Vectors + VECTORS_URL: https://github.com/awslabs/aws-encryption-sdk-test-vectors/raw/master/vectors/awses-decrypt/python-2.3.0.zip + +jobs: + decrypt_python_vectors: + strategy: + matrix: + os: [ + windows-latest, + ubuntu-latest, + macos-12, + ] + runs-on: ${{matrix.os}} + permissions: + id-token: write + contents: read + env: + DOTNET_CLI_TELEMETRY_OPTOUT: 1 + DOTNET_NOLOGO: 1 + steps: + - name: Support longpaths on Git checkout + run: | + git config --global core.longpaths true + - uses: actions/checkout@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup .NET Core SDK 6 + uses: actions/setup-dotnet@v3 + with: + dotnet-version: '6.0.x' + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Download Dependencies + working-directory: AwsEncryptionSDK + run: make setup_net + + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v4 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 + role-session-name: DDBEC-Dafny-Net-Tests + + - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} + shell: bash + working-directory: mpl + run: | + make setup_net + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_net CORES=$CORES + + - name: Setup ESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.esdk-dafny}} + + - name: Build ESDK implementation + shell: bash + working-directory: AwsEncryptionSDK + run: | + # This works because `node` is installed by default on GHA runners + make transpile_implementation_net + make transpile_test_net + + - name: Fetch Python 2.3.0 Test Vectors + working-directory: ./ + shell: bash + run: | + PYTHON_23_VECTOR_PATH=$GITHUB_WORKSPACE/python23/vectors + mkdir -p $PYTHON_23_VECTOR_PATH + DOWNLOAD_NAME=python23.zip + curl --no-progress-meter --output $DOWNLOAD_NAME --location $VECTORS_URL + unzip -o -qq $DOWNLOAD_NAME -d $PYTHON_23_VECTOR_PATH + rm $DOWNLOAD_NAME + + - name: Decrypt Python 2.3.0 Test Vectors on .net48 (Windows ONLY) + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + if: matrix.os == 'windows-latest' + shell: bash + run: | + PYTHON_23_VECTOR_PATH=$GITHUB_WORKSPACE/python23/vectors + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$PYTHON_23_VECTOR_PATH/manifest.json" \ + dotnet test --framework net48 + + - name: Decrypt Python 2.3.0 Test Vectors on .net6.0 + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + if: matrix.os != 'windows-latest' + shell: bash + run: | + PYTHON_23_VECTOR_PATH=$GITHUB_WORKSPACE/python23/vectors + if [ "$RUNNER_OS" == "macOS" ]; then + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$PYTHON_23_VECTOR_PATH/manifest.json" \ + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" \ + dotnet test --framework net6.0 + else + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$PYTHON_23_VECTOR_PATH/manifest.json" \ + dotnet test --framework net6.0 + fi + + generate_vectors: + strategy: + matrix: + os: [ + ubuntu-latest, + macos-12, + ] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + env: + DOTNET_CLI_TELEMETRY_OPTOUT: 1 + DOTNET_NOLOGO: 1 + steps: + - name: Support longpaths on Git checkout + run: | + git config --global core.longpaths true + - uses: actions/checkout@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup .NET Core SDK 6 + uses: actions/setup-dotnet@v3 + with: + dotnet-version: '6.0.x' + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Download Dependencies + working-directory: AwsEncryptionSDK + run: make setup_net + + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v4 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 + role-session-name: DDBEC-Dafny-Net-Tests + + - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} + shell: bash + working-directory: mpl + run: | + make setup_net + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_net CORES=$CORES + + - name: Setup ESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.esdk-dafny}} + + - name: Build ESDK implementation + shell: bash + working-directory: AwsEncryptionSDK + run: | + # This works because `node` is installed by default on GHA runners + make transpile_implementation_net + make transpile_test_net + + - name: Generate Test Vectors with .NET Framework net6.0 + # TODO Post-#619: Fix Zip file creation on Windows + if: matrix.os != 'windows-latest' + working-directory: ./AwsEncryptionSDK + shell: bash + run: | + NET_41_VECTOR_PATH=net41/vectors + mkdir -p $NET_41_VECTOR_PATH + GEN_PATH=runtimes/net/TestVectorsNative/TestVectorGenerator + dotnet run --project $GEN_PATH --framework net6.0 -- \ + --encrypt-manifest $GEN_PATH/resources/0006-awses-message-decryption-generation.v2.json \ + --output-dir $NET_41_VECTOR_PATH + + - name: Zip the Generated Test Vectors for ESDK-JS on Mac/Linux + if: matrix.os != 'windows-latest' + working-directory: ./AwsEncryptionSDK + shell: bash + run: | + NET_41_VECTOR_PATH=net41/vectors + cd $NET_41_VECTOR_PATH + zip -qq net41.zip -r . + + - name: Upload Zip File + uses: actions/upload-artifact@v4 + if: matrix.os != 'windows-latest' + with: + name: ${{matrix.os}}_vector_artifact + path: AwsEncryptionSDK/net41/vectors/*.zip + + decrypt_net_vectors_with_js: + needs: generate_vectors + strategy: + matrix: + os: [ + ubuntu-latest, + macos-12, + ] + 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@v2 + - name: Init Submodules + shell: bash + run: | + git submodule update --init libraries + git submodule update --init --recursive mpl + git submodule update --init smithy-dafny + + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v4 + 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: NetTests + + - name: Set up Dirs + working-directory: ./AwsEncryptionSDK + run: | + NET_41_VECTOR_PATH=AwsEncryptionSDK/net41/vectors + mkdir -p $NET_41_VECTOR_PATH + + - name: Download Encrypt Manifest Artifact + uses: actions/download-artifact@v4 + with: + name: ${{matrix.os}}_vector_artifact + path: AwsEncryptionSDK/net41/vectors + + - uses: actions/setup-node@v4 + with: + node-version: 17 + + - name: Install deps + run: | + openssl version + npm install @aws-crypto/integration-node + npm install fast-xml-parser + + - name: Decrypt Generated Test Vectors with ESDK-JS + working-directory: ./AwsEncryptionSDK + # TODO Post-#619: Fix Zip file creation on Windows + shell: bash + run: | + NET_41_VECTOR_PATH=net41/vectors + cd $NET_41_VECTOR_PATH + npx -y @aws-crypto/integration-node decrypt -v net41.zip -c cpu -f 100 \ No newline at end of file