diff --git a/DynamoDbEncryptionMiddlewareInternal/src/DdbMiddlewareConfig.dfy b/DynamoDbEncryptionMiddlewareInternal/src/DdbMiddlewareConfig.dfy index 6662ba0b7..9f53a6e1e 100644 --- a/DynamoDbEncryptionMiddlewareInternal/src/DdbMiddlewareConfig.dfy +++ b/DynamoDbEncryptionMiddlewareInternal/src/DdbMiddlewareConfig.dfy @@ -19,6 +19,7 @@ module DdbMiddlewareConfig { var encryptorConfig := config.itemEncryptor.config; && config.partitionKeyName == encryptorConfig.partitionKeyName && config.sortKeyName == encryptorConfig.sortKeyName + && config.itemEncryptor.ValidState() } type ValidTableConfig = c: TableConfig | ValidTableConfig?(c) witness * diff --git a/DynamoDbItemEncryptor/src/AwsCryptographyDynamoDbItemEncryptorOperations.dfy b/DynamoDbItemEncryptor/src/AwsCryptographyDynamoDbItemEncryptorOperations.dfy index 9d31fd5f5..206db912e 100644 --- a/DynamoDbItemEncryptor/src/AwsCryptographyDynamoDbItemEncryptorOperations.dfy +++ b/DynamoDbItemEncryptor/src/AwsCryptographyDynamoDbItemEncryptorOperations.dfy @@ -3,11 +3,12 @@ include "../Model/AwsCryptographyDynamoDbItemEncryptorTypes.dfy" include "../../private-aws-encryption-sdk-dafny-staging/AwsCryptographicMaterialProviders/src/CMMs/ExpectedEncryptionContextCMM.dfy" include "DynamoToStruct.dfy" +include "Util.dfy" include "../../StructuredEncryption/src/SearchInfo.dfy" module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptographyDynamoDbItemEncryptorOperations { - import opened StructuredEncryptionUtil import ComAmazonawsDynamodbTypes + import opened DynamoDbItemEncryptorUtil import CMP = AwsCryptographyMaterialProvidersTypes import StructuredEncryption import DynamoToStruct @@ -16,10 +17,10 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog import opened StandardLibrary import Seq import CSE = AwsCryptographyStructuredEncryptionTypes - import SE = StructuredEncryptionUtil import MaterialProviders import ExpectedEncryptionContextCMM import opened SearchableEncryptionInfo + import SET = AwsCryptographyStructuredEncryptionTypes datatype Config = Config( nameonly cmpClient : MaterialProviders.MaterialProvidersClient, @@ -38,6 +39,24 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog ) type InternalConfig = Config + type ValidConfig = x : Config | ValidInternalConfig?(x) witness * + + predicate method IsEncrypted(config : ValidConfig, attr : string) + { + && attr in config.attributeActions + && config.attributeActions[attr] == SET.ENCRYPT_AND_SIGN + } + + predicate method IsSigned(config : ValidConfig, attr : string) + { + && attr in config.attributeActions + && config.attributeActions[attr] != SET.DO_NOTHING + } + + const DoNotSign := + CSE.AuthenticateSchema(content := CSE.AuthenticateSchemaContent.Action(CSE.AuthenticateAction.DO_NOT_SIGN), attributes := None) + const DoSign := + CSE.AuthenticateSchema(content := CSE.AuthenticateSchemaContent.Action(CSE.AuthenticateAction.SIGN), attributes := None) // constant attribute names for the encryption context const TABLE_NAME : seq := UTF8.EncodeAscii("aws-crypto-table-name"); @@ -52,7 +71,7 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog { || (unauthenticatedAttributes.Some? && attr in unauthenticatedAttributes.value) || (unauthenticatedPrefix.Some? && unauthenticatedPrefix.value <= attr) - || SE.ReservedPrefix <= attr + || ReservedPrefix <= attr // Attributes with the reserved prefix are "allowed unauthenticated" in that // they are not specified as signed within attributeActions. // These attributes MAY still be authenticated via other methods, @@ -105,7 +124,7 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog else if unauthenticatedPrefix.Some? && unauthenticatedPrefix.value <= attr then "it also begins with the unauthenticatedPrefix." else - assert SE.ReservedPrefix <= attr; + assert ReservedPrefix <= attr; "it also begins with the reserved prefix." } @@ -298,7 +317,7 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog // It is forbidden to explicitly configure an attribute with the reserved prefix && (forall attribute <- config.attributeActions.Keys :: - !(SE.ReservedPrefix <= attribute)) + !(ReservedPrefix <= attribute)) && (config.beacons.Some? ==> config.beacons.value.ValidState()) } @@ -355,13 +374,13 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog //= type=implication //# Otherwise, Attributes MUST be considered as within the signature scope. ensures ret.Success? ==> - ((ret.value == SE.DoNotSign) <==> !InSignatureScope(config, attr)) + ((ret.value == DoNotSign) <==> !InSignatureScope(config, attr)) { :- Need(!UnknownAttribute(config, attr), "Attribute " + attr + " is not configured"); if InSignatureScope(config, attr) then - Success(SE.DoSign) + Success(DoSign) else - Success(SE.DoNotSign) + Success(DoNotSign) } // get CryptoSchema for this item diff --git a/DynamoDbItemEncryptor/src/DDBIndex.dfy b/DynamoDbItemEncryptor/src/DDBIndex.dfy new file mode 100644 index 000000000..2e6d6846e --- /dev/null +++ b/DynamoDbItemEncryptor/src/DDBIndex.dfy @@ -0,0 +1,355 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +/* + Support routines for Local and Global Index structures +*/ + +include "../Model/AwsCryptographyDynamoDbItemEncryptorTypes.dfy" +include "AwsCryptographyDynamoDbItemEncryptorOperations.dfy" +include "Util.dfy" +include "VirtualDDB.dfy" +include "UpdateExpr.dfy" +include "FilterExpr.dfy" + +module DynamoDBIndexSupport { + + import DDB = ComAmazonawsDynamodbTypes + import opened AwsCryptographyDynamoDbItemEncryptorTypes + import opened Wrappers + import opened StandardLibrary + import opened StandardLibrary.UInt + import opened DynamoDbItemEncryptorUtil + import opened AwsCryptographyDynamoDbItemEncryptorOperations + import opened VirtualDDBFields + import UTF8 + import SortedSets + import Seq + import SE = StructuredEncryptionUtil + import Update = DynamoDbUpdateExpr + import SET = AwsCryptographyStructuredEncryptionTypes + import Filter = DynamoDBFilterExpr + + // transform beacon name to plain names + function method UnbeaconString(s : string) : string + { + if SE.ReservedPrefix <= s then + s[|SE.ReservedPrefix|..] + else + s + } + + // transform beacon names to plain names in KeySchemaAttributeName + function method UnbeaconKeySchemaAttributeName(s : DDB.KeySchemaAttributeName) + : Result + { + if SE.ReservedPrefix <= s then + var ret := s[|SE.ReservedPrefix|..]; + if DDB.IsValid_KeySchemaAttributeName(ret) then + Success(ret) + else + Failure("KeySchemaAttributeName " + s + " is invalid after removing prefix") + else + Success(s) + } + + // transform beacon names to plain names in KeySchemaElement + function method UnbeaconKeySchemaElement(s : DDB.KeySchemaElement) + : Result + { + var name :- UnbeaconKeySchemaAttributeName(s.AttributeName); + Success(s.(AttributeName := name)) + } + + // transform beacon names to plain names in KeySchema + function method UnbeaconKeySchema(config : ValidConfig, schema : DDB.KeySchema) + : Result + { + Seq.MapWithResult((k : DDB.KeySchemaElement) => UnbeaconKeySchemaElement(k), schema) + } + + // transform beacon names to plain names in Projection + function method UnbeaconProjection(config : ValidConfig, projection : DDB.Projection) + : Result + { + if projection.NonKeyAttributes.None? then + Success(projection) + else + var newAttributes := Seq.Filter((k : DDB.NonKeyAttributeName) => !(SE.ReservedPrefix <= k), projection.NonKeyAttributes.value); + if DDB.IsValid_NonKeyAttributeNameList(newAttributes) then + Success(projection.(NonKeyAttributes := Some(newAttributes))) + else + Failure("Project had invalid attribute name list") + } + + // transform beacon names to plain names in Global Index Description + function method TransformOneLocalIndexDescription(config : ValidConfig, index : DDB.LocalSecondaryIndexDescription) + : Result + { + if index.KeySchema.None? then + Success(index) + else + var newSchema :- UnbeaconKeySchema(config, index.KeySchema.value); + Success(index.(KeySchema := Some(newSchema))) + } + + // transform beacon names to plain names in Global Index Description + function method TransformOneGlobalIndexDescription(config : ValidConfig, index : DDB.GlobalSecondaryIndexDescription) + : Result + { + var newKeySchema :- + if index.KeySchema.None? then + Success(None) + else + var schema :- UnbeaconKeySchema(config, index.KeySchema.value); + Success(Some(schema)); + + var newProjection :- + if index.Projection.None? then + Success(None) + else + var projection :- UnbeaconProjection(config, index.Projection.value); + Success(Some(projection)); + + Success(index.(KeySchema := newKeySchema, Projection := newProjection)) + } + + // transform beacon names to plain names in Local Index Descriptions + function method TransformLocalIndexDescription(config : ValidConfig, req : Option) + : Result, string> + { + if req.None? then + Success(req) + else + var nList :- Seq.MapWithResult((d :DDB.LocalSecondaryIndexDescription) => TransformOneLocalIndexDescription(config, d), req.value); + Success(Some(nList)) + } + + // transform beacon names to plain names in Global Index Descriptions + function method TransformGlobalIndexDescription(config : ValidConfig, req : Option) + : Result, string> + { + if req.None? then + Success(req) + else + var nList :- Seq.MapWithResult((d :DDB.GlobalSecondaryIndexDescription) => TransformOneGlobalIndexDescription(config, d), req.value); + Success(Some(nList)) + } + + predicate method IsBeacon(config : ValidConfig, name : string) + { + if config.beacons.None? then + false + else + config.beacons.value.IsBeacon(name) + } + + // make beacon name from attribute name + function method MakeBeaconName(config : ValidConfig, name : string) : string + { + BeaconPrefix + name + } + + // make beacon name from attribute name, fail if it's not a valid Key Schema Attribute Name + function method MakeKeySchemaBeaconName(config : ValidConfig, name : string) + : Result + { + var newName := MakeBeaconName(config, name); + if DDB.IsValid_KeySchemaAttributeName(newName) then + Success(newName) + else + Failure("Can't make valid KeySchemaAttributeName from beacon for " + name) + } + + // make beacon name from attribute name, fail if it's not a valid Non Key Attribute Name + function method MakeNonKeyBeaconName(config : ValidConfig, name : string) + : Result + { + var newName := MakeBeaconName(config, name); + if DDB.IsValid_NonKeyAttributeName(newName) then + Success(newName) + else + Failure("Can't make valid NonKeySchemaAttributeName from beacon for " + name) + } + + // replace oldName with newName, and old type with String + function method {:tailrecursion} ReplaceAttrDef( + attrs : DDB.AttributeDefinitions, + oldName : DDB.KeySchemaAttributeName, + newName : DDB.KeySchemaAttributeName + ) + : DDB.AttributeDefinitions + { + if |attrs| == 0 then + attrs + else if attrs[0].AttributeName == oldName then + var newAttr := DDB.AttributeDefinition(AttributeName := newName, AttributeType := DDB.ScalarAttributeType.S); + [newAttr] + ReplaceAttrDef(attrs[1..], oldName, newName) + else + [attrs[0]] + ReplaceAttrDef(attrs[1..], oldName, newName) + } + + // transform KeySchemaElement for searchable encryption, changing AttributeDefinitions as needed + function method AddBeaconsToKeySchemaElement( + config : ValidConfig, + element : DDB.KeySchemaElement, + attrs : DDB.AttributeDefinitions + ) + : Result<(DDB.KeySchemaElement, DDB.AttributeDefinitions), string> + { + if IsBeacon(config, element.AttributeName) then + var newName :- MakeKeySchemaBeaconName(config, element.AttributeName); + var newAttrs := ReplaceAttrDef(attrs, element.AttributeName, newName); + Success((element.(AttributeName := newName), newAttrs)) + else if IsEncrypted(config, element.AttributeName) then + Failure("You can't make an index on an encrypted attribute, unless you've configured a beacon for that attribute.") + else + Success((element, attrs)) + } + + // transform Projection for searchable encryption + // for any beacon in the Projection, add the beacon name plus any attributes used to construct the beacon + function method AddBeaconsToProjection(config : ValidConfig, proj : DDB.Projection) + : Result + requires config.beacons.Some? + { + if proj.NonKeyAttributes.None? then + Success(proj) + else + var newAttributes := config.beacons.value.GenerateClosure(proj.NonKeyAttributes.value); + if (forall a <- newAttributes :: DDB.IsValid_NonKeyAttributeName(a)) && DDB.IsValid_NonKeyAttributeNameList(newAttributes) then + Success(proj.(NonKeyAttributes := Some(newAttributes))) + else + Failure("Adding beacons to NonKeyAttributes of Projection in CreateGlobalSecondaryIndexAction exceeded the allowed number of projected attributes.") + } + + // transform CreateGlobalSecondaryIndexAction for searchable encryption, changing AttributeDefinitions as needed + function method TransformCreateGSIAction( + config : ValidConfig, + index : DDB.CreateGlobalSecondaryIndexAction, + attrs : DDB.AttributeDefinitions + ) + : Result<(DDB.CreateGlobalSecondaryIndexAction, DDB.AttributeDefinitions), string> + requires config.beacons.Some? + { + var (newKeySchema, attrs) :- AddBeaconsToKeySchema(config, index.KeySchema, attrs); + var newProjection :- AddBeaconsToProjection(config, index.Projection); + Success((index.(KeySchema := newKeySchema, Projection := newProjection), attrs)) + } + + // transform GSI Updates for searchable encryption, changing AttributeDefinitions as needed + function method TransformGlobalSecondaryIndexUpdate( + config : ValidConfig, + index : DDB.GlobalSecondaryIndexUpdate, + attrs : DDB.AttributeDefinitions + ) + : Result<(DDB.GlobalSecondaryIndexUpdate, DDB.AttributeDefinitions), string> + requires config.beacons.Some? + { + if index.Create.None? then + Success((index, attrs)) + else + var (create, attrs) :- TransformCreateGSIAction(config, index.Create.value, attrs); + Success((index.(Create := Some(create)), attrs)) + } + + // transform IndexUpdates for searchable encryption, changing AttributeDefinitions as needed + function method {:tailrecursion} TransformIndexUpdates( + config : ValidConfig, + indexes : DDB.GlobalSecondaryIndexUpdateList, + attrs : DDB.AttributeDefinitions, + acc : DDB.GlobalSecondaryIndexUpdateList := [] + ) + : Result<(DDB.GlobalSecondaryIndexUpdateList, DDB.AttributeDefinitions), string> + requires config.beacons.Some? + { + if |indexes| == 0 then + Success((acc, attrs)) + else + var (newIndex, newAttrs) :- TransformGlobalSecondaryIndexUpdate(config, indexes[0], attrs); + TransformIndexUpdates(config, indexes[1..], newAttrs, acc + [newIndex]) + } + + // transform KeySchema for searchable encryption, changing AttributeDefinitions as needed + function method {:tailrecursion} AddBeaconsToKeySchema( + config : ValidConfig, + schema : seq, + attrs : DDB.AttributeDefinitions, + acc : seq := [], + origSize : nat := |schema| + ) + : (ret : Result<(DDB.KeySchema, DDB.AttributeDefinitions), string>) + requires 1 <= origSize <= 2 + requires |schema| + |acc| == origSize + ensures ret.Success? ==> |ret.value.0| == origSize + { + if |schema| == 0 then + Success((acc, attrs)) + else + var (newSchema, newAttrs) :- AddBeaconsToKeySchemaElement(config, schema[0], attrs); + AddBeaconsToKeySchema(config, schema[1..], newAttrs, acc + [newSchema], origSize) + } + + // transform LSI for searchable encryption, changing AttributeDefinitions as needed + function method TransformOneLsi( + config : ValidConfig, + index : DDB.LocalSecondaryIndex, + attrs : DDB.AttributeDefinitions + ) + : Result<(DDB.LocalSecondaryIndex, DDB.AttributeDefinitions), string> + requires config.beacons.Some? + { + var (newSchema, newAttrs) :- AddBeaconsToKeySchema(config, index.KeySchema, attrs); + var newProjection :- AddBeaconsToProjection(config, index.Projection); + Success((index.(KeySchema := newSchema, Projection := newProjection), newAttrs)) + } + + // transform GSI for searchable encryption, changing AttributeDefinitions as needed + function method TransformOneGsi( + config : ValidConfig, + index : DDB.GlobalSecondaryIndex, + attrs : DDB.AttributeDefinitions + ) + : Result<(DDB.GlobalSecondaryIndex, DDB.AttributeDefinitions), string> + requires config.beacons.Some? + { + var (newSchema, newAttrs) :- AddBeaconsToKeySchema(config, index.KeySchema, attrs); + var newProjection :- AddBeaconsToProjection(config, index.Projection); + Success((index.(KeySchema := newSchema, Projection := newProjection), newAttrs)) + } + + // transform LSIs for searchable encryption, changing AttributeDefinitions as needed + function method LsiWithAttrs( + config : ValidConfig, + indexes : DDB.LocalSecondaryIndexList, + attrs : DDB.AttributeDefinitions, + acc : DDB.LocalSecondaryIndexList := [] + ) + : Result<(DDB.LocalSecondaryIndexList, DDB.AttributeDefinitions), string> + requires config.beacons.Some? + { + if |indexes| == 0 then + Success((acc, attrs)) + else + var (newIndex, newAttrs) :- TransformOneLsi(config, indexes[0], attrs); + LsiWithAttrs(config, indexes[1..], newAttrs, acc + [newIndex]) + } + + // transform GSIs for searchable encryption, changing AttributeDefinitions as needed + function method GsiWithAttrs( + config : ValidConfig, + indexes : DDB.GlobalSecondaryIndexList, + attrs : DDB.AttributeDefinitions, + acc : DDB.GlobalSecondaryIndexList := [] + ) + : Result<(DDB.GlobalSecondaryIndexList, DDB.AttributeDefinitions), string> + requires config.beacons.Some? + { + if |indexes| == 0 then + Success((acc, attrs)) + else + var (newIndex, newAttrs) :- TransformOneGsi(config, indexes[0], attrs); + GsiWithAttrs(config, indexes[1..], newAttrs, acc + [newIndex]) + } + +} \ No newline at end of file diff --git a/DynamoDbItemEncryptor/src/DDBSupport.dfy b/DynamoDbItemEncryptor/src/DDBSupport.dfy index acbecb548..ad39d5e1c 100644 --- a/DynamoDbItemEncryptor/src/DDBSupport.dfy +++ b/DynamoDbItemEncryptor/src/DDBSupport.dfy @@ -14,6 +14,7 @@ include "Util.dfy" include "VirtualDDB.dfy" include "UpdateExpr.dfy" include "FilterExpr.dfy" +include "DDBIndex.dfy" module DynamoDBSupport { @@ -25,26 +26,27 @@ module DynamoDBSupport { import opened DynamoDbItemEncryptorUtil import opened AwsCryptographyDynamoDbItemEncryptorOperations import opened VirtualDDBFields + import opened DynamoDBIndexSupport import UTF8 import SortedSets import Seq - import SE = StructuredEncryptionUtil import Update = DynamoDbUpdateExpr import SET = AwsCryptographyStructuredEncryptionTypes import Filter = DynamoDBFilterExpr + // IsWritable examines an AttributeMap and fails if it is unsuitable for writing. // At the moment, this means that no attribute names starts with "aws_dbe_", // as all other attribute names would need to be configured, and all the // other weird constraints were checked at configuration time. - function method IsWriteable(config : Config, item : DDB.AttributeMap) + function method IsWriteable(config : ValidConfig, item : DDB.AttributeMap) : Result { - if forall k <- item :: !(SE.ReservedPrefix <= k) then + if forall k <- item :: !(ReservedPrefix <= k) then Success(true) else - var bad := set k <- item | SE.ReservedPrefix <= k; - var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, SE.CharLess); + var bad := set k <- item | ReservedPrefix <= k; + var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, CharLess); if |badSeq| == 0 then Failure("") else @@ -52,7 +54,7 @@ module DynamoDBSupport { } function method GetEncryptedAttributes( - config : Config, + config : ValidConfig, expr : Option, attrNames : Option ) : seq @@ -69,7 +71,7 @@ module DynamoDBSupport { // given encryption schema. // Generally this means no encrypted attribute is referenced. function method TestConditionExpression( - config : Config, + config : ValidConfig, expr: Option, attrNames: Option, attrValues: Option @@ -86,13 +88,13 @@ module DynamoDBSupport { Success(true) } - predicate method IsEncrypted(config : Config, attr : string) + predicate method IsEncrypted(config : ValidConfig, attr : string) { && attr in config.attributeActions && config.attributeActions[attr] == SET.ENCRYPT_AND_SIGN } - predicate method IsSigned(config : Config, attr : string) + predicate method IsSigned(config : ValidConfig, attr : string) { && attr in config.attributeActions && config.attributeActions[attr] != SET.DO_NOTHING @@ -102,7 +104,7 @@ module DynamoDBSupport { // given encryption schema. // Generally this means no signed attribute is referenced. function method TestUpdateExpression( - config : Config, + config : ValidConfig, expr: Option, attrNames: Option, attrValues: Option @@ -122,9 +124,8 @@ module DynamoDBSupport { // AddBeacons examines an AttributeMap and modifies it to be appropriate for Searchable Encryption, // returning a replacement AttributeMap. - function method AddBeacons(config : Config, item : DDB.AttributeMap) + function method AddBeacons(config : ValidConfig, item : DDB.AttributeMap) : Result - requires ValidInternalConfig?(config) { if config.beacons.None? then Success(item) @@ -132,50 +133,100 @@ module DynamoDBSupport { var newItems :- config.beacons.value.GenerateBeacons(t => TermToString(t, item), t => TermToBytes(t, item)) .MapFailure(e => "Error generating beacons"); var newAttrs := map k <- newItems :: k := DS(newItems[k]); + var version := DS(VersionPrefix + "1"); Success(item + newAttrs) } // RemoveBeacons examines an AttributeMap and modifies it to be appropriate for customer use, // returning a replacement AttributeMap. - function method RemoveBeacons(config : Config, item : DDB.AttributeMap) + function method RemoveBeacons(config : ValidConfig, item : DDB.AttributeMap) : Result { if config.beacons.None? then Success(item) else - Success(map k <- item | (!(SE.ReservedPrefix <= k)) :: k := item[k]) + Success(map k <- item | (!(ReservedPrefix <= k)) :: k := item[k]) + } + + // transform optional LSIs for searchable encryption, changing AttributeDefinitions as needed + function method LsiOptWithAttrs(config : ValidConfig, schema : Option, attrs : DDB.AttributeDefinitions) + : Result<(Option, DDB.AttributeDefinitions), string> + { + if schema.None? || config.beacons.None? then + Success((schema, [])) + else + var (newSchema, newAttrs) :- LsiWithAttrs(config, schema.value, attrs); + Success((Some(newSchema), newAttrs)) + } + + // transform optional GSIs for searchable encryption, changing AttributeDefinitions as needed + function method GsiOptWithAttrs(config : ValidConfig, schema : Option, attrs : DDB.AttributeDefinitions) + : Result<(Option, DDB.AttributeDefinitions), string> + { + if schema.None? || config.beacons.None? then + Success((schema, [])) + else + var (newSchema, newAttrs) :- GsiWithAttrs(config, schema.value, attrs); + Success((Some(newSchema), newAttrs)) } // Transform a CreateTableInput object for searchable encryption. - function method CreateTableInputForBeacons(config : Config, req : DDB.CreateTableInput) + function method CreateTableInputForBeacons(config : ValidConfig, req : DDB.CreateTableInput) : Result { - Success(req) + if config.beacons.None? then + Success(req) + else + var (newSchema, newAttrs) :- AddBeaconsToKeySchema(config, req.KeySchema, req.AttributeDefinitions); + var (newLsi, newAttrs) :- LsiOptWithAttrs(config, req.LocalSecondaryIndexes, newAttrs); + var (newGsi, newAttrs) :- GsiOptWithAttrs(config, req.GlobalSecondaryIndexes, newAttrs); + Success(req.( + KeySchema := newSchema, + AttributeDefinitions := newAttrs, + LocalSecondaryIndexes := newLsi, + GlobalSecondaryIndexes := newGsi + )) } // Transform a UpdateTableInput object for searchable encryption. - function method UpdateTableInputForBeacons(config : Config, req : DDB.UpdateTableInput) + function method UpdateTableInputForBeacons(config : ValidConfig, req : DDB.UpdateTableInput) : Result { - Success(req) + if config.beacons.None? || req.GlobalSecondaryIndexUpdates.None? then + Success(req) + else + var (indexes, attrs) :- TransformIndexUpdates(config, req.GlobalSecondaryIndexUpdates.value, req.AttributeDefinitions.UnwrapOr([])); + var newAttrs := if |attrs| == 0 then None else Some(attrs); + Success(req.(GlobalSecondaryIndexUpdates := Some(indexes), AttributeDefinitions := newAttrs)) } // Transform a DescribeTableOutput object for searchable encryption. - function method DescribeTableOutputForBeacons(config : Config, req : DDB.DescribeTableOutput) + function method DescribeTableOutputForBeacons(config : ValidConfig, req : DDB.DescribeTableOutput) : Result { - Success(req) + if config.beacons.None? || req.Table.None? then + Success(req) + else + var locals :- TransformLocalIndexDescription(config, req.Table.value.LocalSecondaryIndexes); + var globals :- TransformGlobalIndexDescription(config, req.Table.value.GlobalSecondaryIndexes); + Success( + DDB.DescribeTableOutput( + Table := Some( + req.Table.value.(LocalSecondaryIndexes := locals, GlobalSecondaryIndexes := globals) + ) + ) + ) } // Transform a QueryInput object for searchable encryption. - function method QueryInputForBeacons(config : Config, req : DDB.QueryInput) + function method QueryInputForBeacons(config : ValidConfig, req : DDB.QueryInput) : Result { Success(req) } // Transform a QueryOutput object for searchable encryption. - function method QueryOutputForBeacons(config : Config, req : DDB.QueryInput, resp : DDB.QueryOutput) + function method QueryOutputForBeacons(config : ValidConfig, req : DDB.QueryInput, resp : DDB.QueryOutput) : (ret : Result) requires resp.Items.Some? ensures ret.Success? ==> @@ -186,14 +237,14 @@ module DynamoDBSupport { } // Transform a ScanInput object for searchable encryption. - function method ScanInputForBeacons(config : Config, req : DDB.ScanInput) + function method ScanInputForBeacons(config : ValidConfig, req : DDB.ScanInput) : Result { Success(req) } // Transform a ScanOutput object for searchable encryption. - function method ScanOutputForBeacons(config : Config, req : DDB.ScanInput, resp : DDB.ScanOutput) + function method ScanOutputForBeacons(config : ValidConfig, req : DDB.ScanInput, resp : DDB.ScanOutput) : (ret : Result) requires resp.Items.Some? ensures ret.Success? ==> diff --git a/DynamoDbItemEncryptor/src/DynamoToStruct.dfy b/DynamoDbItemEncryptor/src/DynamoToStruct.dfy index 2a118301e..8426046e1 100644 --- a/DynamoDbItemEncryptor/src/DynamoToStruct.dfy +++ b/DynamoDbItemEncryptor/src/DynamoToStruct.dfy @@ -11,16 +11,14 @@ module DynamoToStruct { import opened StandardLibrary import opened StandardLibrary.UInt import AwsCryptographyDynamoDbItemEncryptorTypes - import Util = StructuredEncryptionUtil import UTF8 import SortedSets import Seq - import SE = StructuredEncryptionUtil type Error = AwsCryptographyDynamoDbItemEncryptorTypes.Error - type TerminalDataMap = map - + type StructuredDataTerminalType = x : StructuredData | x.content.Terminal? witness * + type TerminalDataMap = map /* TODO - prove the following StructuredToItem(ItemToStructured(itemMap)) == itemMap @@ -244,7 +242,7 @@ module DynamoToStruct { const NULL : TerminalTypeId := [TERM_T, NULL_T]; const STRING : TerminalTypeId := [TERM_T, STRING_T]; const NUMBER : TerminalTypeId := [TERM_T, NUMBER_T]; - const BINARY : TerminalTypeId := SE.BYTES_TYPE_ID; + const BINARY : TerminalTypeId := [0xFF, 0xFF]; const BOOLEAN : TerminalTypeId := [TERM_T, BOOLEAN_T]; const STRING_SET : TerminalTypeId := [SET_T, STRING_T]; const NUMBER_SET : TerminalTypeId := [SET_T, NUMBER_T]; diff --git a/DynamoDbItemEncryptor/src/Index.dfy b/DynamoDbItemEncryptor/src/Index.dfy index acad4742a..ca9be5a68 100644 --- a/DynamoDbItemEncryptor/src/Index.dfy +++ b/DynamoDbItemEncryptor/src/Index.dfy @@ -2,16 +2,17 @@ // SPDX-License-Identifier: Apache-2.0 include "AwsCryptographyDynamoDbItemEncryptorOperations.dfy" +include "Util.dfy" module {:extern "Dafny.Aws.Cryptography.DynamoDbItemEncryptor" } DynamoDbItemEncryptor refines AbstractAwsCryptographyDynamoDbItemEncryptorService { + import opened DynamoDbItemEncryptorUtil import StructuredEncryption import CSE = AwsCryptographyStructuredEncryptionTypes import MaterialProviders import Operations = AwsCryptographyDynamoDbItemEncryptorOperations - import SE = StructuredEncryptionUtil // TODO there is no sensible default, so what should this do? // As is, the default config is invalid. Can we update the codegen to *not* @@ -31,10 +32,10 @@ module ) } - // because an inline "!(SE.ReservedPrefix <= attr)" is too hard for Dafny + // because an inline "!(ReservedPrefix <= attr)" is too hard for Dafny predicate method UnreservedPrefix(attr : string) { - !(SE.ReservedPrefix <= attr) + !(ReservedPrefix <= attr) } method DynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig) diff --git a/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbItemEncryptor/src/Util.dfy index a8105a9c3..03f5304f9 100644 --- a/DynamoDbItemEncryptor/src/Util.dfy +++ b/DynamoDbItemEncryptor/src/Util.dfy @@ -5,9 +5,27 @@ include "../Model/AwsCryptographyDynamoDbItemEncryptorTypes.dfy" module DynamoDbItemEncryptorUtil { import opened AwsCryptographyDynamoDbItemEncryptorTypes - + import opened Wrappers + import opened StandardLibrary + import opened StandardLibrary.UInt + + const ReservedPrefix := "aws_dbe_" + const BeaconPrefix := ReservedPrefix + "b_" + const VersionPrefix := ReservedPrefix + "v_" + function method E(msg : string) : Error { DynamoDbItemEncryptorException(message := msg) } + + predicate method ByteLess(x : uint8, y : uint8) + { + x < y + } + + predicate method CharLess(x : char, y : char) + { + x < y + } + } diff --git a/StructuredEncryption/src/Beacon.dfy b/StructuredEncryption/src/Beacon.dfy index 10be10c2c..548126bd7 100644 --- a/StructuredEncryption/src/Beacon.dfy +++ b/StructuredEncryption/src/Beacon.dfy @@ -147,6 +147,12 @@ module BaseBeacon { hash(bytes) } + // TODO virtual fields + function method GetFields() : seq + { + [loc.parts[0].key] + } + //= specification/searchable-encryption/beacons.md#getpart-for-a-standard-beacon //= type=implication diff --git a/StructuredEncryption/src/CompoundBeacon.dfy b/StructuredEncryption/src/CompoundBeacon.dfy index 5bef25761..fceeafc8e 100644 --- a/StructuredEncryption/src/CompoundBeacon.dfy +++ b/StructuredEncryption/src/CompoundBeacon.dfy @@ -41,7 +41,14 @@ module CompoundBeacon { loc : TerminalLocation, prefix : Prefix, length : Option - ) + ) { + + // TODO virtual fields + function method GetFields() : seq + { + [loc.parts[0].key] + } + } datatype ConstructorPart = ConstructorPart ( name : string, @@ -71,6 +78,11 @@ module CompoundBeacon { Success(part[0]) } + function method GetFields() : seq + { + Seq.Flatten(Seq.Map((p : BeaconPart) => p.GetFields(), parts)) + } + function method {:opaque} {:tailrecursion} TryConstructor(consFields : seq, stringify : Stringify, acc : string := "") : (ret : Result) ensures ret.Success? ==> |ret.value| > 0 diff --git a/StructuredEncryption/src/SearchInfo.dfy b/StructuredEncryption/src/SearchInfo.dfy index 21994ec97..2ba14c20d 100644 --- a/StructuredEncryption/src/SearchInfo.dfy +++ b/StructuredEncryption/src/SearchInfo.dfy @@ -51,6 +51,12 @@ module SearchableEncryptionInfo { versions[currWrite].IsVirtualField(field) } + function method GenerateClosure(fields : seq) : seq + requires ValidState() + { + versions[currWrite].GenerateClosure(fields) + } + function method GenerateBeacons(stringify : Stringify, byteify : Byteify) : Result, Error> requires ValidState() { @@ -76,6 +82,13 @@ module SearchableEncryptionInfo { else cmp.base.name } + function method GetFields() : seq + { + if Standard? then + std.GetFields() + else + cmp.GetFields() + } } type BeaconMap = map @@ -104,6 +117,21 @@ module SearchableEncryptionInfo { field in virtualFields } + function method GetFields(field : string) : seq + { + if IsBeacon(field) then + beacons[field].GetFields() + ["aws_dbe_b_" + field] + else + [field] + } + + function method GenerateClosure(fields : seq) : seq + { + var fieldLists := Seq.Map((s : string) => GetFields(s), fields); + var fieldSet := set f <- fieldLists, g <- f :: g; + SortedSets.ComputeSetToOrderedSequence2(fieldSet, CharLess) + } + // TerminalLocation to string via virtual field, if any function method GetVirtualLocationString(loc : TerminalLocation, stringify : Stringify) : Option { @@ -157,9 +185,10 @@ module SearchableEncryptionInfo { // Generate all possible beacons function method GenerateBeacons(stringify : Stringify, byteify : Byteify) : Result, Error> { + var versionMap := map["aws_dbe_v1" := " "]; var result := map k <- beacons :: k := beacons[k].hash(t => VirtualStringify(t, stringify), t => VirtualByteify(t, stringify, byteify)); - Success(map k <- result | result[k].Success? :: k := result[k].value) + Success((map k <- result | result[k].Success? :: k := result[k].value) + versionMap) } } -} \ No newline at end of file +}