Skip to content

Commit fec798d

Browse files
texastonytexastony
authored
fix(dafny): BKS & KMS Keyring Verification (#1537)
1 parent 279d4af commit fec798d

File tree

5 files changed

+449
-184
lines changed

5 files changed

+449
-184
lines changed

‎.github/workflows/library_dafny_verification.yml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,14 @@ jobs:
7171
CORES=$(node -e 'console.log(os.cpus().length)')
7272
make verify CORES=$CORES
7373
74+
# If you ever need to figure out ONE file in CI, here is a pttern
75+
# - name: Verify ${{ matrix.library }} Dafny code
76+
# working-directory: ./${{ matrix.library }}
77+
# run: |
78+
# # This works because `node` is installed by default on GHA runners
79+
# CORES=$(node -e 'console.log(os.cpus().length)')
80+
# make verify_single FILE=dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy CORES=$CORES
81+
7482
- name: Check solver resource use
7583
if: success() || failure()
7684
working-directory: ./${{ matrix.library }}

‎.github/workflows/pull.yml‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,12 @@ jobs:
3939
uses: ./.github/workflows/library_net_tests.yml
4040
with:
4141
dafny: ${{needs.getVersion.outputs.version}}
42+
pr-interop-test:
43+
needs: getVersion
44+
uses: ./.github/workflows/library_interop_tests.yml
45+
with:
46+
dafny: ${{needs.getVersion.outputs.version}}
47+
secrets: inherit
4248
# TODO-HV-2-Rust: Removing Rust until we rebase or need it
4349
# pr-ci-rust:
4450
# needs: getVersion
@@ -57,30 +63,24 @@ jobs:
5763
# uses: ./.github/workflows/library_go_tests.yml
5864
# with:
5965
# dafny: ${{needs.getVersion.outputs.version}}
60-
pr-interop-test:
61-
needs: getVersion
62-
uses: ./.github/workflows/library_interop_tests.yml
63-
with:
64-
dafny: ${{needs.getVersion.outputs.version}}
65-
secrets: inherit
6666
pr-ci-all-required:
6767
if: always()
6868
needs:
6969
- getVersion
7070
- getVerifyVersion
71+
- pr-ci-verification
7172
- pr-ci-format
7273
- pr-ci-codegen
73-
- pr-ci-verification
7474
- pr-ci-java
7575
- pr-ci-net
76+
- pr-interop-test
77+
- pr-ci-examples
7678
# TODO-HV-2-Python: Removing Python until we fix bugs in Dafny/Python transpilation
7779
# - pr-ci-python
7880
# TODO-HV-2-Go: Removing Go CI until we rebase or need it
7981
# - pr-ci-go
8082
# TODO-HV-2-Rust: Removing Rust until we rebase or need it
8183
# - pr-ci-rust
82-
- pr-interop-test
83-
- pr-ci-examples
8484
runs-on: ubuntu-22.04
8585
steps:
8686
- name: Verify all required jobs passed

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

Lines changed: 31 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -455,6 +455,12 @@ module AwsKmsKeyring {
455455
//# included in the input [decryption materials]
456456
//# (../structures.md#decryption-materials).
457457
&& AlgorithmSuites.GetEncryptKeyLength(input.materials.algorithmSuite) as nat == |res.value.materials.plaintextDataKey.value|
458+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
459+
//= type=implication
460+
//# To attempt to decrypt a particular [encrypted data key]
461+
//# (../structures.md#encrypted-data-key), OnDecrypt MUST call [AWS KMS
462+
//# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html)
463+
//# with the configured AWS KMS client.
458464
&& var LastDecrypt := Last(client.History.Decrypt);
459465
&& LastDecrypt.output.Success?
460466
&& OkForDecrypt(awsKmsArn, awsKmsKey).Pass?
@@ -476,36 +482,26 @@ module AwsKmsKeyring {
476482
//# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html),
477483
//# the keyring MUST call with a request constructed
478484
//# as follows:
479-
&& KMS.DecryptRequest(
480-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
481-
//= type=implication
482-
//# - `KeyId` MUST be the configured AWS KMS key identifier.
483-
KeyId := Some(awsKmsKey),
484-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
485-
//= type=implication
486-
//# - `CiphertextBlob` MUST be the [encrypted data key ciphertext]
487-
//# (../structures.md#ciphertext).
488-
CiphertextBlob := maybeWrappedMaterial.value,
489-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
490-
//= type=implication
491-
//# - `EncryptionContext` MUST be the [encryption context]
492-
//# (../structures.md#encryption-context) included in the input
493-
//# [decryption materials](../structures.md#decryption-materials).
494-
EncryptionContext := Some(maybeStringifiedEncCtx.value),
495-
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
496-
//= type=implication
497-
//# - `GrantTokens` MUST be this keyring's [grant tokens]
498-
//# (https://docs.aws.amazon.com/kms/latest/developerguide/concepts.html#grant_token).
499-
GrantTokens := Some(grantTokens),
500-
EncryptionAlgorithm := None
501-
)
502485
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
503486
//= type=implication
504-
//# To attempt to decrypt a particular [encrypted data key]
505-
//# (../structures.md#encrypted-data-key), OnDecrypt MUST call [AWS KMS
506-
//# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html)
507-
//# with the configured AWS KMS client.
508-
== LastDecrypt.input
487+
//# - `KeyId` MUST be the configured AWS KMS key identifier.
488+
&& LastDecrypt.input.KeyId == Some(awsKmsKey)
489+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
490+
//= type=implication
491+
//# - `CiphertextBlob` MUST be the [encrypted data key ciphertext]
492+
//# (../structures.md#ciphertext).
493+
&& LastDecrypt.input.CiphertextBlob == maybeWrappedMaterial.value
494+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
495+
//= type=implication
496+
//# - `EncryptionContext` MUST be the [encryption context]
497+
//# (../structures.md#encryption-context) included in the input
498+
//# [decryption materials](../structures.md#decryption-materials).
499+
&& LastDecrypt.input.EncryptionContext == Some(maybeStringifiedEncCtx.value)
500+
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
501+
//= type=implication
502+
//# - `GrantTokens` MUST be this keyring's [grant tokens]
503+
//# (https://docs.aws.amazon.com/kms/latest/developerguide/concepts.html#grant_token).
504+
&& LastDecrypt.input.GrantTokens == Some(grantTokens)
509505
//= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
510506
//= type=implication
511507
//# - The `KeyId` field in the response MUST equal the configured AWS
@@ -592,7 +588,13 @@ module AwsKmsKeyring {
592588
&& var maybeWrappedMaterial :=
593589
EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, input.materials.algorithmSuite);
594590
&& maybeWrappedMaterial.Success?
595-
&& KMS.IsValid_CiphertextType(maybeWrappedMaterial.value);
591+
&& KMS.IsValid_CiphertextType(maybeWrappedMaterial.value)
592+
&& LastDecrypt.input.KeyId == Some(awsKmsKey)
593+
&& LastDecrypt.input.CiphertextBlob == maybeWrappedMaterial.value
594+
&& LastDecrypt.input.GrantTokens == Some(grantTokens)
595+
&& var maybeStringifiedEncCtx := StringifyEncryptionContext(materials.encryptionContext);
596+
&& maybeStringifiedEncCtx.Success?
597+
&& LastDecrypt.input.EncryptionContext == Some(maybeStringifiedEncCtx.value);
596598

597599
assert decryptClosure.Ensures(Last(attempts).input, Success(SealedDecryptionMaterials), DropLast(attempts));
598600
return Success(Types.OnDecryptOutput(

0 commit comments

Comments
 (0)