feat(Decrypt)!: Encryption Context is optional input to DecryptInput (#…

…223) Co-authored-by: lavaleri <49660121+lavaleri@users.noreply.github.com> Co-authored-by: seebees <ryanemer@amazon.com>
aws · Oct 11, 2023 · c26f2dd · c26f2dd
1 parent 16a0615
commit c26f2dd
Show file tree

Hide file tree

Showing 27 changed files with 1,985 additions and 127 deletions.
diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml
@@ -34,15 +34,24 @@ jobs:
         ]
         os: [ macos-latest ]
     runs-on: ${{ matrix.os }}
+    environment: "MPL_DAFNY"
     env:
       DOTNET_CLI_TELEMETRY_OPTOUT: 1
       DOTNET_NOLOGO: 1
     steps:
       - uses: actions/checkout@v2
-      # The specification submodule is private so we don't have access, but we don't need
-      # it to verify the Dafny code. Instead we manually pull the submodules we DO need.
-      - run: git submodule update --init libraries
-      - run: git submodule update --init --recursive mpl
+      - name: Init Submodules
+        env:
+          # This secret is in the configured environment
+          # Token created on # 09/26/2023
+          # expires in ~30 days 10/26/2023
+          MPL_PAT: ${{ secrets.MPL_DAFNY }}
+        run: |
+            AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')"
+            git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
+            git config --global --add url.https://github.com/.insteadOf git@github.com:
+            git submodule update --init libraries
+            git submodule update --init --recursive mpl
 
       - name: Support longpaths
         run: |

diff --git a/.github/workflows/library_java_tests.yml b/.github/workflows/library_java_tests.yml
@@ -30,15 +30,28 @@ jobs:
           macos-latest
         ]
     runs-on: ${{ matrix.os }}
+    environment: "MPL_DAFNY"
     permissions:
       id-token: write
       contents: read
     steps:
       - uses: actions/checkout@v2
-      # The specification submodule is private so we don't have access, but we don't need
-      # it to verify the Dafny code. Instead we manually pull the submodules we DO need.
-      - run: git submodule update --init libraries
-      - run: git submodule update --init --recursive mpl
+      - name: Init Submodules
+        env:
+          # This secret is in the configured environment
+          # Token created on # 09/26/2023
+          # expires in ~30 days 10/26/2023
+          MPL_PAT: ${{ secrets.MPL_DAFNY }}
+        run: |
+            AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')"
+            git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
+            git config --global --add url.https://github.com/.insteadOf git@github.com:
+            git submodule update --init libraries
+            git submodule update --init --recursive mpl
+
+      - name: Support longpaths
+        run: |
+          git config --global core.longpaths true
       - name: Configure AWS Credentials
         uses: aws-actions/configure-aws-credentials@v1
         with:

diff --git a/.github/workflows/library_net_tests.yml b/.github/workflows/library_net_tests.yml
@@ -30,6 +30,7 @@ jobs:
           macos-latest,
         ]
     runs-on: ${{ matrix.os }}
+    environment: "MPL_DAFNY"
     permissions:
       id-token: write
       contents: read
@@ -41,8 +42,19 @@ jobs:
         run: |
           git config --global core.longpaths true
       - uses: actions/checkout@v2
-      - run: git submodule update --init libraries
-      - run: git submodule update --init --recursive mpl
+      - name: Init Submodules
+        shell: bash
+        env:
+          # This secret is in the configured environment
+          # Token created on # 09/26/2023
+          # expires in ~30 days 10/26/2023
+          MPL_PAT: ${{ secrets.MPL_DAFNY }}
+        run: |
+          AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')"
+          git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
+          git config --global --add url.https://github.com/.insteadOf git@github.com:
+          git submodule update --init libraries
+          git submodule update --init --recursive mpl
 
       - name: Configure AWS Credentials
         uses: aws-actions/configure-aws-credentials@v1

diff --git a/.gitmodules b/.gitmodules
@@ -7,7 +7,7 @@
 	url = https://github.com/awslabs/aws-encryption-sdk-specification.git
 [submodule "mpl"]
 	path = mpl
-	url = https://github.com/aws/aws-cryptographic-material-providers-library-java.git
+	url = https://github.com/aws/aws-cryptographic-material-providers-library-dafny.git
 [submodule "AwsEncryptionSDK/runtimes/net/TestVectorsV3/TestVectors/resources/aws-encryption-sdk-test-vectors"]
 	path = AwsEncryptionSDK/runtimes/net/TestVectorsV3/TestVectors/resources/aws-encryption-sdk-test-vectors
 	url = https://github.com/awslabs/aws-encryption-sdk-test-vectors.git
diff --git a/AwsEncryptionSDK/Makefile b/AwsEncryptionSDK/Makefile
@@ -10,7 +10,7 @@ PROJECT_SERVICES := \
 	AwsEncryptionSdk \
 
 SERVICE_NAMESPACE_AwsEncryptionSdk=aws.cryptography.encryptionSdk
-MAX_RESOURCE_COUNT=100000000
+MAX_RESOURCE_COUNT=90000000
 # Order is important
 # In java they MUST be built
 # in the order they depend on each other

diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy
@@ -113,7 +113,8 @@ include "../../../../mpl/StandardLibrary/src/Index.dfy"
  datatype DecryptInput = | DecryptInput (
  nameonly ciphertext: seq<uint8> ,
  nameonly materialsManager: Option<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager> ,
- nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring>
+ nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring> ,
+ nameonly encryptionContext: Option<AwsCryptographyMaterialProvidersTypes.EncryptionContext>
  )
  datatype DecryptOutput = | DecryptOutput (
  nameonly plaintext: seq<uint8> ,

diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy
@@ -1,5 +1,8 @@
 namespace aws.cryptography.encryptionSdk
 
+use aws.cryptography.primitives#AwsCryptographicPrimitives
+use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders
+
 /////////////
 // ESDK Client Creation
 
@@ -9,6 +12,10 @@ namespace aws.cryptography.encryptionSdk
 @aws.polymorph#localService(
   sdkId: "ESDK",
   config: AwsEncryptionSdkConfig,
+  dependencies: [
+    AwsCryptographicPrimitives,
+    AwsCryptographicMaterialProviders
+  ]
 )
 service AwsEncryptionSdk {
   version: "2020-10-24",
@@ -77,6 +84,12 @@ structure DecryptInput {
   // One of keyring or CMM are required
   materialsManager: aws.cryptography.materialProviders#CryptographicMaterialsManagerReference,
   keyring: aws.cryptography.materialProviders#KeyringReference,
+  //= aws-encryption-sdk-specification/client-apis/keyring-interface.md#onencrypt
+  //= type=implication
+  //# The following inputs to this behavior MUST be OPTIONAL:
+  // (blank line for duvet)
+  //# - [Encryption Context](#encryption-context)
+  encryptionContext: aws.cryptography.materialProviders#EncryptionContext,
 }
 
 structure DecryptOutput {