From 402d4c7fc81aee2ceac1967d8446ca7d57c7d46f Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Wed, 30 Oct 2024 12:08:37 -0700 Subject: [PATCH] start decrypt vectors --- .../dafny/ESDK/src/EsdkTestManifests.dfy | 39 ++++++++-------- .../dafny/ESDK/src/EsdkTestVectors.dfy | 39 ++++++++-------- .../dafny/ESDK/src/ParseEsdkJsonManifest.dfy | 4 +- .../VectorsComposition/AllEsdkV4NoReqEc.dfy | 6 ++- .../VectorsComposition/AllEsdkV4WithReqEc.dfy | 3 +- .../dafny/ESDK/src/WriteEsdkJsonManifests.dfy | 44 +++++++++++++++++-- TestVectors/dafny/ESDK/src/WriteVectors.dfy | 31 ++++++++++--- TestVectors/dafny/ESDK/test/RunMain.dfy | 20 +++++++-- 8 files changed, 130 insertions(+), 56 deletions(-) diff --git a/TestVectors/dafny/ESDK/src/EsdkTestManifests.dfy b/TestVectors/dafny/ESDK/src/EsdkTestManifests.dfy index a51ba6126..08a47d6ed 100644 --- a/TestVectors/dafny/ESDK/src/EsdkTestManifests.dfy +++ b/TestVectors/dafny/ESDK/src/EsdkTestManifests.dfy @@ -29,25 +29,26 @@ module {:options "-functionSyntax:4"} EsdkTestManifests { import opened EsdkTestVectors import WriteVectors - // method StartDecryptVectors( - // op: EsdkManifestOptions.ManifestOptions - // ) - // returns (output: Result, string>) - // requires op.Decrypt? - // requires 0 < |op.manifestPath| - // requires Seq.Last(op.manifestPath) == '/' - // { - // var decryptManifest :- expect GetManifest(op.manifestPath, "manifest.json"); - // :- Need(decryptManifest.DecryptManifest?, "Not a decrypt manifest"); - - // var decryptVectors :- ParseEsdkJsonManifest.BuildDecryptTestVector( - // op, - // decryptManifest.version, - // decryptManifest.keys, - // decryptManifest.jsonTests - // ); - // output := TestDecrypts(decryptManifest.keys, decryptVectors); - // } + method StartDecryptVectors( + op: EsdkManifestOptions.ManifestOptions + ) + returns (output: Result, string>) + requires op.Decrypt? + requires 0 < |op.manifestPath| + requires Seq.Last(op.manifestPath) == '/' + { + var decryptManifest :- expect GetManifest(op.manifestPath, "decrypt-manifest.json"); + :- Need(decryptManifest.DecryptManifest?, "Not a decrypt manifest"); + + // var decryptVectors :- ParseEsdkJsonManifest.BuildDecryptTestVector( + // op, + // decryptManifest.version, + // decryptManifest.keys, + // decryptManifest.jsonTests + // ); + // output := TestDecrypts(decryptManifest.keys, decryptVectors); + return Failure("Implement me!"); + } predicate TestDecryptVector?(v: EsdkDecryptTestVector) { diff --git a/TestVectors/dafny/ESDK/src/EsdkTestVectors.dfy b/TestVectors/dafny/ESDK/src/EsdkTestVectors.dfy index b4e5a8c68..26bbe2901 100644 --- a/TestVectors/dafny/ESDK/src/EsdkTestVectors.dfy +++ b/TestVectors/dafny/ESDK/src/EsdkTestVectors.dfy @@ -79,6 +79,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { commitmentPolicy: mplTypes.ESDKCommitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT, frameLength: Option, algorithmSuiteId: Option, + description: string, maxEncryptedDataKeys: Option := Some(1) ) | PositiveEncryptNegativeDecryptTestVector ( @@ -96,6 +97,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { frameLength: Option, algorithmSuiteId: Option, decryptErrorDescription: string, + description: string, maxEncryptedDataKeys: Option := Some(1) ) | NegativeEncryptTestVector( @@ -111,6 +113,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { frameLength: Option, algorithmSuiteId: Option, errorDescription: string, + description: string, maxEncryptedDataKeys: Option := Some(1) ) @@ -135,6 +138,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { commitmentPolicy: mplTypes.ESDKCommitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT, frameLength: Option, algorithmSuiteId: Option, + description: string, decryptionMethod: DecryptionMethod ) | NegativeDecryptTestVector( @@ -144,8 +148,12 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { ciphertextPath: string, errorDescription: string, encryptionContext: Option := None, + requiredEncryptionContextKeys: Option := None, decryptDescriptions: KeyVectorsTypes.KeyDescription, commitmentPolicy: mplTypes.ESDKCommitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT, + frameLength: Option, + algorithmSuiteId: Option, + description: string, decryptionMethod: DecryptionMethod ) @@ -277,7 +285,8 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { requires test.vector.frameLength.Some? ==> Types.IsValid_FrameLength(test.vector.frameLength.value) requires test.vector.algorithmSuiteId.Some? && test.vector.algorithmSuiteId.value.id.ESDK? { - print "\nTEST===> ", test.vector.name, "\n"; + var id := AllAlgorithmSuites.ToHex(test.vector.algorithmSuiteId.value); + print "\nTEST===> ", test.vector.name, "\n", id, " ", test.vector.description, "\n"; // The decrypt test vectors also test initialization // This is because they were developed when the MPL @@ -305,8 +314,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { || test.vector.PositiveEncryptNegativeDecryptTestVector? ) { - var name :- expect UUID.GenerateUUID(); - var decryptVector :- EncryptTestToDecryptVector(name, test, result.value); + var decryptVector :- EncryptTestToDecryptVector(test, result.value); output := Success(EncryptTestOutput( vector := Some(decryptVector), output := true @@ -370,7 +378,6 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { } method EncryptTestToDecryptVector( - name: string, test: EncryptTest, result: Types.EncryptOutput ) returns (output: Result) @@ -380,12 +387,12 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { requires test.vector.algorithmSuiteId.Some? { output := match test.vector - case PositiveEncryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_) => + case PositiveEncryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_,_) => Success(PositiveDecryptTestVector( - name := name, + name := test.vector.name, version := 3, manifestPath := test.vector.decryptManifestPath, - ciphertextPath := ciphertextPathPathRoot + name, + ciphertextPath := ciphertextPathPathRoot + test.vector.name, plaintextPath := plaintextPathRoot + test.vector.plaintextPath, encryptionContext := test.vector.encryptionContext, requiredEncryptionContextKeys := test.vector.requiredEncryptionContextKeys, @@ -393,23 +400,13 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { commitmentPolicy := test.vector.commitmentPolicy, frameLength := test.vector.frameLength, algorithmSuiteId := test.vector.algorithmSuiteId, + description := test.vector.description, decryptionMethod := DecryptionMethod.OneShot )) case _ => Failure("Only postive tests supported"); - // case PositiveEncryptNegativeDecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_,_) => - // NegativeDecryptTestVector( - // name := name, - // version := 2, - // manifestPath := test.vector.decryptManifestPath, - // ciphertextPath := ciphertextPathPathRoot + name, - // errorDescription := test.vector.decryptErrorDescription, - // encryptionContext := test.vector.encryptionContext, - // decryptDescriptions := [test.vector.decryptDescriptions], - // commitmentPolicy := test.vector.commitmentPolicy, - // decryptionMethod := DecryptionMethod.OneShot - // ); - var decryptManifestCiphertext := test.vector.decryptManifestPath + ciphertextPathPathRoot + name; + + var decryptManifestCiphertext := test.vector.decryptManifestPath + ciphertextPathPathRoot + test.vector.name; // Side effect, to avoid thousands of ciphertext in memory... var _ :- expect WriteVectorsFile(decryptManifestCiphertext, result.ciphertext); } @@ -487,4 +484,4 @@ module {:options "-functionSyntax:4"} EsdkTestVectors { var bv := BytesBv(bytes); output := FileIO.WriteBytesToFile(location, bv); } -} +} \ No newline at end of file diff --git a/TestVectors/dafny/ESDK/src/ParseEsdkJsonManifest.dfy b/TestVectors/dafny/ESDK/src/ParseEsdkJsonManifest.dfy index ed71f8cc9..9f4c81734 100644 --- a/TestVectors/dafny/ESDK/src/ParseEsdkJsonManifest.dfy +++ b/TestVectors/dafny/ESDK/src/ParseEsdkJsonManifest.dfy @@ -262,6 +262,7 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { var encryptionContextStrings :- SmallObjectToStringStringMap(encryptionContextJsonKey, scenario); var encryptionContext :- utf8EncodeMap(encryptionContextStrings); + var description :- GetString("description", scenario); match typ case "positive-esdk" => @@ -278,7 +279,8 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest { encryptionContext := Some(encryptionContext), commitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT, frameLength := frameLength, - algorithmSuiteId := Some(algorithmSuite) + algorithmSuiteId := Some(algorithmSuite), + description := description )) case _ => Failure("Unsupported ESDK TestVector type: " + typ) diff --git a/TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4NoReqEc.dfy b/TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4NoReqEc.dfy index 38cba424a..60567f666 100644 --- a/TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4NoReqEc.dfy +++ b/TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4NoReqEc.dfy @@ -77,7 +77,8 @@ module {:options "/functionSyntax:4" } AllEsdkV4NoReqEc { encryptDescriptions := keyringConfig.encryptDescription, decryptDescriptions := keyringConfig.decryptDescription, frameLength := Some(frameSize), - algorithmSuiteId := Some(algorithmSuite) + algorithmSuiteId := Some(algorithmSuite), + description := keyringConfig.name ) const AllPositiveKeyringTestsNoDBEKmsRsa := @@ -94,7 +95,8 @@ module {:options "/functionSyntax:4" } AllEsdkV4NoReqEc { encryptDescriptions := keyringConfig.encryptDescription, decryptDescriptions := keyringConfig.decryptDescription, frameLength := Some(frameSize), - algorithmSuiteId := Some(algorithmSuite) + algorithmSuiteId := Some(algorithmSuite), + description := keyringConfig.name ) const Tests := diff --git a/TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4WithReqEc.dfy b/TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4WithReqEc.dfy index e8f539e22..d2cf8cd31 100644 --- a/TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4WithReqEc.dfy +++ b/TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4WithReqEc.dfy @@ -90,7 +90,8 @@ module {:options "/functionSyntax:4" } AllEsdkV4WithReqEc { requiredEncryptionContextKeys := config.requiredEncryptionContextKeys, requiredECDescription := Some(config.name), frameLength := Some(frameSize), - algorithmSuiteId := Some(algorithmSuite) + algorithmSuiteId := Some(algorithmSuite), + description := config.name ) const Tests := diff --git a/TestVectors/dafny/ESDK/src/WriteEsdkJsonManifests.dfy b/TestVectors/dafny/ESDK/src/WriteEsdkJsonManifests.dfy index 478e1f7cb..a55182077 100644 --- a/TestVectors/dafny/ESDK/src/WriteEsdkJsonManifests.dfy +++ b/TestVectors/dafny/ESDK/src/WriteEsdkJsonManifests.dfy @@ -80,12 +80,13 @@ module {:options "-functionSyntax:4"} WriteEsdkJsonManifests { var optionalValues := requiredEncryptionContextKeys + encryptionContext; match test - case PositiveEncryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_) => + case PositiveEncryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_,_) => var encrypt :- KeyDescription.ToJson(test.encryptDescriptions, 3); var decrypt :- KeyDescription.ToJson(test.decryptDescriptions, 3); var scenario := Object([ ("type", String("positive-esdk")), ("plaintext", String("small")), + ("description", String(test.description)), ("algorithmSuiteId", String(id)), ("frame-size", Number(Int(test.frameLength.value as int))), ("encryptKeyDescription", encrypt), @@ -195,11 +196,46 @@ module {:options "-functionSyntax:4"} WriteEsdkJsonManifests { // ] + reproducedEc + encryptionContext)) // } - function DecryptTestVectorToJson( + function {:vcs_split_on_every_assert} DecryptTestVectorToJson( test: EsdkTestVectors.EsdkDecryptTestVector ): Result { - // var id := AllAlgorithmSuites.ToHex(test); - Failure("whelp") + :- Need( + && test.algorithmSuiteId.Some? + && test.frameLength.Some?, + "test is missing algorithmSuite ID, or frameLength" + ); + var id := AllAlgorithmSuites.ToHex(test.algorithmSuiteId.value); + var description := test.name + " " + id; + + var encryptionContext + :- if test.encryptionContext.Some? then + EncryptionContextToJson("encryption-context", test.encryptionContext.value) + else + EncryptionContextToJson("encryption-context", map[]); + + :- Need( + |encryptionContext| == 1, + "Error parsing encryption context" + ); + + var requiredEncryptionContextKeys :- EncryptionContextKeysToJson(test.requiredEncryptionContextKeys); + var optionalValues := requiredEncryptionContextKeys + encryptionContext; + + match test + case PositiveDecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_) => + var decrypt :- KeyDescription.ToJson(test.decryptDescriptions, 3); + var scenario := Object([ + ("type", String("positive-esdk")), + ("ciphertext", String("file://ciphertexts/" + test.name)), + ("algorithmSuiteId", String(id)), + ("frame-size", Number(Int(test.frameLength.value as int))), + ("decryptKeyDescription", decrypt) + ] + optionalValues); + Success(Object([ + ("decryption-scenario", scenario) + ])) + case _ => + Failure("Only Positive Tests supported :(") } } diff --git a/TestVectors/dafny/ESDK/src/WriteVectors.dfy b/TestVectors/dafny/ESDK/src/WriteVectors.dfy index 9ac4a77ad..b1ab42899 100644 --- a/TestVectors/dafny/ESDK/src/WriteVectors.dfy +++ b/TestVectors/dafny/ESDK/src/WriteVectors.dfy @@ -74,9 +74,8 @@ module {:options "-functionSyntax:4"} WriteVectors { var id := AllAlgorithmSuites.ToHex(tests[i].algorithmSuiteId.value); var uuid :- expect UUID.GenerateUUID(); - var name := id + "-" + tests[i].name + "-" + uuid; var test :- WriteEsdkJsonManifests.EncryptTestVectorToJson(tests[i]); - testsJSON := testsJSON + [(name, test)]; + testsJSON := testsJSON + [(uuid, test)]; } var manifestJson := Object([ @@ -98,7 +97,7 @@ module {:options "-functionSyntax:4"} WriteVectors { var esdkEncryptManifestBv := JSONHelpers.BytesBv(esdkEncryptManifestBytes); var _ :- expect FileIO.WriteBytesToFile( - op.encryptManifestOutput + "manifest.json", + op.encryptManifestOutput + "encrypt-manifest.json", esdkEncryptManifestBv ); @@ -119,12 +118,34 @@ module {:options "-functionSyntax:4"} WriteVectors { for i := 0 to |tests| { - var name :- UUID.GenerateUUID(); + var name := tests[i].name; var test :- WriteEsdkJsonManifests.DecryptTestVectorToJson(tests[i]); testsJSON := testsJSON + [(name, test)]; } - return Failure("Whelp"); + var manifestJson := Object([ + ("type", String("awses-decrypt")), + ("version", Number(Int(3)))]); + + var esdkDecryptManifest := Object( + [ + ("manifest", manifestJson), + // TODO create an extern that gets that runtimes namespace and latest version + ("client", String("aws-encryption-sdk-dafny")), + ("keys", String("file://keys.json")), + ("tests", Object(testsJSON)) + ] + ); + + var esdkDecryptManifestBytes :- expect API.Serialize(esdkDecryptManifest); + var esdkDecryptManifestBv := JSONHelpers.BytesBv(esdkDecryptManifestBytes); + + var _ :- expect FileIO.WriteBytesToFile( + op.decryptManifestOutput + "decrypt-manifest.json", + esdkDecryptManifestBv + ); + + output := Success(()); } function getVersionTests(version: nat): (ret: Result, string>) diff --git a/TestVectors/dafny/ESDK/test/RunMain.dfy b/TestVectors/dafny/ESDK/test/RunMain.dfy index 70e68d024..106052445 100644 --- a/TestVectors/dafny/ESDK/test/RunMain.dfy +++ b/TestVectors/dafny/ESDK/test/RunMain.dfy @@ -70,7 +70,7 @@ module {:extern} TestWrappedESDKMain { method {:test} RunManifestTests() { TestGenerateEncryptManifest(); TestEncryptManifest(); - // TestDecryptManifest(); + TestDecryptManifest(); } method TestGenerateEncryptManifest() { @@ -91,8 +91,8 @@ module {:extern} TestWrappedESDKMain { var result := EsdkTestManifests.StartEncryptVectors( EsdkManifestOptions.Encrypt( manifestPath := directory + "dafny/TestVectors/test/", - manifest := "manifest.json", - decryptManifestOutput := directory + "dafny/TestVectors/" + manifest := "encrypt-manifest.json", + decryptManifestOutput := directory + "dafny/TestVectors/test" ) ); if result.Failure? { @@ -101,4 +101,18 @@ module {:extern} TestWrappedESDKMain { expect result.Success?; } + method TestDecryptManifest() + { + var directory := GetTestVectorExecutionDirectory(); + var result := EsdkTestManifests.StartDecryptVectors( + EsdkManifestOptions.Decrypt( + manifestPath := directory + "dafny/TestVectors/" + ) + ); + + if result.Failure? { + print result.error; + } + expect result.Success?; + } }