Skip to content

Commit 3f09bcb

Browse files
josecorellalavaleriseebees
committed
feat(Decrypt)!: Encryption Context is optional input to DecryptInput (#223)
Co-authored-by: lavaleri <[email protected]> Co-authored-by: seebees <[email protected]>
1 parent 4255799 commit 3f09bcb

27 files changed

+1985
-127
lines changed

.github/workflows/library_dafny_verification.yml

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -34,15 +34,24 @@ jobs:
3434
]
3535
os: [ macos-latest ]
3636
runs-on: ${{ matrix.os }}
37+
environment: "MPL_DAFNY"
3738
env:
3839
DOTNET_CLI_TELEMETRY_OPTOUT: 1
3940
DOTNET_NOLOGO: 1
4041
steps:
4142
- uses: actions/checkout@v2
42-
# The specification submodule is private so we don't have access, but we don't need
43-
# it to verify the Dafny code. Instead we manually pull the submodules we DO need.
44-
- run: git submodule update --init libraries
45-
- run: git submodule update --init --recursive mpl
43+
- name: Init Submodules
44+
env:
45+
# This secret is in the configured environment
46+
# Token created on # 09/26/2023
47+
# expires in ~30 days 10/26/2023
48+
MPL_PAT: ${{ secrets.MPL_DAFNY }}
49+
run: |
50+
AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')"
51+
git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
52+
git config --global --add url.https://github.com/.insteadOf [email protected]:
53+
git submodule update --init libraries
54+
git submodule update --init --recursive mpl
4655
4756
- name: Support longpaths
4857
run: |

.github/workflows/library_java_tests.yml

Lines changed: 17 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -30,15 +30,28 @@ jobs:
3030
macos-latest
3131
]
3232
runs-on: ${{ matrix.os }}
33+
environment: "MPL_DAFNY"
3334
permissions:
3435
id-token: write
3536
contents: read
3637
steps:
3738
- uses: actions/checkout@v2
38-
# The specification submodule is private so we don't have access, but we don't need
39-
# it to verify the Dafny code. Instead we manually pull the submodules we DO need.
40-
- run: git submodule update --init libraries
41-
- run: git submodule update --init --recursive mpl
39+
- name: Init Submodules
40+
env:
41+
# This secret is in the configured environment
42+
# Token created on # 09/26/2023
43+
# expires in ~30 days 10/26/2023
44+
MPL_PAT: ${{ secrets.MPL_DAFNY }}
45+
run: |
46+
AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')"
47+
git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
48+
git config --global --add url.https://github.com/.insteadOf [email protected]:
49+
git submodule update --init libraries
50+
git submodule update --init --recursive mpl
51+
52+
- name: Support longpaths
53+
run: |
54+
git config --global core.longpaths true
4255
- name: Configure AWS Credentials
4356
uses: aws-actions/configure-aws-credentials@v1
4457
with:

.github/workflows/library_net_tests.yml

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@ jobs:
3030
macos-latest,
3131
]
3232
runs-on: ${{ matrix.os }}
33+
environment: "MPL_DAFNY"
3334
permissions:
3435
id-token: write
3536
contents: read
@@ -41,8 +42,19 @@ jobs:
4142
run: |
4243
git config --global core.longpaths true
4344
- uses: actions/checkout@v2
44-
- run: git submodule update --init libraries
45-
- run: git submodule update --init --recursive mpl
45+
- name: Init Submodules
46+
shell: bash
47+
env:
48+
# This secret is in the configured environment
49+
# Token created on # 09/26/2023
50+
# expires in ~30 days 10/26/2023
51+
MPL_PAT: ${{ secrets.MPL_DAFNY }}
52+
run: |
53+
AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')"
54+
git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
55+
git config --global --add url.https://github.com/.insteadOf [email protected]:
56+
git submodule update --init libraries
57+
git submodule update --init --recursive mpl
4658
4759
- name: Configure AWS Credentials
4860
uses: aws-actions/configure-aws-credentials@v1

.gitmodules

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
url = https://github.com/awslabs/aws-encryption-sdk-specification.git
88
[submodule "mpl"]
99
path = mpl
10-
url = https://github.com/aws/aws-cryptographic-material-providers-library-java.git
10+
url = https://github.com/aws/aws-cryptographic-material-providers-library-dafny.git
1111
[submodule "AwsEncryptionSDK/runtimes/net/TestVectorsV3/TestVectors/resources/aws-encryption-sdk-test-vectors"]
1212
path = AwsEncryptionSDK/runtimes/net/TestVectorsV3/TestVectors/resources/aws-encryption-sdk-test-vectors
1313
url = https://github.com/awslabs/aws-encryption-sdk-test-vectors.git

AwsEncryptionSDK/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ PROJECT_SERVICES := \
1010
AwsEncryptionSdk \
1111

1212
SERVICE_NAMESPACE_AwsEncryptionSdk=aws.cryptography.encryptionSdk
13-
MAX_RESOURCE_COUNT=100000000
13+
MAX_RESOURCE_COUNT=90000000
1414
# Order is important
1515
# In java they MUST be built
1616
# in the order they depend on each other

AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,8 @@ include "../../../../mpl/StandardLibrary/src/Index.dfy"
113113
datatype DecryptInput = | DecryptInput (
114114
nameonly ciphertext: seq<uint8> ,
115115
nameonly materialsManager: Option<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager> ,
116-
nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring>
116+
nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring> ,
117+
nameonly encryptionContext: Option<AwsCryptographyMaterialProvidersTypes.EncryptionContext>
117118
)
118119
datatype DecryptOutput = | DecryptOutput (
119120
nameonly plaintext: seq<uint8> ,

AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
namespace aws.cryptography.encryptionSdk
22

3+
use aws.cryptography.primitives#AwsCryptographicPrimitives
4+
use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders
5+
36
/////////////
47
// ESDK Client Creation
58

@@ -9,6 +12,10 @@ namespace aws.cryptography.encryptionSdk
912
@aws.polymorph#localService(
1013
sdkId: "ESDK",
1114
config: AwsEncryptionSdkConfig,
15+
dependencies: [
16+
AwsCryptographicPrimitives,
17+
AwsCryptographicMaterialProviders
18+
]
1219
)
1320
service AwsEncryptionSdk {
1421
version: "2020-10-24",
@@ -77,6 +84,12 @@ structure DecryptInput {
7784
// One of keyring or CMM are required
7885
materialsManager: aws.cryptography.materialProviders#CryptographicMaterialsManagerReference,
7986
keyring: aws.cryptography.materialProviders#KeyringReference,
87+
//= aws-encryption-sdk-specification/client-apis/keyring-interface.md#onencrypt
88+
//= type=implication
89+
//# The following inputs to this behavior MUST be OPTIONAL:
90+
// (blank line for duvet)
91+
//# - [Encryption Context](#encryption-context)
92+
encryptionContext: aws.cryptography.materialProviders#EncryptionContext,
8093
}
8194

8295
structure DecryptOutput {

0 commit comments

Comments
 (0)