diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 580dbb3ad..9f1dd7e90 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -397,6 +397,12 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestBatchWriteItem(c1, c2, globalRecords); BasicIoTestPutItem(c1, c2, globalRecords); BasicIoTestTransactWriteItems(c1, c2, globalRecords); + BasicIoTestUpdateItem(c1, c2, globalRecords, "One"); + BasicIoTestUpdateItem(c1, c2, globalRecords, "Two"); + BasicIoTestDeleteItem(c1, c2, globalRecords, "One", "Uno"); + BasicIoTestDeleteItem(c1, c2, globalRecords, "Two", "Dos"); + BasicIoTestDeleteItemWithoutConditionExpression(c1, c2, globalRecords, "One", "Uno"); + BasicIoTestDeleteItemWithoutConditionExpression(c1, c2, globalRecords, "Two", "Dos"); BasicIoTestExecuteStatement(c1, c2); BasicIoTestExecuteTransaction(c1, c2); BasicIoTestBatchExecuteStatement(c1, c2); @@ -844,6 +850,108 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { BasicIoTestTransactGetItems(rClient, records); } + method BasicIoTestUpdateItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq, attributeToUpdate: DDB.AttributeName) + { + var wClient, rClient := SetupTestTable(writeConfig, readConfig); + WriteAllRecords(wClient, records); + // Update each record by appending "updated" to the partition key + for i := 0 to |records| { + var newValue := "updated"; + // Create an update expression to update the partition key + var updateExpr := "SET #att = :val"; + expect attributeToUpdate in writeConfig.config.attributeActionsOnEncrypt, "`attributeToUpdate` not in attributeActionsOnEncrypt"; + var exprAttrNames := map["#att" := attributeToUpdate]; + var exprAttrValues := map[":val" := DDB.AttributeValue.S(newValue)]; + expect HashName in records[i].item, "`HashName` is not in records."; + var updateInput := DDB.UpdateItemInput( + TableName := TableName, + Key := map[HashName := records[i].item[HashName]], + UpdateExpression := Some(updateExpr), + ExpressionAttributeNames := Some(exprAttrNames), + ExpressionAttributeValues := Some(exprAttrValues), + ReturnValues := None, + ReturnConsumedCapacity := None, + ReturnItemCollectionMetrics := None, + ConditionExpression := None + ); + var updateResult := wClient.UpdateItem(updateInput); + if writeConfig.config.attributeActionsOnEncrypt[attributeToUpdate] == SE.ENCRYPT_AND_SIGN || writeConfig.config.attributeActionsOnEncrypt[attributeToUpdate] == SE.SIGN_ONLY { + expect updateResult.Failure?, "UpdateItem should have failed for signed item."; + // This error is of type DynamoDbEncryptionTransformsException + // but AWS SDK wraps it into its own type for which customers should be unwrapping. + // In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText. + expect updateResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText"; + var hasDynamoDbEncryptionTransformsException? := String.HasSubString(updateResult.error.objMessage, "Update Expressions forbidden on signed attributes"); + expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException"; + } else { + expect updateResult.Success?; + } + } + } + + method BasicIoTestDeleteItem(writeConfig : TableConfig, readConfig : TableConfig, records : seq, attributeToDelete: DDB.AttributeName, expectedAttributeValue: string) + { + var wClient, rClient := SetupTestTable(writeConfig, readConfig); + WriteAllRecords(wClient, records); + // Try to delete records with a condition expression with condition to + // delete records if the record has an attribute attributeToDelete with value expectedAttributeValue + for i := 0 to |records| { + // Set up condition expression to only delete if Two = expectedAttributeValue + var conditionExpr := "#attr = :val"; + var exprAttrNames := map["#attr" := attributeToDelete]; + var exprAttrValues := map[":val" := DDB.AttributeValue.S(expectedAttributeValue)]; + expect HashName in records[i].item, "`HashName` is not in records."; + var deleteInput := DDB.DeleteItemInput( + TableName := TableName, + Key := map[HashName := records[i].item[HashName]], + ConditionExpression := Some(conditionExpr), + ExpressionAttributeNames := Some(exprAttrNames), + ExpressionAttributeValues := Some(exprAttrValues), + ReturnValues := Some(DDB.ReturnValue.ALL_OLD) + ); + var deleteResult := wClient.DeleteItem(deleteInput); + expect attributeToDelete in writeConfig.config.attributeActionsOnEncrypt, "`attributeToDelete` not found in attributeActionsOnEncrypt of config."; + if writeConfig.config.attributeActionsOnEncrypt[attributeToDelete] == SE.ENCRYPT_AND_SIGN { + expect deleteResult.Failure?, "DeleteItem should have failed."; + // This error is of type DynamoDbEncryptionTransformsException + // but AWS SDK wraps it into its own type for which customers should be unwrapping. + // In test vectors, we still have to change the error from AWS SDK to dafny so it turns out to be OpaqueWithText. + expect deleteResult.error.OpaqueWithText?, "Error should have been of type OpaqueWithText"; + var hasDynamoDbEncryptionTransformsException? := String.HasSubString(deleteResult.error.objMessage, "Condition Expressions forbidden on encrypted attributes"); + expect hasDynamoDbEncryptionTransformsException?.Some?, "Error might is not be of type DynamoDbEncryptionTransformsException"; + } else if attributeToDelete in records[i].item && records[i].item[attributeToDelete].S? && records[i].item[attributeToDelete].S == expectedAttributeValue { + expect deleteResult.Success?, "DeleteItem should have succeeded."; + expect deleteResult.value.Attributes.Some?, "DeleteItemOutput should have had some attribute because ReturnValues was set as `ALL_OLD` in DeleteItemInput"; + expect HashName in deleteResult.value.Attributes.value, "Deleted item does not have right partition key:" + HashName; + expect deleteResult.value.Attributes.value[HashName] == records[i].item[HashName], "Wrong item was deleted."; + } else { + expect deleteResult.Failure?, "DeleteItem should have failed."; + expect deleteResult.error.ConditionalCheckFailedException?, "DeleteItem should have failed with ConditionalCheckFailedException"; + } + } + } + + method BasicIoTestDeleteItemWithoutConditionExpression(writeConfig : TableConfig, readConfig : TableConfig, records : seq, attributeToDelete: DDB.AttributeName, expectedAttributeValue: string) + { + var wClient, rClient := SetupTestTable(writeConfig, readConfig); + WriteAllRecords(wClient, records); + for i := 0 to |records| { + expect HashName in records[i].item, "`HashName` is not in records."; + var deleteInputWithoutConditionExpression := DDB.DeleteItemInput( + TableName := TableName, + Key := map[HashName := records[i].item[HashName]], + ReturnValues := Some(DDB.ReturnValue.ALL_OLD) + ); + var deleteResultForWithoutConditionExpressionCase := wClient.DeleteItem(deleteInputWithoutConditionExpression); + expect deleteResultForWithoutConditionExpressionCase.Success?, "DeleteItem should have succeeded."; + expect deleteResultForWithoutConditionExpressionCase.value.Attributes.Some?, "DeleteItemOutput should have had some attribute because ReturnValues was set as `ALL_OLD` in DeleteItemInput"; + if attributeToDelete in records[i].item { + expect HashName in deleteResultForWithoutConditionExpressionCase.value.Attributes.value, "Deleted item does not have right partition key:" + HashName; + expect deleteResultForWithoutConditionExpressionCase.value.Attributes.value[HashName] == records[i].item[HashName], "Wrong item was deleted."; + } + } + } + method BasicIoTestExecuteStatement(writeConfig : TableConfig, readConfig : TableConfig) { var wClient, rClient := SetupTestTable(writeConfig, readConfig);