diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy index a371045798..db30c0285d 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy @@ -11,7 +11,7 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw import opened UTF8 import ComAmazonawsDynamodbTypes import ComAmazonawsKmsTypes - // Generic helpers for verification of mock/unit tests. + // Generic helpers for verification of mock/unit tests. datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) // Begin Generated Types @@ -69,7 +69,8 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw nameonly keyStoreName: ComAmazonawsDynamodbTypes.TableName , nameonly logicalKeyStoreName: string , nameonly grantTokens: GrantTokenList , - nameonly kmsConfiguration: KMSConfiguration + nameonly kmsConfiguration: KMSConfiguration , + nameonly requireConsistentReads: bool ) type GrantTokenList = seq type HmacKeyMap = map @@ -231,7 +232,8 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw nameonly id: Option := Option.None , nameonly grantTokens: Option := Option.None , nameonly ddbClient: Option := Option.None , - nameonly kmsClient: Option := Option.None + nameonly kmsClient: Option := Option.None , + nameonly requireConsistentReads: Option := Option.None ) datatype KMSConfiguration = | kmsKeyArn(kmsKeyArn: ComAmazonawsKmsTypes.KeyIdType) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/KeyStore.smithy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/KeyStore.smithy index 8eb8935711..c4ff92f920 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/KeyStore.smithy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/KeyStore.smithy @@ -89,6 +89,7 @@ structure KeyStoreConfig { //# - [ID](#keystore-id) //# - [AWS KMS Grant Tokens](#aws-kms-grant-tokens) //# - [DynamoDb Client](#dynamodb-client) + //# - [Require Consistent Reads](#require-consistent-reads) //# - [KMS Client](#kms-client) @javadoc("An identifier for this Key Store.") @@ -99,6 +100,9 @@ structure KeyStoreConfig { ddbClient: DdbClientReference, @javadoc("The KMS client this Key Store uses to call AWS KMS. If None is provided and the KMS ARN is, the KMS ARN is used to determine the Region of the default client.") kmsClient: KmsClientReference, + + @javadoc("Whether read operations are required to perform consistent reads. If set to true read operations return results which reflect the most recently executed write operations. Defaults to false.") + requireConsistentReads: Boolean, } //= aws-encryption-sdk-specification/framework/branch-key-store.md#aws-kms-configuration @@ -156,7 +160,10 @@ structure GetKeyStoreInfoOutput { grantTokens: GrantTokenList, @required @javadoc("Configures Key Store's KMS Key ARN restrictions.") - kmsConfiguration: KMSConfiguration + kmsConfiguration: KMSConfiguration, + @required + @javadoc("The consistent reads configuration of this keystore instance.") + requireConsistentReads: Boolean, } @javadoc("Create the DynamoDB table that backs this Key Store based on the Key Store configuration. If a table already exists, validate it is configured as expected.") diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy index 5b6494a233..4f86dbb65d 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy @@ -30,6 +30,7 @@ module AwsCryptographyKeyStoreOperations refines AbstractAwsCryptographyKeyStore nameonly id: string, nameonly ddbTableName: DDB.TableName, nameonly logicalKeyStoreName: string, + nameonly requireConsistentReads: bool, nameonly kmsConfiguration: KMSConfiguration, nameonly grantTokens: KMS.GrantTokenList, nameonly kmsClient: ComAmazonawsKmsTypes.IKMSClient, @@ -77,7 +78,8 @@ module AwsCryptographyKeyStoreOperations refines AbstractAwsCryptographyKeyStore keyStoreName := config.ddbTableName, logicalKeyStoreName := config.logicalKeyStoreName, grantTokens := config.grantTokens, - kmsConfiguration := config.kmsConfiguration + kmsConfiguration := config.kmsConfiguration, + requireConsistentReads := config.requireConsistentReads ) ); } @@ -246,7 +248,8 @@ module AwsCryptographyKeyStoreOperations refines AbstractAwsCryptographyKeyStore config.kmsConfiguration, config.grantTokens, config.kmsClient, - config.ddbClient + config.ddbClient, + config.requireConsistentReads ); } @@ -263,7 +266,8 @@ module AwsCryptographyKeyStoreOperations refines AbstractAwsCryptographyKeyStore config.kmsConfiguration, config.grantTokens, config.kmsClient, - config.ddbClient + config.ddbClient, + config.requireConsistentReads ); } @@ -280,7 +284,8 @@ module AwsCryptographyKeyStoreOperations refines AbstractAwsCryptographyKeyStore config.kmsConfiguration, config.grantTokens, config.kmsClient, - config.ddbClient + config.ddbClient, + config.requireConsistentReads ); } @@ -297,7 +302,8 @@ module AwsCryptographyKeyStoreOperations refines AbstractAwsCryptographyKeyStore config.kmsConfiguration, config.grantTokens, config.kmsClient, - config.ddbClient + config.ddbClient, + config.requireConsistentReads ); } } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy index 5b6a7199d3..5f17703b60 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy @@ -108,7 +108,7 @@ module {:options "/functionSyntax:4" } CreateKeys { //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation //= type=implication - //# - `KeyId` MUST be [compatible with](#aws-key-arn-compatibility) the configured KMS Key in the [AWS KMS Configuration](#aws-kms-configuration) for this keystore. + //# - `KeyId` MUST be the configured `AWS KMS Key ARN` in the [AWS KMS Configuration](#aws-kms-configuration) for this keystore. && KMSKeystoreOperations.Compatible?(kmsConfiguration, beaconKmsInput.KeyId) //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation @@ -301,7 +301,8 @@ module {:options "/functionSyntax:4" } CreateKeys { kmsConfiguration: Types.KMSConfiguration, grantTokens: KMS.GrantTokenList, kmsClient: KMS.IKMSClient, - ddbClient: DDB.IDynamoDBClient + ddbClient: DDB.IDynamoDBClient, + requireConsistentReads: bool ) returns (output: Result) requires 0 < |input.branchKeyIdentifier| && 0 < |branchKeyVersion| @@ -326,6 +327,13 @@ module {:options "/functionSyntax:4" } CreateKeys { Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.BRANCH_KEY_ACTIVE_TYPE) ] + //= aws-encryption-sdk-specification/framework/branch-key-store.md#versionkey + //= type=implication + //# The [Require Consistent Reads](#require-consistent-reads) configuration MUST be honored + //# by setting `ConsistentRead` to `true` + //# when consistent reads are required. + && Seq.Last(ddbClient.History.GetItem).input.ConsistentRead == Some(requireConsistentReads) + && Seq.Last(ddbClient.History.GetItem).output.Success? && Seq.Last(ddbClient.History.GetItem).output.value.Item.Some? && var oldActiveItem := Seq.Last(ddbClient.History.GetItem).output.value.Item.value; @@ -362,6 +370,12 @@ module {:options "/functionSyntax:4" } CreateKeys { //# - `SourceEncryptionContext` MUST be the [encryption context](#encryption-context) constructed above && reEncryptInput.SourceEncryptionContext == Some(Structure.ToBranchKeyContext(oldActiveItem, logicalKeyStoreName)) + //= aws-encryption-sdk-specification/framework/branch-key-store.md#versionkey + //= type=implication + //# The `kms-arn` stored in the DDB table MUST NOT change as a result of this operation, + //# even if the KeyStore is configured with a `KMS MRKey ARN` that does not exactly match the stored ARN. + && reEncryptInput.SourceEncryptionContext.value[Structure.KMS_FIELD] == oldActiveItem[Structure.KMS_FIELD].S + //= aws-encryption-sdk-specification/framework/branch-key-store.md#authenticating-a-keystore-item //= type=implication //# - `SourceKeyId` MUST be [compatible with](#aws-key-arn-compatibility) the configured KMS Key in the [AWS KMS Configuration](#aws-kms-configuration) for this keystore. @@ -482,7 +496,8 @@ module {:options "/functionSyntax:4" } CreateKeys { var oldActiveItem :- DDBKeystoreOperations.GetActiveBranchKeyItem( input.branchKeyIdentifier, ddbTableName, - ddbClient + ddbClient, + requireConsistentReads ); var oldActiveEncryptionContext := Structure.ToBranchKeyContext(oldActiveItem, logicalKeyStoreName); @@ -583,7 +598,7 @@ module {:options "/functionSyntax:4" } CreateKeys { //= aws-encryption-sdk-specification/framework/branch-key-store.md#wrapped-branch-key-creation //= type=implication - //# - `KeyId` MUST be [compatible with](#aws-key-arn-compatibility) the configured KMS Key in the [AWS KMS Configuration](#aws-kms-configuration) for this keystore. + //# - `KeyId` MUST be the configured `AWS KMS Key ARN` in the [AWS KMS Configuration](#aws-kms-configuration) for this keystore. && KMSKeystoreOperations.Compatible?(kmsConfiguration, decryptOnlyKmsInput.KeyId) //= aws-encryption-sdk-specification/framework/branch-key-store.md#wrapped-branch-key-creation @@ -612,12 +627,12 @@ module {:options "/functionSyntax:4" } CreateKeys { //= aws-encryption-sdk-specification/framework/branch-key-store.md#wrapped-branch-key-creation //= type=implication - //# - `SourceKeyId` MUST be [compatible with](#aws-key-arn-compatibility) the configured KMS Key in the [AWS KMS Configuration](#aws-kms-configuration) for this keystore. + //# - `SourceKeyId` MUST be the configured `AWS KMS Key ARN` in the [AWS KMS Configuration](#aws-kms-configuration) for this keystore. && KMSKeystoreOperations.OptCompatible?(kmsConfiguration, activeInput.SourceKeyId) //= aws-encryption-sdk-specification/framework/branch-key-store.md#wrapped-branch-key-creation //= type=implication - //# - `DestinationKeyId` MUST be [compatible with](#aws-key-arn-compatibility) the configured KMS Key in the [AWS KMS Configuration](#aws-kms-configuration) for this keystore. + //# - `DestinationKeyId` MUST be the configured `AWS KMS Key ARN` in the [AWS KMS Configuration](#aws-kms-configuration) for this keystore. && KMSKeystoreOperations.Compatible?(kmsConfiguration, activeInput.DestinationKeyId) //= aws-encryption-sdk-specification/framework/branch-key-store.md#wrapped-branch-key-creation diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DDBKeystoreOperations.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DDBKeystoreOperations.dfy index 63d7985e6f..fbdec7ce46 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DDBKeystoreOperations.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/DDBKeystoreOperations.dfy @@ -146,7 +146,8 @@ module DDBKeystoreOperations { method GetActiveBranchKeyItem( branchKeyIdentifier: string, tableName: DDB.TableName, - ddbClient: DDB.IDynamoDBClient + ddbClient: DDB.IDynamoDBClient, + requireConsistentReads: bool ) returns (output: Result) requires DDB.IsValid_TableName(tableName) @@ -161,6 +162,8 @@ module DDBKeystoreOperations { Structure.BRANCH_KEY_IDENTIFIER_FIELD := DDB.AttributeValue.S(branchKeyIdentifier), Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.BRANCH_KEY_ACTIVE_TYPE) ] + && Seq.Last(ddbClient.History.GetItem).input.ConsistentRead == Some(requireConsistentReads) + ensures output.Success? ==> && output.value[Structure.BRANCH_KEY_IDENTIFIER_FIELD].S == branchKeyIdentifier @@ -187,7 +190,7 @@ module DDBKeystoreOperations { Key := dynamoDbKey, TableName := tableName, AttributesToGet := None, - ConsistentRead := None, + ConsistentRead := Some(requireConsistentReads), ReturnConsumedCapacity := None, ProjectionExpression := None, ExpressionAttributeNames := None @@ -216,7 +219,8 @@ module DDBKeystoreOperations { branchKeyIdentifier: string, branchKeyVersion: string, tableName: DDB.TableName, - ddbClient: DDB.IDynamoDBClient + ddbClient: DDB.IDynamoDBClient, + requireConsistentReads: bool ) returns (output: Result) requires DDB.IsValid_TableName(tableName) @@ -231,6 +235,7 @@ module DDBKeystoreOperations { Structure.BRANCH_KEY_IDENTIFIER_FIELD := DDB.AttributeValue.S(branchKeyIdentifier), Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.BRANCH_KEY_TYPE_PREFIX + branchKeyVersion) ] + && Seq.Last(ddbClient.History.GetItem).input.ConsistentRead == Some(requireConsistentReads) ensures output.Success? ==> @@ -255,7 +260,7 @@ module DDBKeystoreOperations { Key := dynamoDbKey, TableName := tableName, AttributesToGet := None, - ConsistentRead := None, + ConsistentRead := Some(requireConsistentReads), ReturnConsumedCapacity := None, ProjectionExpression := None, ExpressionAttributeNames := None @@ -284,7 +289,8 @@ module DDBKeystoreOperations { method GetBeaconKeyItem( branchKeyIdentifier: string, tableName: DDB.TableName, - ddbClient: DDB.IDynamoDBClient + ddbClient: DDB.IDynamoDBClient, + requireConsistentReads: bool ) returns (output: Result) requires DDB.IsValid_TableName(tableName) @@ -302,6 +308,7 @@ module DDBKeystoreOperations { Structure.BRANCH_KEY_IDENTIFIER_FIELD := DDB.AttributeValue.S(branchKeyIdentifier), Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.BEACON_KEY_TYPE_VALUE) ] + && Seq.Last(ddbClient.History.GetItem).input.ConsistentRead == Some(requireConsistentReads) ensures output.Success? ==> @@ -326,7 +333,7 @@ module DDBKeystoreOperations { Key := dynamoDbKey, TableName := tableName, AttributesToGet := None, - ConsistentRead := None, + ConsistentRead := Some(requireConsistentReads), ReturnConsumedCapacity := None, ProjectionExpression := None, ExpressionAttributeNames := None diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy index 8605e8efd8..b433049da0 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy @@ -31,7 +31,8 @@ module GetKeys { kmsConfiguration: Types.KMSConfiguration, grantTokens: KMS.GrantTokenList, kmsClient: KMS.IKMSClient, - ddbClient: DDB.IDynamoDBClient + ddbClient: DDB.IDynamoDBClient, + requireConsistentReads: bool ) returns (output: Result) requires ddbClient.Modifies !! kmsClient.Modifies @@ -53,6 +54,13 @@ module GetKeys { Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.BRANCH_KEY_ACTIVE_TYPE) ] + //= aws-encryption-sdk-specification/framework/branch-key-store.md#getactivebranchkey + //= type=implication + //# The [Require Consistent Reads](#require-consistent-reads) configuration MUST be honored + //# by setting `ConsistentRead` to `true` + //# when consistent reads are required. + && Seq.Last(ddbClient.History.GetItem).input.ConsistentRead == Some(requireConsistentReads) + ensures output.Success? ==> && Seq.Last(ddbClient.History.GetItem).output.Success? @@ -124,7 +132,8 @@ module GetKeys { var branchKeyItem :- DDBKeystoreOperations.GetActiveBranchKeyItem( input.branchKeyIdentifier, tableName, - ddbClient + ddbClient, + requireConsistentReads ); var encryptionContext := Structure.ToBranchKeyContext(branchKeyItem, logicalKeyStoreName); @@ -165,7 +174,8 @@ module GetKeys { kmsConfiguration: Types.KMSConfiguration, grantTokens: KMS.GrantTokenList, kmsClient: KMS.IKMSClient, - ddbClient: DDB.IDynamoDBClient + ddbClient: DDB.IDynamoDBClient, + requireConsistentReads: bool ) returns (output: Result) requires ddbClient.Modifies !! kmsClient.Modifies @@ -186,6 +196,13 @@ module GetKeys { Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.BRANCH_KEY_TYPE_PREFIX + input.branchKeyVersion) ] + //= aws-encryption-sdk-specification/framework/branch-key-store.md#getbranchkeyversion + //= type=implication + //# The [Require Consistent Reads](#require-consistent-reads) configuration MUST be honored + //# by setting `ConsistentRead` to `true` + //# when consistent reads are required. + && Seq.Last(ddbClient.History.GetItem).input.ConsistentRead == Some(requireConsistentReads) + ensures output.Success? ==> && Seq.Last(ddbClient.History.GetItem).output.Success? @@ -261,7 +278,8 @@ module GetKeys { input.branchKeyIdentifier, input.branchKeyVersion, tableName, - ddbClient + ddbClient, + requireConsistentReads ); var encryptionContext := Structure.ToBranchKeyContext(branchKeyItem, logicalKeyStoreName); @@ -301,7 +319,8 @@ module GetKeys { kmsConfiguration: Types.KMSConfiguration, grantTokens: KMS.GrantTokenList, kmsClient: KMS.IKMSClient, - ddbClient: DDB.IDynamoDBClient + ddbClient: DDB.IDynamoDBClient, + requireConsistentReads: bool ) returns (output: Result) requires ddbClient.Modifies !! kmsClient.Modifies @@ -322,6 +341,13 @@ module GetKeys { Structure.TYPE_FIELD := DDB.AttributeValue.S(Structure.BEACON_KEY_TYPE_VALUE) ] + //= aws-encryption-sdk-specification/framework/branch-key-store.md#getbeaconkey + //= type=implication + //# The [Require Consistent Reads](#require-consistent-reads) configuration MUST be honored + //# by setting `ConsistentRead` to `true` + //# when consistent reads are required. + && Seq.Last(ddbClient.History.GetItem).input.ConsistentRead == Some(requireConsistentReads) + ensures output.Success? ==> && Seq.Last(ddbClient.History.GetItem).output.Success? && Seq.Last(ddbClient.History.GetItem).output.value.Item.Some? @@ -393,7 +419,8 @@ module GetKeys { var branchKeyItem :- DDBKeystoreOperations.GetBeaconKeyItem( input.branchKeyIdentifier, tableName, - ddbClient + ddbClient, + requireConsistentReads ); var encryptionContext := Structure.ToBranchKeyContext(branchKeyItem, logicalKeyStoreName); diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy index 550b8c9be1..cf22b3be15 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy @@ -29,7 +29,8 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny"} KeyStore id := None, grantTokens := None, kmsClient := None, - ddbClient := None + ddbClient := None, + requireConsistentReads := Some(false) ) } @@ -178,7 +179,8 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny"} KeyStore kmsConfiguration := config.kmsConfiguration, grantTokens := grantTokens.value, kmsClient := kmsClient, - ddbClient := ddbClient + ddbClient := ddbClient, + requireConsistentReads := config.requireConsistentReads.UnwrapOr(false) ) ); return Success(client); diff --git a/aws-encryption-sdk-specification b/aws-encryption-sdk-specification index 8f4afff943..c277763d7b 160000 --- a/aws-encryption-sdk-specification +++ b/aws-encryption-sdk-specification @@ -1 +1 @@ -Subproject commit 8f4afff94358492e1e2e8847d1c6b78db5b204b2 +Subproject commit c277763d7b532aef79cd7975c910398893e527f1