feat(keystore) Branch Key Store read consistency

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<I, O> = 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<string>
   type HmacKeyMap = map<string, Secret>
@@ -231,7 +232,8 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
     nameonly id: Option<string> := Option.None ,
     nameonly grantTokens: Option<GrantTokenList> := Option.None ,
     nameonly ddbClient: Option<ComAmazonawsDynamodbTypes.IDynamoDBClient> := Option.None ,
-    nameonly kmsClient: Option<ComAmazonawsKmsTypes.IKMSClient> := Option.None
+    nameonly kmsClient: Option<ComAmazonawsKmsTypes.IKMSClient> := Option.None ,
+    nameonly requireConsistentReads: Option<bool> := Option.None
   )
   datatype KMSConfiguration =
     | kmsKeyArn(kmsKeyArn: ComAmazonawsKmsTypes.KeyIdType)

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.")

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
     );
   }
 }

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<Types.VersionKeyOutput, Types.Error>)
     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

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<Structure.ActiveBranchKeyItem, Types.Error>)
     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<Structure.VersionBranchKeyItem, Types.Error>)
     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<Structure.BeaconKeyItem, Types.Error>)
     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

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<Types.GetActiveBranchKeyOutput, Types.Error>)
     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<Types.GetBranchKeyVersionOutput, Types.Error>)
     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<Types.GetBeaconKeyOutput, Types.Error>)
     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);