Skip to content

Commit

Permalink
add v2
Browse files Browse the repository at this point in the history
  • Loading branch information
@josecorella
josecorella committed Nov 15, 2024
1 parent d51d649 commit c33924f
Show file tree
Hide file tree
Showing 4 changed files with 83 additions and 157 deletions.
13 changes: 10 additions & 3 deletions .github/workflows/library_legacy_interop_test_vectors.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down Expand Up @@ -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
make test_decrypt_encrypt_vectors_net_legacy
4 changes: 2 additions & 2 deletions TestVectors/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
192 changes: 71 additions & 121 deletions TestVectors/dafny/TestVectors/src/ParseEsdkJsonManifest.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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
Expand All @@ -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);
}

Expand All @@ -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(
Expand Down Expand Up @@ -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<EsdkEncryptTestVector, string>
// 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,
Expand Down Expand Up @@ -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<EsdkDecryptTestVector, string>
// 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<EsdkDecryptTestVector, string>
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,
Expand Down
31 changes: 0 additions & 31 deletions TestVectors/dafny/TestVectors/test/RunMain.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down

0 comments on commit c33924f

Please sign in to comment.