From ae00d3a8c1a245451016617ea11fba8d232fcd7c Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 19 Jul 2024 12:07:12 -0400 Subject: [PATCH 1/3] feat: allow indirect attribute names with MultiKeyStore --- .../DynamoDbEncryption/src/FilterExpr.dfy | 2 +- .../test/BeaconTestFixtures.dfy | 64 +++++++++++++++++- .../DynamoDbEncryption/test/DDBSupport.dfy | 65 +++++++++++++++++++ 3 files changed, 129 insertions(+), 2 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy index b9cdb6384..2f2a2cff9 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy @@ -1533,7 +1533,7 @@ module DynamoDBFilterExpr { else var name := if names.Some? && attr.value.s in names.value then names.value[attr.value.s] else attr.value.s; var keyIdField := bv.keySource.keyLoc.keyName; - if keyIdField == attr.value.s then + if keyIdField == name then Some(value) else KeyIdFromPart(bv, keyIdField, attr.value.s, value) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index b96e0d566..039592400 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy @@ -141,6 +141,29 @@ module BeaconTestFixtures { return store; } + method GetMultiKeyStore() returns (output : SI.ValidStore) + ensures fresh(output.Modifies) + { + var kmsClient :- expect KMS.KMSClient(); + var ddbClient :- expect DDBC.DynamoDBClient(); + var kmsConfig := KTypes.KMSConfiguration.kmsKeyArn( + "arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126" + ); + var keyStoreConfig := KTypes.KeyStoreConfig( + id := None, + kmsConfiguration := kmsConfig, + logicalKeyStoreName := "KeyStoreDdbTable", + grantTokens := None, + ddbTableName := "KeyStoreDdbTable", + ddbClient := Some(ddbClient), + kmsClient := Some(kmsClient) + ); + + var store :- expect KeyStore.KeyStore(keyStoreConfig); + return store; + } + + method GetEmptyBeacons() returns (output : BeaconVersion) ensures output.keyStore.ValidState() ensures fresh(output.keyStore.Modifies) @@ -177,6 +200,24 @@ module BeaconTestFixtures { ); } + method GetLotsaBeaconsMulti() returns (output : BeaconVersion) + ensures output.keyStore.ValidState() + ensures fresh(output.keyStore.Modifies) + ensures output.version == 1 + { + var store := GetMultiKeyStore(); + return BeaconVersion ( + version := 1, + keyStore := store, + keySource := multi(MultiKeyStore(keyFieldName := "TheKeyField", cacheTTL := 42)), + standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB], + compoundBeacons := Some([NameTitle, YearName, Mixed, JustSigned]), + virtualFields := Some([NameTitleField]), + encryptedParts := None, + signedParts := None + ); + } + const EmptyTableConfig := DynamoDbTableEncryptionConfig ( logicalTableName := "Foo", partitionKeyName := "foo", @@ -200,7 +241,8 @@ module BeaconTestFixtures { "Title" := SE.ENCRYPT_AND_SIGN, "TooBad" := SE.ENCRYPT_AND_SIGN, "Year" := SE.SIGN_ONLY, - "Date" := SE.SIGN_ONLY + "Date" := SE.SIGN_ONLY, + "TheKeyField" := SE.SIGN_ONLY ] ) @@ -223,6 +265,26 @@ module BeaconTestFixtures { return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0); } + datatype KeyLocation = + | LiteralLoc (keys: HmacKeyMap) + | SingleLoc (keyId: string) + | MultiLoc (keyName : string, deleteKey : bool) + + method GetMultiSource(keyName : string, version : BeaconVersion) returns (output : SI.KeySource) + requires version.keyStore.ValidState() + ensures output.ValidState() + ensures version.keyStore == output.store + ensures fresh(output.client.Modifies) + { + var client :- expect Primitives.AtomicPrimitives(); + var mpl :- expect MaterialProviders.MaterialProviders(); + var input := MPT.CreateCryptographicMaterialsCacheInput( + cache := MPT.Default(Default := MPT.DefaultCache(entryCapacity := 3)) + ); + var cache :- expect mpl.CreateCryptographicMaterialsCache(input); + return SI.KeySource(client, version.keyStore, SI.MultiLoc(keyName, false), cache, 0); + } + const SimpleItem : DDB.AttributeMap := map[ "std2" := Std2String, "std4" := Std4String, diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy index df292e684..3f09ec783 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy @@ -32,4 +32,69 @@ module TestDDBSupport { expect newItem == SimpleItem + expectedNew; } + function method DS(x : string) : DDB.AttributeValue + { + DDB.AttributeValue.S(x) + } + + method {:test} TestMulti() { + var version := GetLotsaBeaconsMulti(); + var src := GetMultiSource("TheKeyField", version); + var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); + var search := SI.SearchInfo([bv], 0); + var expressionAttributeValues : map := map[ + ":value" := DS("0ad21413-51aa-42e1-9c3d-6a4b1edf7e10") + ]; + var queryInput := DDB.QueryInput ( + TableName := "SomeTable", + ExpressionAttributeValues := Some(expressionAttributeValues), + KeyConditionExpression := Some("TheKeyField = :value") + ); + var result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + + expressionAttributeValues := map[ + ":value" := DS("0ad21413-51aa-42e1-9c3d-6a4b1edf7e10"), + ":other" := DS("junk") + ]; + queryInput := DDB.QueryInput ( + TableName := "foo", + ExpressionAttributeValues := Some(expressionAttributeValues), + KeyConditionExpression := Some("TheKeyField = :value AND std2 = :other") + ); + result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + + queryInput := DDB.QueryInput ( + TableName := "foo", + ExpressionAttributeValues := Some(expressionAttributeValues), + KeyConditionExpression := Some("std2 = :other") + ); + var result2 := QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + expect result2 == Failure(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.DynamoDbEncryptionException( + message := "Need KeyId because of beacon std2 but no KeyId found in query")); + + var expressionAttributeNames := map[ + "#beacon" := "std2", + "#keyfield" := "TheKeyField" + ]; + queryInput := DDB.QueryInput ( + TableName := "foo", + ExpressionAttributeNames := Some(expressionAttributeNames), + ExpressionAttributeValues := Some(expressionAttributeValues), + KeyConditionExpression := Some("#keyfield = :value AND #beacon = :other") + ); + result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + } } +// Map expressionAttributesNames = new HashMap<>(); +// expressionAttributesNames.put("#compound", "firstNameCompound"); + +// Map expressionAttributeValues = new HashMap<>(); +// expressionAttributeValues.put(":value", AttributeValue.builder().s("f1-l.f2-li.f3-lil.f4-lily.s-Placeholder - 3afba703-6345-4a25-b28a-ec22b1b79a35").build()); + +// QueryRequest queryRequest = QueryRequest.builder() +// .tableName(tableName) +// .indexName("aws_dbe_b_firstNameCompound-index") +// .keyConditionExpression("#compound = :value") +// .expressionAttributeNames(expressionAttributesNames) +// .expressionAttributeValues(expressionAttributeValues) +// .build(); From 7fff1c11ec997be7ccd9209f1011b283b4b759c4 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 19 Jul 2024 12:38:44 -0400 Subject: [PATCH 2/3] remove noise --- .../test/BeaconTestFixtures.dfy | 5 ----- .../dafny/DynamoDbEncryption/test/DDBSupport.dfy | 16 +++------------- 2 files changed, 3 insertions(+), 18 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index 039592400..c890fdde5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy @@ -265,11 +265,6 @@ module BeaconTestFixtures { return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0); } - datatype KeyLocation = - | LiteralLoc (keys: HmacKeyMap) - | SingleLoc (keyId: string) - | MultiLoc (keyName : string, deleteKey : bool) - method GetMultiSource(keyName : string, version : BeaconVersion) returns (output : SI.KeySource) requires version.keyStore.ValidState() ensures output.ValidState() diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy index 3f09ec783..cb73f312d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy @@ -52,6 +52,7 @@ module TestDDBSupport { ); var result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + // Verify Success with branch key id plus beacon expressionAttributeValues := map[ ":value" := DS("0ad21413-51aa-42e1-9c3d-6a4b1edf7e10"), ":other" := DS("junk") @@ -63,6 +64,7 @@ module TestDDBSupport { ); result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + // Verify Failure with beacon but no branch key id queryInput := DDB.QueryInput ( TableName := "foo", ExpressionAttributeValues := Some(expressionAttributeValues), @@ -72,6 +74,7 @@ module TestDDBSupport { expect result2 == Failure(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.DynamoDbEncryptionException( message := "Need KeyId because of beacon std2 but no KeyId found in query")); + // Verify Success, even when field names are indirect via ExpressionAttributeNames var expressionAttributeNames := map[ "#beacon" := "std2", "#keyfield" := "TheKeyField" @@ -85,16 +88,3 @@ module TestDDBSupport { result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); } } -// Map expressionAttributesNames = new HashMap<>(); -// expressionAttributesNames.put("#compound", "firstNameCompound"); - -// Map expressionAttributeValues = new HashMap<>(); -// expressionAttributeValues.put(":value", AttributeValue.builder().s("f1-l.f2-li.f3-lil.f4-lily.s-Placeholder - 3afba703-6345-4a25-b28a-ec22b1b79a35").build()); - -// QueryRequest queryRequest = QueryRequest.builder() -// .tableName(tableName) -// .indexName("aws_dbe_b_firstNameCompound-index") -// .keyConditionExpression("#compound = :value") -// .expressionAttributeNames(expressionAttributesNames) -// .expressionAttributeValues(expressionAttributeValues) -// .build(); From d83d88ef0182014296d3f0610e909d8c1f3b63c5 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 19 Jul 2024 13:02:58 -0400 Subject: [PATCH 3/3] cleanup --- .../test/BeaconTestFixtures.dfy | 25 +------------------ .../DynamoDbEncryption/test/DDBSupport.dfy | 1 + 2 files changed, 2 insertions(+), 24 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index c890fdde5..7244fa87a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy @@ -121,28 +121,6 @@ module BeaconTestFixtures { method GetKeyStore() returns (output : SI.ValidStore) ensures fresh(output.Modifies) - { - var kmsClient :- expect KMS.KMSClient(); - var ddbClient :- expect DDBC.DynamoDBClient(); - var kmsConfig := KTypes.KMSConfiguration.kmsKeyArn( - "arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126" - ); - var keyStoreConfig := KTypes.KeyStoreConfig( - id := None, - kmsConfiguration := kmsConfig, - logicalKeyStoreName := "foo", - grantTokens := None, - ddbTableName := "foo", - ddbClient := Some(ddbClient), - kmsClient := Some(kmsClient) - ); - - var store :- expect KeyStore.KeyStore(keyStoreConfig); - return store; - } - - method GetMultiKeyStore() returns (output : SI.ValidStore) - ensures fresh(output.Modifies) { var kmsClient :- expect KMS.KMSClient(); var ddbClient :- expect DDBC.DynamoDBClient(); @@ -163,7 +141,6 @@ module BeaconTestFixtures { return store; } - method GetEmptyBeacons() returns (output : BeaconVersion) ensures output.keyStore.ValidState() ensures fresh(output.keyStore.Modifies) @@ -205,7 +182,7 @@ module BeaconTestFixtures { ensures fresh(output.keyStore.Modifies) ensures output.version == 1 { - var store := GetMultiKeyStore(); + var store := GetKeyStore(); return BeaconVersion ( version := 1, keyStore := store, diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy index cb73f312d..4cf5118cc 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy @@ -32,6 +32,7 @@ module TestDDBSupport { expect newItem == SimpleItem + expectedNew; } + // DynamoDB String :: cast string to DDB.AttributeValue.S function method DS(x : string) : DDB.AttributeValue { DDB.AttributeValue.S(x)