chore: add test for VersionKey with an MRK (#296)

* chore: add test for VersionKey with an MRK

.github/workflows/library_dafny_verification.yml

@@ -53,7 +53,7 @@ jobs:
           dafny-version: ${{ inputs.dafny }}
 
       # dafny-reportgenerator requires next6
-      # but only 7.0 is installed on macos-latest-large
+      # but only 7.0 is installed on macos-12-large
       - name: Setup .NET Core SDK '6.0.x'
         uses: actions/setup-dotnet@v3
         with:

.github/workflows/library_java_tests.yml

@@ -32,7 +32,7 @@ jobs:
             # TODO just test on mac for now
             # windows-latest,
             ubuntu-latest,
-            macos-latest,
+            macos-12,
           ]
     runs-on: ${{ matrix.os }}
     permissions:

.github/workflows/library_net_tests.yml

@@ -29,7 +29,7 @@ jobs:
             TestVectorsAwsCryptographicMaterialProviders,
           ]
         dotnet-version: ["6.0.x"]
-        os: [windows-latest, ubuntu-latest, macos-latest]
+        os: [windows-latest, ubuntu-latest, macos-12]
     runs-on: ${{ matrix.os }}
     defaults:
       run:

.github/workflows/sem_ver.yml

@@ -6,7 +6,7 @@ on:
 
 jobs:
   semantic-release:
-    runs-on: macos-latest
+    runs-on: macos-12
     permissions:
       id-token: write
       contents: read

.github/workflows/semantic_release.yml

@@ -15,7 +15,7 @@ jobs:
     # privileged operation, so we must make sure this list of users is a subset of the users labeled as maintainers of
     # https://github.com/orgs/aws/teams/aws-crypto-tools
     if: contains('["seebees","texastony","ShubhamChaturvedi7","lucasmcdonald3","josecorella","imabhichow","rishav-karanjit","antonf-amzn","justplaz","ajewellamz"]', github.actor)
-    runs-on: macos-latest
+    runs-on: macos-12
     permissions:
       id-token: write
       contents: write

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestVersionKey.dfy

@@ -88,6 +88,103 @@ module TestVersionKey {
     expect getBranchKeyVersionResult.branchKeyMaterials.branchKey != newActiveResult.branchKeyMaterials.branchKey;
   }
 
+  method {:test} TestMrkVersionKey()
+  {
+    var ddbClient :- expect DDB.DynamoDBClient();
+
+    var eastKeyStoreConfig := Types.KeyStoreConfig(
+      id := None,
+      kmsConfiguration := KmsMrkConfigEast,
+      logicalKeyStoreName := logicalKeyStoreName,
+      grantTokens := None,
+      ddbTableName := branchKeyStoreName,
+      ddbClient := Some(ddbClient)
+    );
+
+    var westKeyStoreConfig := Types.KeyStoreConfig(
+      id := None,
+      kmsConfiguration := KmsMrkConfigWest,
+      logicalKeyStoreName := logicalKeyStoreName,
+      grantTokens := None,
+      ddbTableName := branchKeyStoreName,
+      ddbClient := Some(ddbClient)
+    );
+
+    var eastKeyStore :- expect KeyStore.KeyStore(eastKeyStoreConfig);
+    var westKeyStore :- expect KeyStore.KeyStore(westKeyStoreConfig);
+
+    // Create a new key with the WEST key store
+    // We will create a use this new key per run to avoid tripping up
+    // when running in different runtimes
+    var branchKeyId :- expect westKeyStore.CreateKey(Types.CreateKeyInput(
+                                                       branchKeyIdentifier := None,
+                                                       encryptionContext := None
+                                                     ));
+
+    var oldActiveResult :- expect westKeyStore.GetActiveBranchKey(
+      Types.GetActiveBranchKeyInput(
+        branchKeyIdentifier := branchKeyId.branchKeyIdentifier
+      ));
+
+    var oldActiveVersion :- expect UTF8.Decode(oldActiveResult.branchKeyMaterials.branchKeyVersion);
+
+    // Version the key with the EAST key store
+    var versionKeyResult :- expect eastKeyStore.VersionKey(
+      Types.VersionKeyInput(
+        branchKeyIdentifier := branchKeyId.branchKeyIdentifier
+      ));
+
+    var getBranchKeyVersionResultWest :- expect westKeyStore.GetBranchKeyVersion(
+      Types.GetBranchKeyVersionInput(
+        branchKeyIdentifier := branchKeyId.branchKeyIdentifier,
+        // We get the old active key by using the version
+        branchKeyVersion := oldActiveVersion
+      )
+    );
+
+    var getBranchKeyVersionResultEast :- expect eastKeyStore.GetBranchKeyVersion(
+      Types.GetBranchKeyVersionInput(
+        branchKeyIdentifier := branchKeyId.branchKeyIdentifier,
+        // We get the old active key by using the version
+        branchKeyVersion := oldActiveVersion
+      )
+    );
+    if (getBranchKeyVersionResultWest != getBranchKeyVersionResultEast) {
+      print "getBranchKeyVersionResultWest\n", getBranchKeyVersionResultWest, "\n";
+      print "getBranchKeyVersionResultEast\n", getBranchKeyVersionResultEast, "\n";
+    }
+    expect getBranchKeyVersionResultWest == getBranchKeyVersionResultEast;
+
+    var newActiveResultWest :- expect westKeyStore.GetActiveBranchKey(
+      Types.GetActiveBranchKeyInput(
+        branchKeyIdentifier := branchKeyId.branchKeyIdentifier
+      ));
+    var newActiveResultEast :- expect eastKeyStore.GetActiveBranchKey(
+      Types.GetActiveBranchKeyInput(
+        branchKeyIdentifier := branchKeyId.branchKeyIdentifier
+      ));
+
+    expect newActiveResultWest == newActiveResultEast;
+
+    var newActiveVersionWest :- expect UTF8.Decode(newActiveResultWest.branchKeyMaterials.branchKeyVersion);
+    var newActiveVersionEast :- expect UTF8.Decode(newActiveResultEast.branchKeyMaterials.branchKeyVersion);
+    expect newActiveVersionWest == newActiveVersionEast;
+
+    // Since this process uses a read DDB table,
+    // the number of records will forever increase.
+    // To avoid this, remove the items.
+    CleanupItems.DeleteVersion(branchKeyId.branchKeyIdentifier, newActiveVersionEast, ddbClient);
+    CleanupItems.DeleteVersion(branchKeyId.branchKeyIdentifier, oldActiveVersion, ddbClient);
+    CleanupItems.DeleteActive(branchKeyId.branchKeyIdentifier, ddbClient);
+
+    // We expect that getting the old active key has the same version as getting a branch key through the get version key api
+    expect getBranchKeyVersionResultEast.branchKeyMaterials.branchKeyVersion == oldActiveResult.branchKeyMaterials.branchKeyVersion;
+    expect getBranchKeyVersionResultEast.branchKeyMaterials.branchKey == oldActiveResult.branchKeyMaterials.branchKey;
+    // We expect that if we rotate the branch key, the returned materials MUST NOT be equal to the previous active key.
+    expect getBranchKeyVersionResultEast.branchKeyMaterials.branchKeyVersion != newActiveResultEast.branchKeyMaterials.branchKeyVersion;
+    expect getBranchKeyVersionResultEast.branchKeyMaterials.branchKey != newActiveResultEast.branchKeyMaterials.branchKey;
+  }
+
   method {:test} InsertingADuplicateVersionWillFail()
   {
     var ddbClient :- expect DDB.DynamoDBClient();