feat(KSA): KMS Decrypt/Encrypt Strategy #1020
Conversation
|
Detected changes to the release files or to the check-files action |
|
Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS |
texastony
changed the title
|
Detected changes to the release files or to the check-files action |
|
Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS |
|
Detected changes to the release files or to the check-files action |
|
Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS |
|
Detected changes to the release files or to the check-files action |
|
Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS |
texastony
force-pushed
the
mutations/mutations
branch
3 times, most recently
from
d972522 to
8dc3711
Compare
josecorella
force-pushed
the
mutations/decrypt-encrypt-strat
branch
2 times, most recently
from
36fbc86 to
bd60751
Compare
|
Detected changes to the release files or to the check-files action |
|
Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS |
texastony
force-pushed
the
mutations/mutations
branch
from
8dc3711 to
266bf70
Compare
texastony
force-pushed
the
mutations/decrypt-encrypt-strat
branch
from
cddc657 to
a1800b5
Compare
|
Detected changes to the release files or to the check-files action |
|
Changes to the release files or the check-files action requires 2 approvals from CODEOWNERS |
| method VerifyViaDecryptEncryptKey( | ||
| ciphertext: seq<uint8>, | ||
| sourceEncryptionContext: Structure.BranchKeyContext, | ||
| destinationEncryptionContext: Structure.BranchKeyContext, | ||
| kmsConfiguration: Types.KMSConfiguration, | ||
| decryptGrantTokens: KMS.GrantTokenList, | ||
| decryptKmsClient: KMS.IKMSClient | ||
| ) |
There was a problem hiding this comment.
Suggestion: A little bit of source comments may help those without context.
These will also help us write the Spec.
| method VerifyViaDecryptEncryptKey( | |
| ciphertext: seq<uint8>, | |
| sourceEncryptionContext: Structure.BranchKeyContext, | |
| destinationEncryptionContext: Structure.BranchKeyContext, | |
| kmsConfiguration: Types.KMSConfiguration, | |
| decryptGrantTokens: KMS.GrantTokenList, | |
| decryptKmsClient: KMS.IKMSClient | |
| ) | |
| /* Decrypt is assumed to be the "source", or "original", client. | |
| The Decrypt KMS Client is used for both a Decrypt and Encrypt call. | |
| */ | |
| method VerifyViaDecryptEncryptKey( | |
| ciphertext: seq<uint8>, | |
| sourceEncryptionContext: Structure.BranchKeyContext, | |
| destinationEncryptionContext: Structure.BranchKeyContext, | |
| kmsConfiguration: Types.KMSConfiguration, | |
| decryptGrantTokens: KMS.GrantTokenList, | |
| decryptKmsClient: KMS.IKMSClient | |
| ) |
AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy
Show resolved
Hide resolved
| message := "Invalid response from AWS KMS Encrypt :: Invalid KMS Key Id" | ||
| )); | ||
|
|
||
| return Success(encryptResponse); |
There was a problem hiding this comment.
TODO: Based on the error cases I have seen,
we will need to map these errors, in Mutations,
we will need to map these errors to the following failures:
- Opaque KMS that matches Decrypt or Encrypt => MutationFromException
- KMS InvalidCiphertextException => We need to create a new exception for broken branch keys...
- All other exceptions => KeyStoreAdminException for un-expected errors
The ReEncrypt strategy probably also needs these error refinements.
I focused my error refinements on the critical case of KMS Access Denied.
But InvalidCiphertext is a separate issue.
| requires KmsArn.ValidKmsArn?(sourceKmsArn) && KmsArn.ValidKmsArn?(destinationKmsArn) | ||
| requires decryptKmsClient.Modifies !! encryptKmsClient.Modifies | ||
| requires decryptKmsClient.ValidState() && encryptKmsClient.ValidState() | ||
| modifies decryptKmsClient.Modifies + encryptKmsClient.Modifies |
There was a problem hiding this comment.
Suggestion: I have a thesis, that is probably wrong,
but that using , instead of concatenation (+) creates a multiset instead of a union of two sets.
I need to look into more thesis more,
but , has resolved some of my problems.
| modifies decryptKmsClient.Modifies + encryptKmsClient.Modifies | |
| modifies decryptKmsClient.Modifies, encryptKmsClient.Modifies |
| && decryptResponse.KeyId.Some? | ||
| && decryptResponse.KeyId.value == sourceKmsArn, | ||
| Types.KeyManagementException( | ||
| message := "Invalid response from AWS KMS Decrypt :: Invalid KMS Key Id" |
There was a problem hiding this comment.
Nit/non-blocking: this error message is not quite accurate,
since the plaintext could be invalid.
I am not sure this matters at all.
| function ValidateCommitmentAndIndexStructures( | ||
| input: Types.ApplyMutationInput, | ||
| fetchMutation: KeyStoreTypes.GetMutationOutput, | ||
| commitment: KeyStoreTypes.MutationCommitment, | ||
| index: KeyStoreTypes.MutationIndex | ||
| ): (output: Result<(), Types.Error>) |
There was a problem hiding this comment.
Note: I also refactored this method.
I removed the fetch type entirely,
along with some other changes to facilitate System Key verification.
| requires forall item <- items :: item.item.Type.HierarchicalSymmetricVersion? | ||
| requires forall item <- items :: KmsArn.ValidKmsArn?(item.item.KmsArn) | ||
| requires forall item <- items :: Structure.EncryptedHierarchicalKey?(item.item) | ||
| requires forall item <- items :: item.itemOriginal? ==> item.item.KmsArn == mutationToApply.Original.kmsArn |
There was a problem hiding this comment.
Note: it really fascinates me that we need to prove the original condition's KMS ARN,
but not the terminal condition's,
nor do we need to make any statements on the Encryption Context...
| // We have initialized the mutation. Instead of continuing with the Decrypt/Encrypt Strategy we will | ||
| // go to the ReEncrypt strategy bc as of today (11-20-2023) Decrypt/Encrypt Strategy is not supported for | ||
| // Apply Mutation. |
There was a problem hiding this comment.
Issue: This is no longer true, correct? This is the only comment so far that MUST be addressed.
Resolved by test below.
Still, we should remove this comment.
| // We have initialized the mutation. Instead of continuing with the Decrypt/Encrypt Strategy we will | ||
| // go to the ReEncrypt strategy bc as of today (11-20-2023) Decrypt/Encrypt Strategy is not supported for | ||
| // Apply Mutation. |
There was a problem hiding this comment.
Oh good. I know this is no longer true because this test literally proves this.
| // -- All items have been mutated | ||
|
|
||
|
|
||
| module {:options "/functionSyntax:4" } TestDecryptEncryptStrat { |
There was a problem hiding this comment.
TODO: Between @texastony and @josecorella , we should do a major refactor of the Mutation testing.
There is a ton of duplicate code that could be consolidated to:
- Start Mutation
- Verify Start
- Work Mutation
- Verify Work
- Complete Mutation
- Verify Complete
- Clean Up everything
Or something along those lines.
|
@texastony and @texastony, I noticed you are updating the smithy model files. |
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Co-authored-by: Jose Corella <[email protected]>
Issue #, if available:
Description of changes:
Closes #1013
Squash/merge commit message, if applicable:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.