chore: Refactor Test Vector framework (#96)

Co-authored-by: José Corella <[email protected]>
aws · Jan 31, 2024 · 29c6a2c · 29c6a2c
1 parent ba87b29
commit 29c6a2c
Show file tree

Hide file tree

Showing 62 changed files with 34,096 additions and 2,285 deletions.
diff --git a/Makefile b/Makefile
@@ -71,4 +71,5 @@ duvet_report:
 		--source-pattern "AwsCryptographicMaterialProviders/compliance_exceptions/**/*.txt" \
 		--source-pattern "TestVectorsAwsCryptographicMaterialProviders/compliance_exceptions/**/*.txt" \
 		--source-pattern "(# //=,# //#).github/workflows/duvet.yaml" \
+		--source-pattern "TestVectorsAwsCryptographicMaterialProviders/dafny/**/src/**/*.dfy" \
 		--html specification_compliance_report.html
diff --git a/StandardLibrary/src/Index.dfy b/StandardLibrary/src/Index.dfy
@@ -7,6 +7,7 @@ include "./Base64.dfy"
 include "./Base64Lemmas.dfy"
 include "./ConcurrentCall.dfy"
 include "./FloatCompare.dfy"
+include "./GetOpt.dfy"
 include "./HexStrings.dfy"
 include "./Sets.dfy"
 include "./Sorting.dfy"

diff --git a/TestVectorsAwsCryptographicMaterialProviders/README.md b/TestVectorsAwsCryptographicMaterialProviders/README.md
@@ -0,0 +1,17 @@
+# Test Vectors for AWS Cryptographic Material Providers Library
+
+The TestVectorsAwsCryptographicMaterialProviders is responsible for creating Test Vectors used to test all the combinations of features available in the AWS Cryptographic Material Providers Library.
+
+This project is used as part of AWS Crypto Tools' CI/CD process to test functionality and compatibility across language implementations.
+
+This project does not adhere to semantic versioning; as such it makes no guarantees that functionality will persist across major, minor, or patch versions.
+**DO NOT** take a standalone dependency on this library.
+
+[Security issue notifications](./CONTRIBUTING.md#security-issue-notifications)
+
+## Security
+
+If you discover a potential security issue in this project
+we ask that you notify AWS/Amazon Security via our
+[vulnerability reporting page](http://aws.amazon.com/security/vulnerability-reporting/).
+Please **do not** create a public GitHub issue.
diff --git a/...lProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy b/...lProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy
@@ -16,6 +16,9 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
 
   // Begin Generated Types
 
+  datatype CmmOperation =
+    | ENCRYPT
+    | DECRYPT
   datatype GetKeyDescriptionInput = | GetKeyDescriptionInput (
     nameonly json: seq<uint8>
   )
@@ -34,15 +37,20 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
     | Static(Static: StaticKeyring)
     | KmsRsa(KmsRsa: KmsRsaKeyring)
     | Hierarchy(Hierarchy: HierarchyKeyring)
+    | Multi(Multi: MultiKeyring)
+    | RequiredEncryptionContext(RequiredEncryptionContext: RequiredEncryptionContextCMM)
+  type KeyDescriptionList = seq<KeyDescription>
   class IKeyVectorsClientCallHistory {
     ghost constructor() {
       CreateTestVectorKeyring := [];
-      CreateWappedTestVectorKeyring := [];
+      CreateWrappedTestVectorKeyring := [];
+      CreateWrappedTestVectorCmm := [];
       GetKeyDescription := [];
       SerializeKeyDescription := [];
     }
     ghost var CreateTestVectorKeyring: seq<DafnyCallEvent<TestVectorKeyringInput, Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>>>
-    ghost var CreateWappedTestVectorKeyring: seq<DafnyCallEvent<TestVectorKeyringInput, Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>>>
+    ghost var CreateWrappedTestVectorKeyring: seq<DafnyCallEvent<TestVectorKeyringInput, Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>>>
+    ghost var CreateWrappedTestVectorCmm: seq<DafnyCallEvent<TestVectorCmmInput, Result<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager, Error>>>
     ghost var GetKeyDescription: seq<DafnyCallEvent<GetKeyDescriptionInput, Result<GetKeyDescriptionOutput, Error>>>
     ghost var SerializeKeyDescription: seq<DafnyCallEvent<SerializeKeyDescriptionInput, Result<SerializeKeyDescriptionOutput, Error>>>
   }
@@ -93,14 +101,14 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
       ensures CreateTestVectorKeyringEnsuresPublicly(input, output)
       ensures History.CreateTestVectorKeyring == old(History.CreateTestVectorKeyring) + [DafnyCallEvent(input, output)]
 
-    predicate CreateWappedTestVectorKeyringEnsuresPublicly(input: TestVectorKeyringInput , output: Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>)
+    predicate CreateWrappedTestVectorKeyringEnsuresPublicly(input: TestVectorKeyringInput , output: Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>)
     // The public method to be called by library consumers
-    method CreateWappedTestVectorKeyring ( input: TestVectorKeyringInput )
+    method CreateWrappedTestVectorKeyring ( input: TestVectorKeyringInput )
       returns (output: Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>)
       requires
         && ValidState()
       modifies Modifies - {History} ,
-               History`CreateWappedTestVectorKeyring
+               History`CreateWrappedTestVectorKeyring
       // Dafny will skip type parameters when generating a default decreases clause.
       decreases Modifies - {History}
       ensures
@@ -110,8 +118,28 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
                && output.value.Modifies !! {History}
                && fresh(output.value)
                && fresh ( output.value.Modifies - Modifies - {History} ) )
-      ensures CreateWappedTestVectorKeyringEnsuresPublicly(input, output)
-      ensures History.CreateWappedTestVectorKeyring == old(History.CreateWappedTestVectorKeyring) + [DafnyCallEvent(input, output)]
+      ensures CreateWrappedTestVectorKeyringEnsuresPublicly(input, output)
+      ensures History.CreateWrappedTestVectorKeyring == old(History.CreateWrappedTestVectorKeyring) + [DafnyCallEvent(input, output)]
+
+    predicate CreateWrappedTestVectorCmmEnsuresPublicly(input: TestVectorCmmInput , output: Result<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager, Error>)
+    // The public method to be called by library consumers
+    method CreateWrappedTestVectorCmm ( input: TestVectorCmmInput )
+      returns (output: Result<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager, Error>)
+      requires
+        && ValidState()
+      modifies Modifies - {History} ,
+               History`CreateWrappedTestVectorCmm
+      // Dafny will skip type parameters when generating a default decreases clause.
+      decreases Modifies - {History}
+      ensures
+        && ValidState()
+        && ( output.Success? ==>
+               && output.value.ValidState()
+               && output.value.Modifies !! {History}
+               && fresh(output.value)
+               && fresh ( output.value.Modifies - Modifies - {History} ) )
+      ensures CreateWrappedTestVectorCmmEnsuresPublicly(input, output)
+      ensures History.CreateWrappedTestVectorCmm == old(History.CreateWrappedTestVectorCmm) + [DafnyCallEvent(input, output)]
 
     // Functions are deterministic, no need for historical call events or ensures indirection
     // The public method to be called by library consumers
@@ -127,7 +155,7 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
 
   }
   datatype KeyVectorsConfig = | KeyVectorsConfig (
-    nameonly keyManifiestPath: string
+    nameonly keyManifestPath: string
   )
   datatype KMSInfo = | KMSInfo (
     nameonly keyId: string
@@ -144,6 +172,10 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
     nameonly keyId: string ,
     nameonly encryptionAlgorithm: ComAmazonawsKmsTypes.EncryptionAlgorithmSpec
   )
+  datatype MultiKeyring = | MultiKeyring (
+    nameonly generator: Option<KeyDescription> ,
+    nameonly childKeyrings: KeyDescriptionList
+  )
   datatype RawAES = | RawAES (
     nameonly keyId: string ,
     nameonly providerId: string
@@ -153,6 +185,10 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
     nameonly providerId: string ,
     nameonly padding: AwsCryptographyMaterialProvidersTypes.PaddingScheme
   )
+  datatype RequiredEncryptionContextCMM = | RequiredEncryptionContextCMM (
+    nameonly underlying: KeyDescription ,
+    nameonly requiredEncryptionContextKeys: AwsCryptographyMaterialProvidersTypes.EncryptionContextKeys
+  )
   datatype SerializeKeyDescriptionInput = | SerializeKeyDescriptionInput (
     nameonly keyDescription: KeyDescription
   )
@@ -162,6 +198,10 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
   datatype StaticKeyring = | StaticKeyring (
     nameonly keyId: string
   )
+  datatype TestVectorCmmInput = | TestVectorCmmInput (
+    nameonly keyDescription: KeyDescription ,
+    nameonly forOperation: CmmOperation
+  )
   datatype TestVectorKeyringInput = | TestVectorKeyringInput (
     nameonly keyDescription: KeyDescription
   )
@@ -256,15 +296,15 @@ abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService
       History.CreateTestVectorKeyring := History.CreateTestVectorKeyring + [DafnyCallEvent(input, output)];
     }
 
-    predicate CreateWappedTestVectorKeyringEnsuresPublicly(input: TestVectorKeyringInput , output: Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>)
-    {Operations.CreateWappedTestVectorKeyringEnsuresPublicly(input, output)}
+    predicate CreateWrappedTestVectorKeyringEnsuresPublicly(input: TestVectorKeyringInput , output: Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>)
+    {Operations.CreateWrappedTestVectorKeyringEnsuresPublicly(input, output)}
     // The public method to be called by library consumers
-    method CreateWappedTestVectorKeyring ( input: TestVectorKeyringInput )
+    method CreateWrappedTestVectorKeyring ( input: TestVectorKeyringInput )
       returns (output: Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>)
       requires
         && ValidState()
       modifies Modifies - {History} ,
-               History`CreateWappedTestVectorKeyring
+               History`CreateWrappedTestVectorKeyring
       // Dafny will skip type parameters when generating a default decreases clause.
       decreases Modifies - {History}
       ensures
@@ -274,11 +314,36 @@ abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService
                && output.value.Modifies !! {History}
                && fresh(output.value)
                && fresh ( output.value.Modifies - Modifies - {History} ) )
-      ensures CreateWappedTestVectorKeyringEnsuresPublicly(input, output)
-      ensures History.CreateWappedTestVectorKeyring == old(History.CreateWappedTestVectorKeyring) + [DafnyCallEvent(input, output)]
+      ensures CreateWrappedTestVectorKeyringEnsuresPublicly(input, output)
+      ensures History.CreateWrappedTestVectorKeyring == old(History.CreateWrappedTestVectorKeyring) + [DafnyCallEvent(input, output)]
     {
-      output := Operations.CreateWappedTestVectorKeyring(config, input);
-      History.CreateWappedTestVectorKeyring := History.CreateWappedTestVectorKeyring + [DafnyCallEvent(input, output)];
+      output := Operations.CreateWrappedTestVectorKeyring(config, input);
+      History.CreateWrappedTestVectorKeyring := History.CreateWrappedTestVectorKeyring + [DafnyCallEvent(input, output)];
+    }
+
+    predicate CreateWrappedTestVectorCmmEnsuresPublicly(input: TestVectorCmmInput , output: Result<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager, Error>)
+    {Operations.CreateWrappedTestVectorCmmEnsuresPublicly(input, output)}
+    // The public method to be called by library consumers
+    method CreateWrappedTestVectorCmm ( input: TestVectorCmmInput )
+      returns (output: Result<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager, Error>)
+      requires
+        && ValidState()
+      modifies Modifies - {History} ,
+               History`CreateWrappedTestVectorCmm
+      // Dafny will skip type parameters when generating a default decreases clause.
+      decreases Modifies - {History}
+      ensures
+        && ValidState()
+        && ( output.Success? ==>
+               && output.value.ValidState()
+               && output.value.Modifies !! {History}
+               && fresh(output.value)
+               && fresh ( output.value.Modifies - Modifies - {History} ) )
+      ensures CreateWrappedTestVectorCmmEnsuresPublicly(input, output)
+      ensures History.CreateWrappedTestVectorCmm == old(History.CreateWrappedTestVectorCmm) + [DafnyCallEvent(input, output)]
+    {
+      output := Operations.CreateWrappedTestVectorCmm(config, input);
+      History.CreateWrappedTestVectorCmm := History.CreateWrappedTestVectorCmm + [DafnyCallEvent(input, output)];
     }
 
 
@@ -329,11 +394,11 @@ abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysOperations
     ensures CreateTestVectorKeyringEnsuresPublicly(input, output)
 
 
-  predicate CreateWappedTestVectorKeyringEnsuresPublicly(input: TestVectorKeyringInput , output: Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>)
+  predicate CreateWrappedTestVectorKeyringEnsuresPublicly(input: TestVectorKeyringInput , output: Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>)
   // The private method to be refined by the library developer
 
 
-  method CreateWappedTestVectorKeyring ( config: InternalConfig , input: TestVectorKeyringInput )
+  method CreateWrappedTestVectorKeyring ( config: InternalConfig , input: TestVectorKeyringInput )
     returns (output: Result<AwsCryptographyMaterialProvidersTypes.IKeyring, Error>)
     requires
       && ValidInternalConfig?(config)
@@ -346,7 +411,27 @@ abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysOperations
              && output.value.ValidState()
              && fresh(output.value)
              && fresh ( output.value.Modifies - ModifiesInternalConfig(config) ) )
-    ensures CreateWappedTestVectorKeyringEnsuresPublicly(input, output)
+    ensures CreateWrappedTestVectorKeyringEnsuresPublicly(input, output)
+
+
+  predicate CreateWrappedTestVectorCmmEnsuresPublicly(input: TestVectorCmmInput , output: Result<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager, Error>)
+  // The private method to be refined by the library developer
+
+
+  method CreateWrappedTestVectorCmm ( config: InternalConfig , input: TestVectorCmmInput )
+    returns (output: Result<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager, Error>)
+    requires
+      && ValidInternalConfig?(config)
+    modifies ModifiesInternalConfig(config)
+    // Dafny will skip type parameters when generating a default decreases clause.
+    decreases ModifiesInternalConfig(config)
+    ensures
+      && ValidInternalConfig?(config)
+      && ( output.Success? ==>
+             && output.value.ValidState()
+             && fresh(output.value)
+             && fresh ( output.value.Modifies - ModifiesInternalConfig(config) ) )
+    ensures CreateWrappedTestVectorCmmEnsuresPublicly(input, output)
 
 
   // Functions are deterministic, no need for historical call events or ensures indirection

diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/key-vectors.smithy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/key-vectors.smithy
@@ -11,27 +11,58 @@ service KeyVectors {
   resources: [],
   operations: [
     CreateTestVectorKeyring,
-    CreateWappedTestVectorKeyring,
+    CreateWrappedTestVectorKeyring,
+    CreateWrappedTestVectorCmm,
     GetKeyDescription,
     SerializeKeyDescription,
   ]
 }
 
 structure KeyVectorsConfig {
   @required
-  keyManifiestPath: String
+  keyManifestPath: String
 }
 
 operation CreateTestVectorKeyring {
   input: TestVectorKeyringInput,
   output: aws.cryptography.materialProviders#CreateKeyringOutput,
 }
 
-operation CreateWappedTestVectorKeyring {
+operation CreateWrappedTestVectorKeyring {
   input: TestVectorKeyringInput,
   output: aws.cryptography.materialProviders#CreateKeyringOutput,
 }
 
+operation CreateWrappedTestVectorCmm {
+  input: TestVectorCmmInput,
+  output: CreateWrappedTestVectorCmmOutput,
+}
+
+structure TestVectorCmmInput {
+  @required
+  keyDescription: KeyDescription,
+  @required
+  forOperation: CmmOperation,
+}
+
+@enum([
+  {
+    name: "ENCRYPT",
+    value: "ENCRYPT",
+  },
+  {
+    name: "DECRYPT",
+    value: "DECRYPT",
+  },
+])
+string CmmOperation
+
+@aws.polymorph#positional
+structure CreateWrappedTestVectorCmmOutput {
+  @required
+  cmm: aws.cryptography.materialProviders#CryptographicMaterialsManagerReference,
+}
+
 @readonly
 operation GetKeyDescription {
   input: GetKeyDescriptionInput,
@@ -62,10 +93,9 @@ structure SerializeKeyDescriptionOutput {
   json: Blob
 }
 
-
 structure TestVectorKeyringInput {
   @required
-  keyDescription: KeyDescription
+  keyDescription: KeyDescription,
 }
 
 union KeyDescription {
@@ -77,6 +107,8 @@ union KeyDescription {
   Static: StaticKeyring,
   KmsRsa: KmsRsaKeyring,
   Hierarchy: HierarchyKeyring,
+  Multi: MultiKeyring,
+  RequiredEncryptionContext: RequiredEncryptionContextCMM,
 }
 
 structure KMSInfo {
@@ -125,6 +157,22 @@ structure HierarchyKeyring {
   keyId: String,
 }
 
+structure MultiKeyring {
+  generator: KeyDescription,
+  @required
+  childKeyrings: KeyDescriptionList,
+}
+
+list KeyDescriptionList {
+  member: KeyDescription
+}
+
+structure RequiredEncryptionContextCMM {
+  @required
+  underlying: KeyDescription,
+  @required
+  requiredEncryptionContextKeys: aws.cryptography.materialProviders#EncryptionContextKeys
+}
 
 @error("client")
 structure KeyVectorException {