Skip to content

Commit 0a53669

Browse files
josecorellajosecorella
authored
test: add support for legacy test vectors (#695)
1 parent fdd25ad commit 0a53669

File tree

9 files changed

+328
-125
lines changed

9 files changed

+328
-125
lines changed

‎.github/workflows/library_legacy_interop_test_vectors.yml

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
1+
# This workflow performs legacy test vector tests across the supported runtimes of the ESDK Dafny
2+
name: Library Interoperability Dafny TestVectors
3+
4+
on:
5+
workflow_call:
6+
inputs:
7+
dafny:
8+
description: "The Dafny version to use"
9+
required: true
10+
type: string
11+
regenerate-code:
12+
description: "Regenerate code using smithy-dafny"
13+
required: false
14+
default: false
15+
type: boolean
16+
17+
jobs:
18+
decryptEncryptVectors:
19+
strategy:
20+
matrix:
21+
library: [TestVectors]
22+
os: [
23+
# https://taskei.amazon.dev/tasks/CrypTool-5283
24+
# windows-latest,
25+
ubuntu-latest,
26+
macos-13,
27+
]
28+
# java struggles with the json parsing
29+
# however; the native java esdk already runs a subset of these decrypt
30+
# vectors. More important for the dafny-x implementations to be able
31+
# to decrypt these
32+
language: [net]
33+
legacy_zips: [
34+
aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5,
35+
aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.7,
36+
aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.8,
37+
aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-2.0.0,
38+
aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-2.2.0,
39+
aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-2.3.0
40+
]
41+
# https://taskei.amazon.dev/tasks/CrypTool-5284
42+
dotnet-version: ["6.0.x"]
43+
runs-on: ${{ matrix.os }}
44+
permissions:
45+
id-token: write
46+
contents: read
47+
48+
steps:
49+
- name: Support longpaths on Git checkout
50+
run: |
51+
git config --global core.longpaths true
52+
53+
- uses: actions/checkout@v3
54+
with:
55+
submodules: true
56+
# Not all submodules are needed.
57+
# We manually pull the submodule we DO need.
58+
- run: git submodule update --init libraries
59+
- run: git submodule update --init --recursive mpl
60+
61+
# Set up runtimes
62+
- name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
63+
if: matrix.language == 'net'
64+
uses: actions/setup-dotnet@v3
65+
with:
66+
dotnet-version: ${{ matrix.dotnet-version }}
67+
68+
- name: Setup Java 17
69+
if: matrix.language == 'java'
70+
uses: actions/setup-java@v3
71+
with:
72+
distribution: "corretto"
73+
java-version: 17
74+
75+
- name: Setup Dafny
76+
uses: dafny-lang/[email protected]
77+
with:
78+
dafny-version: ${{ inputs.dafny }}
79+
80+
- name: Regenerate code using smithy-dafny if necessary
81+
if: ${{ inputs.regenerate-code }}
82+
uses: ./.github/actions/polymorph_codegen
83+
with:
84+
dafny: ${{ inputs.dafny }}
85+
library: ${{ matrix.library }}
86+
diff-generated-code: false
87+
88+
# Build implementation for each runtime
89+
- name: Build ${{ matrix.library }} implementation in Java
90+
if: matrix.language == 'java'
91+
shell: bash
92+
working-directory: ./${{ matrix.library }}
93+
run: |
94+
# This works because `node` is installed by default on GHA runners
95+
CORES=$(node -e 'console.log(os.cpus().length)')
96+
make build_java CORES=$CORES
97+
98+
- name: Build ${{ matrix.library }} implementation in .NET
99+
if: matrix.language == 'net'
100+
shell: bash
101+
working-directory: ./${{ matrix.library }}
102+
run: |
103+
# This works because `node` is installed by default on GHA runners
104+
CORES=$(node -e 'console.log(os.cpus().length)')
105+
make transpile_net
106+
107+
- name: Setup gradle
108+
if: matrix.language == 'java'
109+
uses: gradle/gradle-build-action@v2
110+
with:
111+
gradle-version: 7.2
112+
113+
# TestVectors will call KMS
114+
- name: Configure AWS Credentials
115+
uses: aws-actions/configure-aws-credentials@v2
116+
with:
117+
aws-region: us-west-2
118+
role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2
119+
role-session-name: LegacyInterOpTests
120+
121+
# Extract test vector zips
122+
- name: Unzip legacy test vectors
123+
working-directory: ./${{matrix.library}}
124+
run: |
125+
unzip ${{matrix.legacy_zips}}.zip -d ${{matrix.legacy_zips}}
126+
127+
# Test Legacy Vectors
128+
- name: Test legacy vectors via CLI
129+
working-directory: ./${{matrix.library}}
130+
env:
131+
MANIFEST_PATH: ${{matrix.legacy_zips}}/
132+
MANIFEST_NAME: ${{ matrix.legacy_zips == 'aws-encryption-sdk-test-vectors/vectors/awses-decrypt/python-1.3.5' && 'decrypt_message.json' || 'manifest.json'}}
133+
run: |
134+
make test_decrypt_encrypt_vectors_net_legacy
135+

‎.github/workflows/pull.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,3 +29,7 @@ jobs:
2929
uses: ./.github/workflows/library_interop_test_vectors.yml
3030
with:
3131
dafny: '4.8.1'
32+
pr-dafny-legacy-test-vectors:
33+
uses: ./.github/workflows/library_legacy_interop_test_vectors.yml
34+
with:
35+
dafny: '4.8.1'

‎TestVectors/Makefile

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -99,13 +99,19 @@ test_encrypt_vectors_net:
9999
dotnet run --project runtimes/net --framework $(FRAMEWORK) encrypt --manifest-path runtimes/net --decrypt-manifest-path runtimes/net
100100

101101
test_decrypt_encrypt_vectors_java:
102-
gradle -p runtimes/java run --args="decrypt --manifest-path ."
102+
gradle -p runtimes/java run --args="decrypt --manifest-path . --manifest-name decrypt-manifest.json"
103103

104104
test_decrypt_encrypt_vectors_net: FRAMEWORK=net6.0
105105
test_decrypt_encrypt_vectors_net:
106106
dotnet restore runtimes/net
107107
dotnet build runtimes/net
108-
dotnet run --project runtimes/net --framework $(FRAMEWORK) decrypt --manifest-path runtimes/net
108+
dotnet run --project runtimes/net --framework $(FRAMEWORK) decrypt --manifest-path runtimes/net --manifest-name decrypt-manifest.json
109+
110+
test_decrypt_encrypt_vectors_net_legacy: FRAMEWORK=net6.0
111+
test_decrypt_encrypt_vectors_net_legacy:
112+
dotnet restore runtimes/net
113+
dotnet build runtimes/net
114+
dotnet run --project runtimes/net --framework $(FRAMEWORK) decrypt --manifest-path $(MANIFEST_PATH) --manifest-name $(MANIFEST_NAME)
109115

110116
_polymorph_dependencies:
111117
@echo "No polymorphing of dependency"

‎TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ module {:options "-functionSyntax:4"} EsdkManifestOptions {
99
datatype ManifestOptions =
1010
| Decrypt(
1111
nameonly manifestPath: string,
12+
nameonly manifestFileName: string,
1213
nameonly testName: Option<string> := None
1314
)
1415
| Encrypt(

‎TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
3737
requires 0 < |op.manifestPath|
3838
requires Seq.Last(op.manifestPath) == '/'
3939
{
40-
var decryptManifest :- expect GetManifest(op.manifestPath, "decrypt-manifest.json");
40+
var decryptManifest :- expect GetManifest(op.manifestPath, op.manifestFileName);
4141
:- Need(decryptManifest.DecryptManifest?, "Not a decrypt manifest");
4242

4343
var decryptVectors :- ParseEsdkJsonManifest.BuildDecryptTestVector(
@@ -73,7 +73,6 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
7373
{
7474
var vector := vectors[i];
7575
if TestDecryptVector?(vector) {
76-
:- Need(vector.algorithmSuiteId.Some?, "Vector without algorithm suite defined.");
7776
var pass := EsdkTestVectors.TestDecrypt(keys, vector);
7877
if !pass {
7978
hasFailure := true;
@@ -251,7 +250,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
251250
var decryptManifestBv :- FileIO.ReadBytesFromFile(manifestPath + manifestFileName);
252251
var decryptManifestBytes := BvToBytes(decryptManifestBv);
253252
var manifestJson :- API.Deserialize(decryptManifestBytes)
254-
.MapFailure(( e: Errors.DeserializationError ) => e.ToString());
253+
.MapFailure(( e: Errors.DeserializationError ) => e.ToString());
255254
:- Need(manifestJson.Object?, "Not a JSON object");
256255

257256
var manifest :- GetObject("manifest", manifestJson.obj);

‎TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy

Lines changed: 41 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
5555
|| v == 4
5656
}
5757

58-
type SupportedEncryptVersion = v: nat | SupportedEncryptVersion?(v) witness 4
58+
type SupportedEncryptVersion = v: nat | SupportedEncryptVersion?(v) witness 1
5959
predicate SupportedEncryptVersion?(v: nat)
6060
{
6161
|| v == 1
@@ -151,6 +151,21 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
151151
description: string,
152152
decryptionMethod: DecryptionMethod
153153
)
154+
| PositiveV1OrV2DecryptTestVector(
155+
id: string,
156+
version: SupportedDecryptVersion,
157+
manifestPath: string,
158+
ciphertextPath: string,
159+
plaintextPath: string,
160+
reproducedEncryptionContext: Option<mplTypes.EncryptionContext> := None,
161+
requiredEncryptionContextKeys: Option<mplTypes.EncryptionContextKeys> := None,
162+
decryptDescriptions: KeyVectorsTypes.KeyDescription,
163+
commitmentPolicy: mplTypes.ESDKCommitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT,
164+
frameLength: Option<int64>,
165+
algorithmSuiteId: Option<mplTypes.AlgorithmSuiteInfo>,
166+
description: string,
167+
decryptionMethod: DecryptionMethod
168+
)
154169

155170
datatype DecryptionMethod =
156171
| StreamingUnsignedOnly
@@ -164,10 +179,13 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
164179
requires keys.ValidState()
165180
modifies keys.Modifies
166181
ensures keys.ValidState()
167-
requires vector.algorithmSuiteId.Some?
168182
{
169-
var id := AllAlgorithmSuites.ToHex(vector.algorithmSuiteId.value);
170-
print "\nTEST-DECRYPT===> ", vector.id, "\n", id, " ", vector.description, "\n";
183+
if vector.algorithmSuiteId.Some? {
184+
var id := AllAlgorithmSuites.ToHex(vector.algorithmSuiteId.value);
185+
print "\nTEST-DECRYPT===> ", vector.id, "\n", id, " ", vector.description, "\n";
186+
} else {
187+
print "\nTEST-DECRYPT===> ", vector.id, "\n", vector.description, "\n";
188+
}
171189

172190
// The decrypt test vectors also test initialization
173191
// This is because they were developed when the MPL
@@ -183,7 +201,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
183201

184202
var ciphertext :- expect ReadVectorsFile(test.vector.manifestPath + test.vector.ciphertextPath);
185203
var plaintext;
186-
if test.vector.PositiveDecryptTestVector? {
204+
if test.vector.PositiveDecryptTestVector? || test.vector.PositiveV1OrV2DecryptTestVector? {
187205
plaintext :- expect ReadVectorsFile(test.vector.manifestPath + test.vector.plaintextPath);
188206
}
189207

@@ -203,9 +221,13 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
203221
&& result.value.plaintext == plaintext
204222
case NegativeDecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_)
205223
=>
206-
&& result.Failure?;
224+
&& result.Failure?
225+
case PositiveV1OrV2DecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_)
226+
=>
227+
&& result.Success?
228+
&& result.value.plaintext == plaintext;
207229
if !output {
208-
if test.vector.PositiveDecryptTestVector? && result.Failure? {
230+
if (test.vector.PositiveDecryptTestVector? || test.vector.PositiveV1OrV2DecryptTestVector?) && result.Failure? {
209231
print result.error, "\n";
210232
if
211233
&& result.error.AwsCryptographyMaterialProviders?
@@ -218,7 +240,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
218240
}
219241
}
220242

221-
method DecryptVectorToDecryptTest(
243+
method {:vcs_split_on_every_assert} DecryptVectorToDecryptTest(
222244
keys: KeyVectors.KeyVectorsClient,
223245
vector: EsdkDecryptTestVector
224246
)
@@ -233,14 +255,23 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
233255
&& fresh(output.value.cmm.Modifies - keys.Modifies)
234256
&& fresh(output.value.client.Modifies)
235257
{
258+
:- Need(
259+
!vector.NegativeDecryptTestVector?,
260+
KeyVectorsTypes.KeyVectorException(message := "Negative Test Vectors not supported at this time")
261+
);
236262
var cmm :- keys.CreateWrappedTestVectorCmm(
237263
KeyVectorsTypes.TestVectorCmmInput(
238264
keyDescription := vector.decryptDescriptions,
239265
forOperation := KeyVectorsTypes.DECRYPT
240266
));
241267

242-
:- Need(vector.algorithmSuiteId.Some?, KeyVectorsTypes.KeyVectorException(message := "Missing AlgorithmSuiteId in test vector"));
243-
var commitmentPolicy := AllAlgorithmSuites.GetCompatibleCommitmentPolicy(vector.algorithmSuiteId.value);
268+
var commitmentPolicy := if vector.algorithmSuiteId.Some? then
269+
AllAlgorithmSuites.GetCompatibleCommitmentPolicy(vector.algorithmSuiteId.value)
270+
else
271+
// If the manifest does not contain a field for the algorithm suite then we default the
272+
// commitment policy to FORBID_ENCRYPT_ALLOW_DECRYPT. This is currently only triggered
273+
// when we read v1 manifests.
274+
mplTypes.CommitmentPolicy.ESDK(mplTypes.ESDKCommitmentPolicy.FORBID_ENCRYPT_ALLOW_DECRYPT);
244275
:- Need(commitmentPolicy.ESDK?, KeyVectorsTypes.KeyVectorException(message := "Compatible commitment policy is not for ESDK"));
245276

246277
var config := WrappedESDK.WrappedAwsEncryptionSdkConfigWithSuppliedCommitment(

‎TestVectors/dafny/TestVectors/src/Index.dfy

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ module {:options "-functionSyntax:4"} WrappedESDKMain {
2121
Param.Command(Options("decrypt", "decrypt command for test-vectors",
2222
[
2323
Param.Opt("manifest-path", "relative path to the location of the manifest", unused := Required),
24+
Param.Opt("manifest-name", "name of file that contains the decrypt vectors file", unused := Required),
2425
Param.Opt("test-name", "id of the test to run")
2526
])),
2627
Param.Command(Options("encrypt", "encrypt command for test-vectors",
@@ -50,7 +51,7 @@ module {:options "-functionSyntax:4"} WrappedESDKMain {
5051
if op?.Success? {
5152
var op := op?.value;
5253
match op
53-
case Decrypt(_, _) =>
54+
case Decrypt(_, _, _) =>
5455
var result := EsdkTestManifests.StartDecryptVectors(op);
5556
if result.Failure? {
5657
print result.error;
@@ -97,12 +98,17 @@ module {:options "-functionSyntax:4"} WrappedESDKMain {
9798
{
9899
var manifestPath? := OptValue(params, "manifest-path");
99100
var testName? := OptValue(params, "test-name");
101+
var manifestFileName? := OptValue(params, "manifest-name");
100102

101103
var manifestPath := if manifestPath?.Some? then manifestPath?.value else ".";
102104
:- Need(0 < |manifestPath|, "Invalid manifest path length\n");
103105

106+
:- Need(manifestFileName?.Some?, "Must supply manifest file name");
107+
var manifestFileName := manifestFileName?.value;
108+
104109
Success(EsdkManifestOptions.Decrypt(
105110
manifestPath := if Seq.Last(manifestPath) == '/' then manifestPath else manifestPath + "/",
111+
manifestFileName := manifestFileName,
106112
testName := if testName?.Some? then testName? else None
107113
))
108114
}

0 commit comments

Comments
 (0)