Skip to content

Commit 0c5cfa7

Browse files
texastonytexastony
authored
fix(KeyStoreAdmin): Exceptions for Mutations when KMS Key is Disabled (#1235)
This addresses KMS Exceptions when the KMS Key is disabled OR when the caller does not have permission to call GenerateDataKeyWithoutPlaintext on the terminal KMS Key.
1 parent eb56365 commit 0c5cfa7

File tree

5 files changed

+267
-141
lines changed

5 files changed

+267
-141
lines changed

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/KMSKeystoreOperations.dfy

+10-111
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
102102
grantTokens: KMS.GrantTokenList,
103103
kmsClient: KMS.IKMSClient
104104
)
105-
returns (res: Result<KMS.GenerateDataKeyWithoutPlaintextResponse, Types.Error>)
105+
returns (res: Result<KMS.GenerateDataKeyWithoutPlaintextResponse, KmsError>)
106106
requires kmsClient.ValidState()
107107
requires HasKeyId(kmsConfiguration) && KmsArn.ValidKmsArn?(GetKeyId(kmsConfiguration))
108108
requires AttemptKmsOperation?(kmsConfiguration, encryptionContext)
@@ -145,14 +145,14 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
145145

146146
:- Need(
147147
&& generateResponse.KeyId.Some?,
148-
Types.KeyStoreException(
149-
message := "Invalid response from KMS GenerateDataKey:: Invalid Key Id")
148+
Types.KeyManagementException(
149+
message := "Invalid response from AWS KMS GenerateDataKey: Invalid Key Id")
150150
);
151151

152152
:- Need(
153153
&& generateResponse.CiphertextBlob.Some?
154154
&& KMS.IsValid_CiphertextType(generateResponse.CiphertextBlob.value),
155-
Types.KeyStoreException(
155+
Types.KeyManagementException(
156156
message := "Invalid response from AWS KMS GenerateDataKey: Invalid ciphertext")
157157
);
158158

@@ -278,7 +278,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
278278
&& reEncryptResponse.SourceKeyId.value == kmsKeyArn
279279
&& reEncryptResponse.KeyId.value == kmsKeyArn,
280280
Types.KeyManagementException(
281-
message := "Invalid response from AWS KMS ReEncrypt:: Invalid KMS Key Id")
281+
message := "Invalid response from AWS KMS ReEncrypt: Invalid KMS Key Id")
282282
);
283283

284284
:- Need(
@@ -353,113 +353,12 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
353353
&& decryptResponse.KeyId.Some?
354354
&& decryptResponse.KeyId.value == kmsKeyArn,
355355
Types.KeyManagementException(
356-
message := "Invalid response from AWS KMS Decrypt :: Invalid KMS Key Id"
356+
message := "Invalid response from AWS KMS Decrypt: Invalid KMS Key Id"
357357
));
358358

359359
return Success(decryptResponse);
360360
}
361361

362-
method MutateViaDecryptEncrypt(
363-
ciphertext: seq<uint8>,
364-
sourceEncryptionContext: Structure.BranchKeyContext,
365-
destinationEncryptionContext: Structure.BranchKeyContext,
366-
sourceKmsArn: string,
367-
destinationKmsArn: string,
368-
decryptGrantTokens: KMS.GrantTokenList,
369-
decryptKmsClient: KMS.IKMSClient,
370-
encryptGrantTokens: KMS.GrantTokenList,
371-
encryptKmsClient: KMS.IKMSClient
372-
)
373-
returns (res: Result<KMS.CiphertextType, KmsError>)
374-
requires
375-
&& Structure.BranchKeyContext?(sourceEncryptionContext)
376-
&& Structure.BranchKeyContext?(destinationEncryptionContext)
377-
requires AttemptReEncrypt?(sourceEncryptionContext, destinationEncryptionContext)
378-
requires KmsArn.ValidKmsArn?(sourceKmsArn) && KmsArn.ValidKmsArn?(destinationKmsArn)
379-
requires decryptKmsClient.Modifies !! encryptKmsClient.Modifies
380-
requires decryptKmsClient.ValidState() && encryptKmsClient.ValidState()
381-
modifies decryptKmsClient.Modifies + encryptKmsClient.Modifies
382-
ensures decryptKmsClient.ValidState() && encryptKmsClient.ValidState()
383-
ensures
384-
res.Success?
385-
==>
386-
&& KMS.IsValid_CiphertextType(ciphertext)
387-
&& |decryptKmsClient.History.Decrypt| == |old(decryptKmsClient.History.Decrypt)| + 1
388-
&& var decryptInput := Seq.Last(decryptKmsClient.History.Decrypt).input;
389-
&& var decryptOutput := Seq.Last(decryptKmsClient.History.Decrypt).output;
390-
&& KMS.DecryptRequest(
391-
CiphertextBlob := ciphertext,
392-
EncryptionContext := Some(sourceEncryptionContext),
393-
GrantTokens := Some(decryptGrantTokens),
394-
KeyId := Some(sourceKmsArn)
395-
) == decryptInput
396-
&& decryptOutput.Success? && decryptOutput.value.Plaintext.Some? && decryptOutput.value.KeyId.Some?
397-
&& decryptOutput.value.KeyId.value == sourceKmsArn
398-
&& |encryptKmsClient.History.Encrypt| == |old(encryptKmsClient.History.Encrypt)| + 1
399-
&& var encryptInput := Seq.Last(encryptKmsClient.History.Encrypt).input;
400-
&& var encryptResponse := Seq.Last(encryptKmsClient.History.Encrypt).output;
401-
&& KMS.EncryptRequest(
402-
KeyId := destinationKmsArn,
403-
Plaintext := decryptOutput.value.Plaintext.value,
404-
EncryptionContext := Some(destinationEncryptionContext),
405-
GrantTokens := Some(encryptGrantTokens)
406-
) == encryptInput
407-
&& old(encryptKmsClient.History.Encrypt) < encryptKmsClient.History.Encrypt
408-
&& encryptResponse.Success?
409-
&& encryptResponse.value.CiphertextBlob.Some?
410-
&& encryptResponse.value.KeyId.Some?
411-
&& encryptResponse.value.KeyId.value == destinationKmsArn // kmsKeyArn
412-
&& KMS.IsValid_CiphertextType(encryptResponse.value.CiphertextBlob.value)
413-
&& encryptResponse.value.CiphertextBlob.value == res.value
414-
{
415-
:- Need(
416-
KMS.IsValid_CiphertextType(ciphertext),
417-
Types.KeyManagementException(
418-
message := "Invalid KMS ciphertext.")
419-
);
420-
421-
var kmsDecryptRequest := KMS.DecryptRequest(
422-
CiphertextBlob := ciphertext,
423-
EncryptionContext := Some(sourceEncryptionContext),
424-
GrantTokens := Some(decryptGrantTokens),
425-
KeyId := Some(sourceKmsArn)
426-
);
427-
428-
var decryptResponse? := decryptKmsClient.Decrypt(kmsDecryptRequest);
429-
var decryptResponse :- decryptResponse?
430-
.MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));
431-
432-
:- Need(
433-
&& decryptResponse.Plaintext.Some?
434-
&& decryptResponse.KeyId.Some?
435-
&& decryptResponse.KeyId.value == sourceKmsArn,
436-
Types.KeyManagementException(
437-
message := "Invalid response from AWS KMS Decrypt :: Invalid KMS Key Id"
438-
));
439-
440-
var kmsEncryptRequest := KMS.EncryptRequest(
441-
KeyId := destinationKmsArn,
442-
Plaintext := decryptResponse.Plaintext.value,
443-
EncryptionContext := Some(destinationEncryptionContext),
444-
GrantTokens := Some(encryptGrantTokens)
445-
);
446-
447-
var encryptResponse? := encryptKmsClient.Encrypt(kmsEncryptRequest);
448-
var encryptResponse :- encryptResponse?
449-
.MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));
450-
451-
:- Need(
452-
&& encryptResponse.CiphertextBlob.Some?
453-
&& KMS.IsValid_CiphertextType(encryptResponse.CiphertextBlob.value)
454-
&& encryptResponse.KeyId.Some?
455-
&& encryptResponse.KeyId.value == destinationKmsArn,
456-
Types.KeyManagementException(
457-
message := "Invalid response from AWS KMS Encrypt :: Invalid KMS Key Id"
458-
));
459-
460-
return Success(encryptResponse.CiphertextBlob.value);
461-
}
462-
463362
method MutateViaDecryptEncryptOnInitializeMutation(
464363
ciphertext: seq<uint8>,
465364
sourceEncryptionContext: Structure.BranchKeyContext,
@@ -532,7 +431,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
532431
&& decryptResponse.KeyId.Some?
533432
&& decryptResponse.KeyId.value == sourceKmsArn,
534433
Types.KeyManagementException(
535-
message := "Invalid response from AWS KMS Decrypt :: Invalid KMS Key Id"
434+
message := "Invalid response from AWS KMS Decrypt: Invalid KMS Key Id"
536435
));
537436

538437
var kmsEncryptRequest := KMS.EncryptRequest(
@@ -552,7 +451,7 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
552451
&& encryptResponse.KeyId.Some?
553452
&& encryptResponse.KeyId.value == destinationKmsArn,
554453
Types.KeyManagementException(
555-
message := "Invalid response from AWS KMS Encrypt :: Invalid KMS Key Id"
454+
message := "Invalid response from AWS KMS Encrypt: Invalid KMS Key Id"
556455
));
557456

558457
return Success(encryptResponse.CiphertextBlob.value);
@@ -640,13 +539,13 @@ module {:options "/functionSyntax:4" } KMSKeystoreOperations {
640539
&& reEncryptResponse.SourceKeyId.Some?
641540
&& reEncryptResponse.SourceKeyId.value == sourceKmsArn, //kmsKeyArn
642541
Types.KeyManagementException(
643-
message := "Invalid response from KMS ReEncrypt:: Invalid Source Key Id")
542+
message := "Invalid response from KMS ReEncrypt: Invalid Source Key Id")
644543
);
645544
:- Need(
646545
&& reEncryptResponse.KeyId.Some?
647546
&& reEncryptResponse.KeyId.value == destinationKmsArn, // kmsKeyArn,
648547
Types.KeyManagementException(
649-
message := "Invalid response from KMS ReEncrypt:: Invalid Destination Key Id")
548+
message := "Invalid response from KMS ReEncrypt: Invalid Destination Key Id")
650549
);
651550

652551
:- Need(

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/InitializeMutation.dfy

+11-3
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ include "KmsUtils.dfy"
77
include "MutationIndexUtils.dfy"
88
include "SystemKey/Handler.dfy"
99
include "Mutations.dfy"
10+
include "MutationErrorRefinement.dfy"
1011

1112
module {:options "/functionSyntax:4" } InternalInitializeMutation {
1213
// StandardLibrary Imports
@@ -33,6 +34,7 @@ module {:options "/functionSyntax:4" } InternalInitializeMutation {
3334
import MutationIndexUtils
3435
import SystemKeyHandler = SystemKey.Handler
3536
import Mutations
37+
import MutationErrorRefinement
3638

3739
datatype InternalInitializeMutationInput = | InternalInitializeMutationInput (
3840
nameonly Identifier: string ,
@@ -417,12 +419,18 @@ module {:options "/functionSyntax:4" } InternalInitializeMutation {
417419
grantTokens := grantTokens,
418420
kmsClient := kmsClient
419421
);
420-
var wrappedDecryptOnlyBranchKey :- wrappedDecryptOnlyBranchKey?
421-
.MapFailure(e => Types.Error.AwsCryptographyKeyStore(e));
422+
423+
if (wrappedDecryptOnlyBranchKey?.Failure?) {
424+
var error := MutationErrorRefinement.GenerateNewActiveException(
425+
identifier := decryptOnlyEncryptionContext[Structure.BRANCH_KEY_IDENTIFIER_FIELD],
426+
kmsArn := mutationToApply.Terminal.kmsArn,
427+
error := wrappedDecryptOnlyBranchKey?.error);
428+
return Failure(error);
429+
}
422430

423431
var newDecryptOnly := Structure.ConstructEncryptedHierarchicalKey(
424432
decryptOnlyEncryptionContext,
425-
wrappedDecryptOnlyBranchKey.CiphertextBlob.value
433+
wrappedDecryptOnlyBranchKey?.value.CiphertextBlob.value
426434
);
427435

428436
:- Need(

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/MutateViaDecryptEncrypt.dfy

+134
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,134 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
include "../Model/AwsCryptographyKeyStoreAdminTypes.dfy"
4+
5+
module {:options "/functionSyntax:4" } MutateViaDecryptEncrypt {
6+
import opened Wrappers
7+
import opened UInt = StandardLibrary.UInt
8+
import opened Seq
9+
10+
import KeyStoreTypes = AwsCryptographyKeyStoreAdminTypes.AwsCryptographyKeyStoreTypes
11+
import Structure
12+
import KMSKeystoreOperations
13+
14+
method Decrypt(
15+
ciphertext: seq<uint8>,
16+
encryptionContext: Structure.BranchKeyContext,
17+
kmsArn: string,
18+
grantTokens: KMSKeystoreOperations.KMS.GrantTokenList,
19+
kmsClient: KMSKeystoreOperations.KMS.IKMSClient
20+
) returns (res: Result<KMSKeystoreOperations.KMS.PlaintextType, KMSKeystoreOperations.KmsError>)
21+
requires Structure.BranchKeyContext?(encryptionContext)
22+
requires KMSKeystoreOperations.KmsArn.ValidKmsArn?(kmsArn)
23+
requires kmsClient.ValidState()
24+
modifies kmsClient.Modifies
25+
ensures kmsClient.ValidState()
26+
ensures
27+
res.Success?
28+
==>
29+
&& KMSKeystoreOperations.KMS.IsValid_CiphertextType(ciphertext)
30+
&& |kmsClient.History.Decrypt| == |old(kmsClient.History.Decrypt)| + 1
31+
&& var decryptInput := Seq.Last(kmsClient.History.Decrypt).input;
32+
&& var decryptOutput := Seq.Last(kmsClient.History.Decrypt).output;
33+
&& KMSKeystoreOperations.KMS.DecryptRequest(
34+
CiphertextBlob := ciphertext,
35+
EncryptionContext := Some(encryptionContext),
36+
GrantTokens := Some(grantTokens),
37+
KeyId := Some(kmsArn)
38+
) == decryptInput
39+
&& decryptOutput.Success? && decryptOutput.value.Plaintext.Some? && decryptOutput.value.KeyId.Some?
40+
&& decryptOutput.value.KeyId.value == kmsArn
41+
&& res.value == decryptOutput.value.Plaintext.value
42+
{
43+
:- Need(
44+
KMSKeystoreOperations.KMS.IsValid_CiphertextType(ciphertext),
45+
KMSKeystoreOperations.Types.KeyManagementException(
46+
message := "The Branch Key's `enc` or ciphertext field is invalid."
47+
+ " Something must have tampered with the stored item, or the read was bad.")
48+
);
49+
50+
var kmsDecryptRequest := KMSKeystoreOperations.KMS.DecryptRequest(
51+
CiphertextBlob := ciphertext,
52+
EncryptionContext := Some(encryptionContext),
53+
GrantTokens := Some(grantTokens),
54+
KeyId := Some(kmsArn)
55+
);
56+
57+
var decryptResponse? := kmsClient.Decrypt(kmsDecryptRequest);
58+
var decryptResponse :- decryptResponse?
59+
.MapFailure(e => KMSKeystoreOperations.Types.ComAmazonawsKms(ComAmazonawsKms := e));
60+
61+
:- Need(
62+
&& decryptResponse.KeyId.Some?
63+
&& decryptResponse.KeyId.value == kmsArn,
64+
KMSKeystoreOperations.Types.KeyManagementException(
65+
message := "Invalid response from AWS KMS Decrypt: KMS Key ID of response did not match request."
66+
));
67+
:- Need(
68+
&& decryptResponse.Plaintext.Some?
69+
&& KMSKeystoreOperations.KMS.IsValid_PlaintextType(decryptResponse.Plaintext.value),
70+
KMSKeystoreOperations.Types.KeyManagementException(
71+
message := "Invalid response from AWS KMS Decrypt: KMS response did not include plaintext."
72+
));
73+
return Success(decryptResponse.Plaintext.value);
74+
}
75+
76+
method Encrypt(
77+
plaintext: KMSKeystoreOperations.KMS.PlaintextType,
78+
encryptionContext: Structure.BranchKeyContext,
79+
kmsArn: string,
80+
grantTokens: KMSKeystoreOperations.KMS.GrantTokenList,
81+
kmsClient: KMSKeystoreOperations.KMS.IKMSClient
82+
) returns (res: Result<KMSKeystoreOperations.KMS.CiphertextType, KMSKeystoreOperations.KmsError>)
83+
requires Structure.BranchKeyContext?(encryptionContext)
84+
requires KMSKeystoreOperations.KmsArn.ValidKmsArn?(kmsArn)
85+
requires kmsClient.ValidState()
86+
modifies kmsClient.Modifies
87+
ensures kmsClient.ValidState()
88+
ensures
89+
res.Success?
90+
==>
91+
&& |kmsClient.History.Encrypt| == |old(kmsClient.History.Encrypt)| + 1
92+
&& var encryptInput := Seq.Last(kmsClient.History.Encrypt).input;
93+
&& var encryptResponse := Seq.Last(kmsClient.History.Encrypt).output;
94+
&& KMSKeystoreOperations.KMS.EncryptRequest(
95+
KeyId := kmsArn,
96+
Plaintext := plaintext,
97+
EncryptionContext := Some(encryptionContext),
98+
GrantTokens := Some(grantTokens)
99+
) == encryptInput
100+
&& encryptResponse.Success?
101+
&& encryptResponse.value.CiphertextBlob.Some?
102+
&& encryptResponse.value.KeyId.Some?
103+
&& encryptResponse.value.KeyId.value == kmsArn
104+
&& KMSKeystoreOperations.KMS.IsValid_CiphertextType(encryptResponse.value.CiphertextBlob.value)
105+
&& encryptResponse.value.CiphertextBlob.value == res.value
106+
{
107+
var kmsEncryptRequest := KMSKeystoreOperations.KMS.EncryptRequest(
108+
KeyId := kmsArn,
109+
Plaintext := plaintext,
110+
EncryptionContext := Some(encryptionContext),
111+
GrantTokens := Some(grantTokens)
112+
);
113+
114+
var encryptResponse? := kmsClient.Encrypt(kmsEncryptRequest);
115+
var encryptResponse :- encryptResponse?
116+
.MapFailure(e => KMSKeystoreOperations.Types.ComAmazonawsKms(ComAmazonawsKms := e));
117+
118+
:- Need(
119+
&& encryptResponse.CiphertextBlob.Some?
120+
&& KMSKeystoreOperations.KMS.IsValid_CiphertextType(encryptResponse.CiphertextBlob.value),
121+
KMSKeystoreOperations.Types.KeyManagementException(
122+
message := "Invalid response from AWS KMS Encrypt: KMS response's Ciphertext is invalid."
123+
)
124+
);
125+
:- Need(
126+
&& encryptResponse.KeyId.Some?
127+
&& encryptResponse.KeyId.value == kmsArn,
128+
KMSKeystoreOperations.Types.KeyManagementException(
129+
message := "Invalid response from AWS KMS Encrypt: KMS Key ID of response did not match request."
130+
)
131+
);
132+
return Success(encryptResponse.CiphertextBlob.value);
133+
}
134+
}

0 commit comments

Comments
 (0)