feat(dafny): Branch Key Store without modifying Encryption Context

.github/workflows/duvet.yaml

@@ -3,11 +3,12 @@
 # with respect to the specification
 name: Duvet report
 
-on:
-  pull_request:
-  push:
-    branches:
-      - main
+# TODO-HV-2 : Re-Enable Duvet once mutations/mutations Duvet is healthy
+# on:
+#   pull_request:
+#   push:
+#     branches:
+#       - main
 
 jobs:
   duvet:

.github/workflows/library_examples.yml

@@ -51,8 +51,16 @@ jobs:
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
           make build_java CORES=$CORES
+          make mvn_local_deploy
 
       - name: Test AwsCryptographicMaterialProviders Java Examples
-        working-directory: ./AwsCryptographicMaterialProviders
+        working-directory: ./Examples
         run: |
-          make test_example_java
+          make test_java
+
+      # These tests are "flacky" and not really neccessary,
+      # we created them in re-action to a user error with local caches and DDB
+      # - name: Test AwsCryptographicMaterialProviders Java Concurrent
+      #   working-directory: ./Examples
+      #   run: |
+      #     make test_java_concurrent

.github/workflows/library_interop_tests.yml

@@ -19,7 +19,8 @@ jobs:
     strategy:
       matrix:
         library: [TestVectorsAwsCryptographicMaterialProviders]
-        os: [
+        os:
+          [
             # https://taskei.amazon.dev/tasks/CrypTool-5283
             # windows-latest,
             ubuntu-22.04,

.github/workflows/manual.yml

@@ -37,21 +37,23 @@ jobs:
     with:
       dafny: ${{ inputs.dafny }}
       regenerate-code: ${{ inputs.regenerate-code }}
-  manual-ci-rust:
-    uses: ./.github/workflows/library_rust_tests.yml
-    with:
-      dafny: ${{ inputs.dafny }}
-      regenerate-code: ${{ inputs.regenerate-code }}
+  # TODO-HV-2-Rust: Removing Rust Runtimes until the underlying issue resolved.
+  #  manual-ci-rust:
+  #    uses: ./.github/workflows/library_rust_tests.yml
+  #    with:
+  #      dafny: ${{ inputs.dafny }}
+  #      regenerate-code: ${{ inputs.regenerate-code }}
   manual-ci-python:
     uses: ./.github/workflows/library_python_tests.yml
     with:
       dafny: ${{ inputs.dafny }}
       regenerate-code: ${{ inputs.regenerate-code }}
-  manual-ci-go:
-    uses: ./.github/workflows/library_go_tests.yml
-    with:
-      dafny: ${{ inputs.dafny }}
-      regenerate-code: ${{ inputs.regenerate-code }}
+  # TODO-HV-2-Go: Removing Go CI until we rebase or need it
+  # manual-ci-go:
+  #   uses: ./.github/workflows/library_go_tests.yml
+  #   with:
+  #     dafny: ${{ inputs.dafny }}
+  #     regenerate-code: ${{ inputs.regenerate-code }}
   manual-interop-test:
     uses: ./.github/workflows/library_interop_tests.yml
     with:

.github/workflows/pull.yml

@@ -39,16 +39,19 @@ jobs:
     uses: ./.github/workflows/library_net_tests.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  # TODO-HV-2-Rust: Removing Rust until we rebase or need it
   # pr-ci-rust:
   #   needs: getVersion
   #   uses: ./.github/workflows/library_rust_tests.yml
   #   with:
   #     dafny: ${{needs.getVersion.outputs.version}}
-  pr-ci-python:
-    needs: getVersion
-    uses: ./.github/workflows/library_python_tests.yml
-    with:
-      dafny: ${{needs.getVersion.outputs.version}}
+  # TODO-HV-2-Python: Removing Python until we fix bugs in Dafny/Python transpilation
+  # pr-ci-python:
+  #   needs: getVersion
+  #   uses: ./.github/workflows/library_python_tests.yml
+  #   with:
+  #     dafny: ${{needs.getVersion.outputs.version}}
+  # TODO-HV-2-Go: Removing Go CI until we rebase or need it
   # pr-ci-go:
   #   needs: getVersion
   #   uses: ./.github/workflows/library_go_tests.yml
@@ -70,12 +73,15 @@ jobs:
       - pr-ci-verification
       - pr-ci-java
       - pr-ci-net
-      - pr-ci-python
+      # TODO-HV-2-Python: Removing Python until we fix bugs in Dafny/Python transpilation
+      # - pr-ci-python
+      # TODO-HV-2-Go: Removing Go CI until we rebase or need it
       # - pr-ci-go
+      # TODO-HV-2-Rust: Removing Rust until we rebase or need it
       # - pr-ci-rust
       - pr-interop-test
       - pr-ci-examples
-    runs-on: ubuntu--22.04
+    runs-on: ubuntu-22.04
     steps:
       - name: Verify all required jobs passed
         uses: re-actors/alls-green@release/v1

.github/workflows/push.yml

@@ -36,6 +36,7 @@ jobs:
     uses: ./.github/workflows/library_net_tests.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  # TODO-HV-2-Rust: Removing Rust until we rebase or need it.
   # push-ci-rust:
   #   needs: getVersion
   #   uses: ./.github/workflows/library_rust_tests.yml
@@ -46,6 +47,7 @@ jobs:
     uses: ./.github/workflows/library_python_tests.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  # TODO-HV-2-Go: Removing Go CI until we rebase or need it
   # push-ci-go:
   #   needs: getVersion
   #   uses: ./.github/workflows/library_go_tests.yml

AwsCryptographicMaterialProviders/Makefile

@@ -170,6 +170,3 @@ PYTHON_DEPENDENCY_MODULE_NAMES := \
 	--dependency-library-name=aws.cryptography.materialProviders=aws_cryptographic_material_providers \
 	--dependency-library-name=aws.cryptography.keyStore=aws_cryptographic_material_providers \
 	--dependency-library-name=aws.cryptography.keyStoreAdmin=aws_cryptographic_material_providers \
-
-test_example_java:
-	$(GRADLEW) -p runtimes/java cleanTestExamples testExamples

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CanonicalEncryptionContext.dfy

@@ -63,29 +63,75 @@ module CanonicalEncryptionContext {
     else Failure(Types.AwsCryptographicMaterialProvidersException( message := "Unable to serialize encryption context"))
   }
 
+  // @texastony had a dream of using this predicates to
+  // remove duplicate code in HVUtils
+  // and CreateKeyHV2.dfy but has given up on the dream for now.
+  // TODO-HV-2-FOLLOW : Complete Dream or Kill this
+  // predicate digestSHA384ContextPostConditions(
+  //   nameonly content: seq<uint8>,
+  //   nameonly digest: seq<uint8>,
+  //   nameonly digestEvent: AtomicPrimitives.Types.DafnyCallEvent<AtomicPrimitives.Types.DigestInput, Result<seq<uint8>, AtomicPrimitives.Types.Error>>
+  // )
+  // {
+  //   var input := digestEvent.input;
+  //   var output := digestEvent.output;
+  //   && input.digestAlgorithm == AtomicPrimitives.Types.SHA_384
+  //   && input.message == content
+  //   && output.Success?
+  //   ==>
+  //     && |output.value| == 48 // 384 bits / 8 bits per byte == 48 bytes
+  //     && output.value == digest
+  // }
+
+  // twostate predicate encryptionContextDigestPostConditions(
+  //   crypto: AtomicPrimitives.AtomicPrimitivesClient,
+  //   encryptionContext: Types.EncryptionContext,
+  //   digest: seq<uint8>
+  // )
+  //   reads crypto.History
+  // {
+  //   && var content? := EncryptionContextToAAD(encryptionContext);
+  //   && content?.Success?
+  //   && |crypto.History.Digest| == |old(crypto.History.Digest)| + 1
+  //   && var digestEvent := Seq.Last(crypto.History.Digest);
+  //   && digestSHA384ContextPostConditions(
+  //     content := content?.value,
+  //     digest := digest,
+  //     digestEvent := digestEvent)
+  // }
+
   method EncryptionContextDigest(
-    Crypto: AtomicPrimitives.AtomicPrimitivesClient,
+    crypto: AtomicPrimitives.AtomicPrimitivesClient,
     encryptionContext: Types.EncryptionContext
   )
     returns (output: Result<seq<uint8>, CanonizeDigestError>)
-    requires Crypto.ValidState()
-    modifies Crypto.Modifies
-    ensures Crypto.ValidState()
-    ensures output.Success? ==>
-              && 0 < |Crypto.History.Digest|
-              && Seq.Last(Crypto.History.Digest).output.Success?
-              && var DigestInput := Seq.Last(Crypto.History.Digest).input;
-              && var DigestOutput := Seq.Last(Crypto.History.Digest).output;
-              && DigestInput.digestAlgorithm == AtomicPrimitives.Types.SHA_384
-              && DigestOutput.value == output.value
+    requires crypto.ValidState()
+    modifies crypto.Modifies
+    ensures crypto.ValidState()
+    // We tried to collapse all of this post condition into a common predicate.
+    // We failed; we will have to copy and paste it.
+    // @texastony thinks reason is that is very difficult to keep track of the input.
+    ensures
+      && output.Success?
+      ==>
+        && var content? := EncryptionContextToAAD(encryptionContext);
+        && content?.Success?
+        && |crypto.History.Digest| == |old(crypto.History.Digest)| + 1
+        && old(crypto.History.Digest) < crypto.History.Digest
+        && var digestEvent := Seq.Last(crypto.History.Digest);
+        && digestEvent.input.digestAlgorithm == AtomicPrimitives.Types.SHA_384
+        && digestEvent.input.message == content?.value
+        && digestEvent.output.Success?
+        && |digestEvent.output.value| == 48 // 384 bits / 8 bits per byte == 48 bytes
+        && digestEvent.output.value == output.value
   {
     var canonicalEC :- EncryptionContextToAAD(encryptionContext);
 
     var DigestInput := AtomicPrimitives.Types.DigestInput(
       digestAlgorithm := AtomicPrimitives.Types.SHA_384,
       message := canonicalEC
     );
-    var maybeDigest := Crypto.Digest(DigestInput);
+    var maybeDigest := crypto.Digest(DigestInput);
     var digest :- maybeDigest.MapFailure(e => Types.AwsCryptographyPrimitives(e));
 
     // The digest is not truncated.

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy

@@ -518,6 +518,8 @@ module AwsKmsKeyring {
             ));
       }
 
+      AnEdkExistsLemma(edksToAttempt);
+
       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
       //# For each encrypted data key in the filtered set, one at a time, the
       //# OnDecrypt MUST attempt to decrypt the data key.
@@ -548,13 +550,28 @@ module AwsKmsKeyring {
                       list := errors,
                       message := "No Configured KMS Key was able to decrypt the Data Key. The list of encountered Exceptions is available via `list`."));
 
+      assert exists edk | edk in edksToAttempt
+          ::
+            && var maybeWrappedMaterial :=
+              EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, input.materials.algorithmSuite);
+            && maybeWrappedMaterial.Success?
+            && KMS.IsValid_CiphertextType(maybeWrappedMaterial.value);
+
       assert decryptClosure.Ensures(Last(attempts).input, Success(SealedDecryptionMaterials), DropLast(attempts));
       return Success(Types.OnDecryptOutput(
                        materials := SealedDecryptionMaterials
                      ));
     }
   }
 
+  lemma AnEdkExistsLemma(edksToAttempt: seq<Types.EncryptedDataKey>)
+    requires |edksToAttempt| > 0
+    ensures exists edk | edk in edksToAttempt :: true
+  {
+    var edk := edksToAttempt[0];
+    assert edk in edksToAttempt;
+  }
+
   class OnDecryptEncryptedDataKeyFilter
     extends DeterministicActionWithResult<Types.EncryptedDataKey, bool, Types.Error>
   {
@@ -571,8 +588,8 @@ module AwsKmsKeyring {
       && (
         && res.Success?
         && res.value
-        ==>
-          edk.keyProviderId == PROVIDER_ID)
+        ==> exists edk' | edk' == edk
+            :: edk'.keyProviderId == PROVIDER_ID)
     }
 
     method Invoke(edk: Types.EncryptedDataKey)

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy

@@ -2,13 +2,15 @@
 // SPDX-License-Identifier: Apache-2.0
 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
 include "../../../../StandardLibrary/src/Index.dfy"
+include "../../../../AwsCryptographyPrimitives/src/Index.dfy"
 include "../../../../ComAmazonawsDynamodb/src/Index.dfy"
 include "../../../../ComAmazonawsKms/src/Index.dfy"
 module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } AwsCryptographyKeyStoreTypes
 {
   import opened Wrappers
   import opened StandardLibrary.UInt
   import opened UTF8
+  import AwsCryptographyPrimitivesTypes
   import ComAmazonawsDynamodbTypes
   import ComAmazonawsKmsTypes
     // Generic helpers for verification of mock/unit tests.
@@ -151,6 +153,9 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
   datatype HierarchicalSymmetric = | HierarchicalSymmetric (
     nameonly Version: string
   )
+  datatype HierarchyVersion =
+    | v1
+    | v2
   type HmacKeyMap = map<string, Secret>
   datatype KeyManagement =
     | kms(kms: AwsKms)
@@ -924,6 +929,9 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
     | BranchKeyCiphertextException (
         nameonly message: string
       )
+    | HierarchyVersionException (
+        nameonly message: string
+      )
     | KeyManagementException (
         nameonly message: string
       )
@@ -946,6 +954,7 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
         nameonly message: string
       )
       // Any dependent models are listed here
+    | AwsCryptographyPrimitives(AwsCryptographyPrimitives: AwsCryptographyPrimitivesTypes.Error)
     | ComAmazonawsDynamodb(ComAmazonawsDynamodb: ComAmazonawsDynamodbTypes.Error)
     | ComAmazonawsKms(ComAmazonawsKms: ComAmazonawsKmsTypes.Error)
       // The Collection error is used to collect several errors together