Skip to content

feat(KSA): KMS Decrypt/Encrypt Strategy #1020

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 10 commits into from
Nov 25, 2024
Merged

feat(KSA): KMS Decrypt/Encrypt Strategy #1020

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
1334093
chore: add decrypt/encrypt to key store admin model
josecorella Nov 15, 2024
312419c
regenerate code with model updates
josecorella Nov 15, 2024
8e1cdd6
work on initialize mutation
josecorella Nov 18, 2024
7dae9c8
finish initialize mutation
josecorella Nov 19, 2024
a36be9e
start decrypt/encrypt initialize test
josecorella Nov 20, 2024
829fa26
work on apply
josecorella Nov 20, 2024
5fc154c
more progress on apply
josecorella Nov 21, 2024
f8f912b
finish refactoring apply mutation to handle both reencrypt and decryp…
josecorella Nov 22, 2024
0675cba
implement kms operation decrypt/encrypt
josecorella Nov 22, 2024
a1800b5
test happy case roundtrip
josecorella Nov 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
223 changes: 214 additions & 9 deletions ...ryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -291,6 +291,211 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
return Success(reEncryptResponse);
}

method VerifyViaDecryptEncryptKey(
ciphertext: seq<uint8>,
sourceEncryptionContext: Structure.BranchKeyContext,
destinationEncryptionContext: Structure.BranchKeyContext,
kmsConfiguration: Types.KMSConfiguration,
decryptGrantTokens: KMS.GrantTokenList,
decryptKmsClient: KMS.IKMSClient
)
Comment on lines +294 to +301
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggestion: A little bit of source comments may help those without context.
These will also help us write the Spec.

Suggested change
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
)

returns (res: Result<KMS.EncryptResponse, KmsError>)
requires
&& Structure.BranchKeyContext?(sourceEncryptionContext)
&& Structure.BranchKeyContext?(destinationEncryptionContext)
requires AttemptReEncrypt?(sourceEncryptionContext, destinationEncryptionContext)
requires AttemptKmsOperation?(kmsConfiguration, destinationEncryptionContext)
requires HasKeyId(kmsConfiguration) && KmsArn.ValidKmsArn?(GetKeyId(kmsConfiguration))
requires decryptKmsClient.ValidState()
modifies decryptKmsClient.Modifies
ensures decryptKmsClient.ValidState()

ensures
res.Success?
==>
// Proof for success when we decrypt
&& KMS.IsValid_CiphertextType(ciphertext)
&& |decryptKmsClient.History.Decrypt| == |old(decryptKmsClient.History.Decrypt)| + 1
&& |decryptKmsClient.History.Encrypt| == |old(decryptKmsClient.History.Encrypt)| + 1
&& var decryptInput := Seq.Last(decryptKmsClient.History.Decrypt).input;
&& var decryptResponse := Seq.Last(decryptKmsClient.History.Decrypt).output;
&& var kmsKeyArn := GetKeyId(kmsConfiguration);
&& KMS.DecryptRequest(
CiphertextBlob := ciphertext,
EncryptionContext := Some(sourceEncryptionContext),
GrantTokens := Some(decryptGrantTokens),
KeyId := Some(kmsKeyArn)
) == decryptInput
&& var decryptResponse := Seq.Last(decryptKmsClient.History.Decrypt).output;
&& decryptResponse.Success? && decryptResponse.value.Plaintext.Some?
&& old(decryptKmsClient.History.Decrypt) < decryptKmsClient.History.Decrypt
// Proof for success when we encrypt
&& var encryptInput := Seq.Last(decryptKmsClient.History.Encrypt).input;
&& var encryptResponse := Seq.Last(decryptKmsClient.History.Encrypt).output;
&& KMS.EncryptRequest(
KeyId := kmsKeyArn,
Plaintext := decryptResponse.value.Plaintext.value,
EncryptionContext := Some(destinationEncryptionContext),
GrantTokens := Some(decryptGrantTokens)
) == encryptInput
&& old(decryptKmsClient.History.Encrypt) < decryptKmsClient.History.Encrypt
&& res.value.CiphertextBlob.Some?
&& res.value.KeyId.Some?
&& res.value.KeyId.value == kmsKeyArn
&& KMS.IsValid_CiphertextType(res.value.CiphertextBlob.value)
&& encryptResponse.Success?
&& encryptResponse.value == res.value
{
:- Need(
KMS.IsValid_CiphertextType(ciphertext),
Types.KeyManagementException(
message := "Invalid KMS ciphertext.")
);

var kmsKeyArn := GetKeyId(kmsConfiguration);
var kmsDecryptRequest := KMS.DecryptRequest(
CiphertextBlob := ciphertext,
EncryptionContext := Some(sourceEncryptionContext),
GrantTokens := Some(decryptGrantTokens),
KeyId := Some(kmsKeyArn)
);

var decryptResponse? := decryptKmsClient.Decrypt(kmsDecryptRequest);
var decryptResponse :- decryptResponse?
.MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));

:- Need(
&& decryptResponse.Plaintext.Some?
&& decryptResponse.KeyId.Some?
&& decryptResponse.KeyId.value == kmsKeyArn,
Types.KeyManagementException(
message := "Invalid response from AWS KMS Decrypt :: Invalid KMS Key Id"
));

var kmsEncryptRequest := KMS.EncryptRequest(
KeyId := kmsKeyArn,
Plaintext := decryptResponse.Plaintext.value,
EncryptionContext := Some(destinationEncryptionContext),
GrantTokens := Some(decryptGrantTokens)
);

var encryptResponse? := decryptKmsClient.Encrypt(kmsEncryptRequest);
var encryptResponse :- encryptResponse?
.MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));

:- Need(
&& encryptResponse.CiphertextBlob.Some?
&& KMS.IsValid_CiphertextType(encryptResponse.CiphertextBlob.value)
&& encryptResponse.KeyId.Some?
&& encryptResponse.KeyId.value == kmsKeyArn,
Types.KeyManagementException(
message := "Invalid response from AWS KMS Encrypt :: Invalid KMS Key Id"
));

return Success(encryptResponse);
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

}

method MutateViaDecryptEncrypt(
ciphertext: seq<uint8>,
sourceEncryptionContext: Structure.BranchKeyContext,
destinationEncryptionContext: Structure.BranchKeyContext,
sourceKmsArn: string,
destinationKmsArn: string,
decryptGrantTokens: KMS.GrantTokenList,
decryptKmsClient: KMS.IKMSClient,
encryptGrantTokens: KMS.GrantTokenList,
encryptKmsClient: KMS.IKMSClient
)
returns (res: Result<KMS.CiphertextType, KmsError>)
requires
&& Structure.BranchKeyContext?(sourceEncryptionContext)
&& Structure.BranchKeyContext?(destinationEncryptionContext)
requires AttemptReEncrypt?(sourceEncryptionContext, destinationEncryptionContext)
requires KmsArn.ValidKmsArn?(sourceKmsArn) && KmsArn.ValidKmsArn?(destinationKmsArn)
requires decryptKmsClient.Modifies !! encryptKmsClient.Modifies
requires decryptKmsClient.ValidState() && encryptKmsClient.ValidState()
modifies decryptKmsClient.Modifies + encryptKmsClient.Modifies
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Suggested change
modifies decryptKmsClient.Modifies + encryptKmsClient.Modifies
modifies decryptKmsClient.Modifies, encryptKmsClient.Modifies

ensures decryptKmsClient.ValidState() && encryptKmsClient.ValidState()
ensures
res.Success?
==>
&& KMS.IsValid_CiphertextType(ciphertext)
&& |decryptKmsClient.History.Decrypt| == |old(decryptKmsClient.History.Decrypt)| + 1
&& var decryptInput := Seq.Last(decryptKmsClient.History.Decrypt).input;
&& var decryptOutput := Seq.Last(decryptKmsClient.History.Decrypt).output;
&& KMS.DecryptRequest(
CiphertextBlob := ciphertext,
EncryptionContext := Some(sourceEncryptionContext),
GrantTokens := Some(decryptGrantTokens),
KeyId := Some(sourceKmsArn)
) == decryptInput
&& decryptOutput.Success? && decryptOutput.value.Plaintext.Some? && decryptOutput.value.KeyId.Some?
&& decryptOutput.value.KeyId.value == sourceKmsArn
&& |encryptKmsClient.History.Encrypt| == |old(encryptKmsClient.History.Encrypt)| + 1
&& var encryptInput := Seq.Last(encryptKmsClient.History.Encrypt).input;
&& var encryptResponse := Seq.Last(encryptKmsClient.History.Encrypt).output;
&& KMS.EncryptRequest(
KeyId := destinationKmsArn,
Plaintext := decryptOutput.value.Plaintext.value,
EncryptionContext := Some(destinationEncryptionContext),
GrantTokens := Some(encryptGrantTokens)
) == encryptInput
&& old(encryptKmsClient.History.Encrypt) < encryptKmsClient.History.Encrypt
&& encryptResponse.Success?
&& encryptResponse.value.CiphertextBlob.Some?
&& encryptResponse.value.KeyId.Some?
&& encryptResponse.value.KeyId.value == destinationKmsArn // kmsKeyArn
&& KMS.IsValid_CiphertextType(encryptResponse.value.CiphertextBlob.value)
&& encryptResponse.value.CiphertextBlob.value == res.value
{
:- Need(
KMS.IsValid_CiphertextType(ciphertext),
Types.KeyManagementException(
message := "Invalid KMS ciphertext.")
);

var kmsDecryptRequest := KMS.DecryptRequest(
CiphertextBlob := ciphertext,
EncryptionContext := Some(sourceEncryptionContext),
GrantTokens := Some(decryptGrantTokens),
KeyId := Some(sourceKmsArn)
);

var decryptResponse? := decryptKmsClient.Decrypt(kmsDecryptRequest);
var decryptResponse :- decryptResponse?
.MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));

:- Need(
&& decryptResponse.Plaintext.Some?
&& decryptResponse.KeyId.Some?
&& decryptResponse.KeyId.value == sourceKmsArn,
Types.KeyManagementException(
message := "Invalid response from AWS KMS Decrypt :: Invalid KMS Key Id"
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit/non-blocking: this error message is not quite accurate,
since the plaintext could be invalid.

I am not sure this matters at all.

));

var kmsEncryptRequest := KMS.EncryptRequest(
KeyId := destinationKmsArn,
Plaintext := decryptResponse.Plaintext.value,
EncryptionContext := Some(destinationEncryptionContext),
GrantTokens := Some(encryptGrantTokens)
);

var encryptResponse? := encryptKmsClient.Encrypt(kmsEncryptRequest);
var encryptResponse :- encryptResponse?
.MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));

:- Need(
&& encryptResponse.CiphertextBlob.Some?
&& KMS.IsValid_CiphertextType(encryptResponse.CiphertextBlob.value)
&& encryptResponse.KeyId.Some?
&& encryptResponse.KeyId.value == destinationKmsArn,
Types.KeyManagementException(
message := "Invalid response from AWS KMS Encrypt :: Invalid KMS Key Id"
));

return Success(encryptResponse.CiphertextBlob.value);
}

method MutateViaReEncrypt(
ciphertext: seq<uint8>,
sourceEncryptionContext: Structure.BranchKeyContext,
Expand All @@ -300,7 +505,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
grantTokens: KMS.GrantTokenList,
kmsClient: KMS.IKMSClient
)
returns (res: Result<KMS.ReEncryptResponse, KmsError>)
returns (res: Result<KMS.CiphertextType, KmsError>)
requires
&& Structure.BranchKeyContext?(sourceEncryptionContext)
&& Structure.BranchKeyContext?(destinationEncryptionContext)
Expand Down Expand Up @@ -337,15 +542,15 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
ensures
res.Success? ==>
// && var kmsKeyArn := GetKeyId(kmsConfiguration);
&& res.value.CiphertextBlob.Some?
&& res.value.SourceKeyId.Some?
&& res.value.KeyId.Some?
&& res.value.SourceKeyId.value == sourceKmsArn //kmsKeyArn
&& res.value.KeyId.value == destinationKmsArn // kmsKeyArn
&& KMS.IsValid_CiphertextType(res.value.CiphertextBlob.value)
&& var kmsOperationOutput := Seq.Last(kmsClient.History.ReEncrypt).output;
&& kmsOperationOutput.Success?
&& kmsOperationOutput.value == res.value
&& kmsOperationOutput.value.CiphertextBlob.Some?
&& kmsOperationOutput.value.SourceKeyId.Some?
&& kmsOperationOutput.value.KeyId.Some?
&& kmsOperationOutput.value.SourceKeyId.value == sourceKmsArn //kmsKeyArn
&& kmsOperationOutput.value.KeyId.value == destinationKmsArn // kmsKeyArn
&& KMS.IsValid_CiphertextType(kmsOperationOutput.value.CiphertextBlob.value)
&& kmsOperationOutput.value.CiphertextBlob.value == res.value
{
:- Need(
KMS.IsValid_CiphertextType(ciphertext),
Expand Down Expand Up @@ -389,7 +594,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
message := "Invalid response from AWS KMS ReEncrypt: Invalid ciphertext.")
);

return Success(reEncryptResponse);
return Success(reEncryptResponse.CiphertextBlob.value);
}

method DecryptKey(
Expand Down
2 changes: 1 addition & 1 deletion AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -665,7 +665,7 @@ module {:options "/functionSyntax:4" } Structure {
ensures BRANCH_KEY_FIELD !in key.EncryptionContext
{}

lemma EncryptionContextConstructorsAreCorrect(
lemma {:vcs_split_on_every_assert} EncryptionContextConstructorsAreCorrect(
branchKeyId: string,
branchKeyVersion: string,
timestamp: string,
Expand Down
5 changes: 5 additions & 0 deletions ...lProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,10 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
datatype ApplyMutationResult =
| ContinueMutation(ContinueMutation: MutationToken)
| CompleteMutation(CompleteMutation: MutationComplete)
datatype AwsKmsDecryptEncrypt = | AwsKmsDecryptEncrypt (
nameonly decrypt: Option<AwsCryptographyKeyStoreTypes.AwsKms> := Option.None ,
nameonly encrypt: Option<AwsCryptographyKeyStoreTypes.AwsKms> := Option.None
)
datatype CreateKeyInput = | CreateKeyInput (
nameonly Identifier: Option<string> := Option.None ,
nameonly EncryptionContext: Option<AwsCryptographyKeyStoreTypes.EncryptionContext> := Option.None ,
Expand Down Expand Up @@ -64,6 +68,7 @@ module {:extern "software.amazon.cryptography.keystoreadmin.internaldafny.types"
)
datatype KeyManagementStrategy =
| AwsKmsReEncrypt(AwsKmsReEncrypt: AwsCryptographyKeyStoreTypes.AwsKms)
| AwsKmsDecryptEncrypt(AwsKmsDecryptEncrypt: AwsKmsDecryptEncrypt)
class IKeyStoreAdminClientCallHistory {
ghost constructor() {
CreateKey := [];
Expand Down
44 changes: 20 additions & 24 deletions ...ptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/Model/KeyStoreAdmin.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,16 +140,14 @@ union SystemKey {
trustStorage: TrustStorage
}

// TODO-Mutations-FF :
// For GA of Mutations, of Mutations, only ReEncrypt is allowed
// structure AwsKmsDecryptEncrypt {
// @documentation("The KMS Client (and Grant Tokens) used to Decrypt Branch Key Store Items.")
// decrypt: aws.cryptography.keyStore#AwsKms
// @documentation(
// "The KMS Client (and Grant Tokens) used to Encrypt Branch Key Store Items
// and to Generate new Cryptographic Material.")
// encrypt: aws.cryptography.keyStore#AwsKms
// }
structure AwsKmsDecryptEncrypt {
@documentation("The KMS Client (and Grant Tokens) used to Decrypt Branch Key Store Items.")
decrypt: aws.cryptography.keyStore#AwsKms
@documentation(
"The KMS Client (and Grant Tokens) used to Encrypt Branch Key Store Items
and to Generate new Cryptographic Material.")
encrypt: aws.cryptography.keyStore#AwsKms
}

@documentation(
"This configures which Key Management Operations will be used
Expand All @@ -160,20 +158,18 @@ union KeyManagementStrategy {
executed with the provided Grant Tokens and KMS Client.
This is one request to Key Management, as compared to two.
But only one set of credentials can be used.")
AwsKmsReEncrypt: aws.cryptography.keyStore#AwsKms
// TODO-Mutations-FF :
// For GA of Mutations, only ReEncrypt is allowed
// @documentation(
// "Key Store Items are authenticated and re-wrapped via a Decrypt and then Encrypt request.
// This is two separate requests to Key Management, as compared to one.
// But the Decrypt requests will use the Decrypt KMS Client (and Grant Tokens),
// while the Encrypt requests will use the Encrypt KMS Client (and Grant Tokens).
// This option affords for different credentials to be utilized,
// based on the operation.
// When Generating new material,
// KMS GenerateDataKeyWithoutPlaintext will be executed against
// the Encrypt option.")
// AwsKmsDecryptEncrypt: AwsKmsDecryptEncrypt
AwsKmsReEncrypt: aws.cryptography.keyStore#AwsKms,
@documentation(
"Key Store Items are authenticated and re-wrapped via a Decrypt and then Encrypt request.
This is two separate requests to Key Management, as compared to one.
But the Decrypt requests will use the Decrypt KMS Client (and Grant Tokens),
while the Encrypt requests will use the Encrypt KMS Client (and Grant Tokens).
This option affords for different credentials to be utilized,
based on the operation.
When Generating new material,
KMS GenerateDataKeyWithoutPlaintext will be executed against
the Encrypt option.")
Comment on lines +163 to +171
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TODO: In the documentation,
detail that during Initialize Mutation,
the active item is validated with the Decrypt Client.

During Apply Mutation,
terminal items are validated with encrypt client.

AwsKmsDecryptEncrypt: AwsKmsDecryptEncrypt
}


Expand Down
Loading
Loading