diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy index da87f4a30..08b8a5b5e 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy @@ -100,7 +100,19 @@ module Fixtures { const KmsMrkConfigAP : Types.KMSConfiguration := Types.KMSConfiguration.kmsMRKeyArn(MrkArnAP) const KmsMrkEC : Types.EncryptionContext := map[UTF8.EncodeAscii("abc") := UTF8.EncodeAscii("123")] const EastBranchKey : string := "MyEastBranch2" + const EastBranchKeyIdActiveVersion : string := "6f22825b-bd56-4434-83e2-2782e2160172" + const EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes: seq := [ + 54, 102, 50, 50, 56, 50, 53, 98, 45, 98, 100, + 53, 54, 45, 52, 52, 51, 52, 45, 56, 51, 101, 50, + 45, 50, 55, 56, 50, 101, 50, 49, 54, 48, 49, 55, 50 + ] const WestBranchKey : string := "MyWestBranch2" + const WestBranchKeyIdActiveVersion : string := "094715a4-b98d-4c98-bf50-17422a8938f4" + const WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes: seq := [ + 48, 57, 52, 55, 49, 53, 97, 52, 45, 98, 57, 56, + 100, 45, 52, 99, 57, 56, 45, 98, 102, 53, 48, 45, + 49, 55, 52, 50, 50, 97, 56, 57, 51, 56, 102, 52 + ] const publicKeyArn := "arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f" // TODO: After ~2024/06/11 launch, add the next two lines to cfn/ESDK-Hierarchy-CI.yaml @@ -243,14 +255,19 @@ module Fixtures { return Success(keyStore); } - method KeyStoreWithNoClient( + method KeyStoreWithOptionalClient( nameonly kmsId: string := keyArn, nameonly physicalName: string := branchKeyStoreName, - nameonly logicalName: string := logicalKeyStoreName + nameonly logicalName: string := logicalKeyStoreName, + nameonly ddbClient?: Option := None, + nameonly kmsClient?: Option := None, + nameonly srkKey: bool := true, + nameonly mrkKey: bool := false ) returns (output: Result) requires DDB.Types.IsValid_TableName(physicalName) requires KMS.Types.IsValid_KeyIdType(kmsId) + requires srkKey != mrkKey ensures output.Success? ==> output.value.ValidState() ensures output.Success? ==> @@ -258,7 +275,19 @@ module Fixtures { && fresh(output.value) && fresh(output.value.Modifies) { - var kmsConfig := Types.KMSConfiguration.kmsKeyArn(kmsId); + if ddbClient?.Some? { + assume {:axiom} fresh(ddbClient?.value) && fresh(ddbClient?.value.Modifies); + } + if kmsClient?.Some? { + assume {:axiom} fresh(kmsClient?.value) && fresh(kmsClient?.value.Modifies); + } + expect srkKey != mrkKey; + var kmsConfig := if srkKey then + createSrkKMSConfig(kmsId) + else + createMrkKMSConfig(kmsId); + expect srkKey ==> kmsConfig.kmsKeyArn?; + expect mrkKey ==> kmsConfig.kmsMRKeyArn?; var keyStoreConfig := Types.KeyStoreConfig( id := None, kmsConfiguration := kmsConfig, @@ -266,13 +295,33 @@ module Fixtures { storage := Some( Types.ddb( Types.DynamoDBTable( - ddbTableName := physicalName + ddbTableName := physicalName, + ddbClient := ddbClient? + ))), + keyManagement := Some( + Types.kms( + Types.AwsKms( + kmsClient := kmsClient? ))) ); var keyStore :- expect KeyStore.KeyStore(keyStoreConfig); return Success(keyStore); } + function method createSrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration) + requires KMS.Types.IsValid_KeyIdType(kmsId) + ensures output.kmsKeyArn? + { + Types.KMSConfiguration.kmsKeyArn(kmsId) + } + + function method createMrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration) + requires KMS.Types.IsValid_KeyIdType(kmsId) + ensures output.kmsMRKeyArn? + { + Types.KMSConfiguration.kmsMRKeyArn(kmsId) + } + datatype allThree = | allThree ( active: Types.EncryptedHierarchicalKey, beacon: Types.EncryptedHierarchicalKey, diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy index 2309503b5..c1215f118 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy @@ -77,128 +77,89 @@ module TestGetKeys { { var ddbClient :- expect DDB.DynamoDBClient(); - var eastKeyStoreConfig := Types.KeyStoreConfig( - id := None, - kmsConfiguration := KmsConfigEast, - logicalKeyStoreName := logicalKeyStoreName, - storage := Some( - Types.ddb( - Types.DynamoDBTable( - ddbTableName := branchKeyStoreName, - ddbClient := Some(ddbClient) - ))) + var westKeyStore :- expect KeyStoreWithOptionalClient( + kmsId := MrkArnWest, + physicalName := branchKeyStoreName, + logicalName := logicalKeyStoreName, + ddbClient? := Some(ddbClient) ); - var westKeyStoreConfig := Types.KeyStoreConfig( - id := None, - kmsConfiguration := KmsConfigWest, - logicalKeyStoreName := logicalKeyStoreName, - storage := Some( - Types.ddb( - Types.DynamoDBTable( - ddbTableName := branchKeyStoreName, - ddbClient := Some(ddbClient) - ))) + var eastKeyStore :- expect KeyStoreWithOptionalClient( + kmsId := MrkArnEast, + physicalName := branchKeyStoreName, + logicalName := logicalKeyStoreName, + ddbClient? := Some(ddbClient) ); - var eastMrkKeyStoreConfig := Types.KeyStoreConfig( - id := None, - kmsConfiguration := KmsMrkConfigEast, - logicalKeyStoreName := logicalKeyStoreName, - storage := Some( - Types.ddb( - Types.DynamoDBTable( - ddbTableName := branchKeyStoreName, - ddbClient := Some(ddbClient) - ))) + var westMrkKeyStore :- expect KeyStoreWithOptionalClient( + kmsId := MrkArnWest, + physicalName := branchKeyStoreName, + logicalName := logicalKeyStoreName, + ddbClient? := Some(ddbClient), + srkKey := false, + mrkKey := true ); - var westMrkKeyStoreConfig := Types.KeyStoreConfig( - id := None, - kmsConfiguration := KmsMrkConfigWest, - logicalKeyStoreName := logicalKeyStoreName, - storage := Some( - Types.ddb( - Types.DynamoDBTable( - ddbTableName := branchKeyStoreName, - ddbClient := Some(ddbClient) - ))) + var eastMrkKeyStore :- expect KeyStoreWithOptionalClient( + kmsId := MrkArnEast, + physicalName := branchKeyStoreName, + logicalName := logicalKeyStoreName, + ddbClient? := Some(ddbClient), + srkKey := false, + mrkKey := true ); - // KmsMrkConfigAP is NOT created - var apMrkKeyStoreConfig := Types.KeyStoreConfig( - id := None, - kmsConfiguration := KmsMrkConfigAP, - logicalKeyStoreName := logicalKeyStoreName, - storage := Some( - Types.ddb( - Types.DynamoDBTable( - ddbTableName := branchKeyStoreName, - ddbClient := Some(ddbClient) - ))) + var apMrkKeyStore :- expect KeyStoreWithOptionalClient( + kmsId := MrkArnAP, + physicalName := branchKeyStoreName, + logicalName := logicalKeyStoreName, + ddbClient? := Some(ddbClient), + srkKey := false, + mrkKey := true ); + // All four set of keys (branch, beacon and version) should work when the regions match + testActiveBranchKeyHappyCase(westKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes); + testBeaconKeyHappyCase(westKeyStore, WestBranchKey); + testBranchKeyVersionHappyCase(westKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes); - var westKeyStore :- expect KeyStore.KeyStore(westKeyStoreConfig); - var eastKeyStore :- expect KeyStore.KeyStore(eastKeyStoreConfig); - var westMrkKeyStore :- expect KeyStore.KeyStore(westMrkKeyStoreConfig); - var eastMrkKeyStore :- expect KeyStore.KeyStore(eastMrkKeyStoreConfig); - var apMrkKeyStore :- expect KeyStore.KeyStore(apMrkKeyStoreConfig); + testActiveBranchKeyHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes); + testBeaconKeyHappyCase(eastKeyStore, EastBranchKey); + testBranchKeyVersionHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes); - // All four should work when the regions match + testActiveBranchKeyHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes); + testBeaconKeyHappyCase(westMrkKeyStore, WestBranchKey); + testBranchKeyVersionHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes); - var activeResult :- expect westKeyStore.GetActiveBranchKey( - Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey)); - expect activeResult.branchKeyMaterials.branchKeyIdentifier == WestBranchKey; - expect |activeResult.branchKeyMaterials.branchKey| == 32; - - activeResult :- expect eastKeyStore.GetActiveBranchKey( - Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey)); - expect activeResult.branchKeyMaterials.branchKeyIdentifier == EastBranchKey; - expect |activeResult.branchKeyMaterials.branchKey| == 32; - - activeResult :- expect westMrkKeyStore.GetActiveBranchKey( - Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey)); - expect activeResult.branchKeyMaterials.branchKeyIdentifier == WestBranchKey; - expect |activeResult.branchKeyMaterials.branchKey| == 32; - - activeResult :- expect eastMrkKeyStore.GetActiveBranchKey( - Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey)); - expect activeResult.branchKeyMaterials.branchKeyIdentifier == EastBranchKey; - expect |activeResult.branchKeyMaterials.branchKey| == 32; + testActiveBranchKeyHappyCase(eastMrkKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes); + testBeaconKeyHappyCase(eastMrkKeyStore, EastBranchKey); + testBranchKeyVersionHappyCase(eastMrkKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes); // MRK Configuration should work with the other region - activeResult :- expect westMrkKeyStore.GetActiveBranchKey( - Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey)); - expect activeResult.branchKeyMaterials.branchKeyIdentifier == EastBranchKey; - expect |activeResult.branchKeyMaterials.branchKey| == 32; + testActiveBranchKeyHappyCase(westMrkKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes); + testBeaconKeyHappyCase(westMrkKeyStore, EastBranchKey); + testBranchKeyVersionHappyCase(westMrkKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes); - activeResult :- expect eastMrkKeyStore.GetActiveBranchKey( - Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey)); - expect activeResult.branchKeyMaterials.branchKeyIdentifier == WestBranchKey; - expect |activeResult.branchKeyMaterials.branchKey| == 32; + testActiveBranchKeyHappyCase(eastMrkKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes); + testBeaconKeyHappyCase(eastMrkKeyStore, WestBranchKey); + testBranchKeyVersionHappyCase(eastMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes); // Plain Configuration should fail with the other region - var badResult := westKeyStore.GetActiveBranchKey( - Types.GetActiveBranchKeyInput(branchKeyIdentifier := EastBranchKey)); - expect badResult.Failure?; - expect badResult.error == Types.Error.KeyStoreException(message := ErrorMessages.GET_KEY_ARN_DISAGREEMENT); + GetActiveKeyWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey); + GetBeaconKeyWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey); + GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion); - badResult := eastKeyStore.GetActiveBranchKey( - Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey)); - expect badResult.Failure?; - expect badResult.error == Types.Error.KeyStoreException(message := ErrorMessages.GET_KEY_ARN_DISAGREEMENT); + GetActiveKeyWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey); + GetBeaconKeyWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey); + GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion); // apMrkKeyStore should always fail - badResult := apMrkKeyStore.GetActiveBranchKey( - Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey)); - expect badResult.Failure?; - expect badResult.error.ComAmazonawsKms?; - expect badResult.error.ComAmazonawsKms.OpaqueWithText?; - // it's an opaque error, so I can't test its contents + testActiveBranchKeyKMSFailureCase(apMrkKeyStore, WestBranchKey); + testBranchKeyVersionKMSFailureCase(apMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion); + testBeaconKeyKMSFailureCase(apMrkKeyStore, WestBranchKey); } method {:test} TestKeyWithIncorrectKmsKeyArn() { @@ -246,7 +207,7 @@ module TestGetKeys { method {:test} TestGetKeysWithNoClients() { var kmsConfig := Types.KMSConfiguration.kmsKeyArn(keyArn); - var keyStore :- expect KeyStoreWithNoClient(kmsId:=keyArn, physicalName:=branchKeyStoreName, logicalName := logicalKeyStoreName); + var keyStore :- expect KeyStoreWithOptionalClient(kmsId:=keyArn, physicalName:=branchKeyStoreName, logicalName := logicalKeyStoreName); testActiveBranchKeyHappyCase(keyStore, branchKeyId, branchKeyIdActiveVersionUtf8Bytes); testActiveBranchKeyHappyCase(keyStore, hv2BranchKeyId, hv2BranchKeyIdActiveVersionUtf8Bytes); @@ -462,6 +423,46 @@ module TestGetKeys { && |versionResult.branchKeyMaterials.branchKey| == 32 } + method testActiveBranchKeyKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string) + requires keyStore.ValidState() + modifies keyStore.Modifies + { + var branchKeyResult := keyStore.GetActiveBranchKey( + Types.GetActiveBranchKeyInput( + branchKeyIdentifier := branchKeyId + )); + expect branchKeyResult.Failure?; + expect branchKeyResult.error.ComAmazonawsKms?; + expect branchKeyResult.error.ComAmazonawsKms.OpaqueWithText?; + } + + method testBranchKeyVersionKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string, branchKeyIdActiveVersion: string) + requires keyStore.ValidState() + modifies keyStore.Modifies + { + var versionResult := keyStore.GetBranchKeyVersion( + Types.GetBranchKeyVersionInput( + branchKeyIdentifier := branchKeyId, + branchKeyVersion := branchKeyIdActiveVersion + )); + expect versionResult.Failure?; + expect versionResult.error.ComAmazonawsKms?; + expect versionResult.error.ComAmazonawsKms.OpaqueWithText?; + } + + method testBeaconKeyKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string) + requires keyStore.ValidState() + modifies keyStore.Modifies + { + var beaconKeyResult := keyStore.GetBeaconKey( + Types.GetBeaconKeyInput( + branchKeyIdentifier := branchKeyId + )); + expect beaconKeyResult.Failure?; + expect beaconKeyResult.error.ComAmazonawsKms?; + expect beaconKeyResult.error.ComAmazonawsKms.OpaqueWithText?; + } + method VerifyGetKeysFromStorage( identifier : string, storage : Types.IKeyStorageInterface