diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index 383fd6ead..c3e33b3ae 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy @@ -22,6 +22,9 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" // Begin Generated Types + datatype AsSet = | AsSet ( + + ) type AttributeActions = map type BeaconBitLength = x: int32 | IsValid_BeaconBitLength(x) witness * predicate method IsValid_BeaconBitLength(x: int32) { @@ -30,6 +33,11 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" datatype BeaconKeySource = | single(single: SingleKeyStore) | multi(multi: MultiKeyStore) + datatype BeaconStyle = + | partOnly(partOnly: PartOnly) + | twinned(twinned: Twinned) + | asSet(asSet: AsSet) + | twinnedSet(twinnedSet: TwinnedSet) datatype BeaconVersion = | BeaconVersion ( nameonly version: VersionNumber , nameonly keyStore: AwsCryptographyKeyStoreTypes.IKeyStoreClient , @@ -310,6 +318,9 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" nameonly keyFieldName: string , nameonly cacheTTL: int32 , nameonly cache: Option + ) + datatype PartOnly = | PartOnly ( + ) datatype PlaintextOverride = | FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ @@ -339,7 +350,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" datatype StandardBeacon = | StandardBeacon ( nameonly name: string , nameonly length: BeaconBitLength , - nameonly loc: Option + nameonly loc: Option , + nameonly style: Option ) type StandardBeaconList = x: seq | IsValid_StandardBeaconList(x) witness * predicate method IsValid_StandardBeaconList(x: seq) { @@ -349,6 +361,12 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" predicate method IsValid_TerminalLocation(x: string) { ( 1 <= |x| ) } + datatype Twinned = | Twinned ( + nameonly other: string + ) + datatype TwinnedSet = | TwinnedSet ( + nameonly other: string + ) datatype Upper = | Upper ( ) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy index fe7cc927e..43a48f726 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy @@ -465,6 +465,60 @@ union VirtualTransform { segments : GetSegments } +//= specification/searchable-encryption/beacons.md#partonly-initialization +//= type=implication +//# On initialization of a PartOnly, the caller MUST NOT provide any +//# additional parameters to the PartOnly. +@javadoc("Attribute must be used as part of a Compound Beacon, never alone.") +structure PartOnly {} + +//= specification/searchable-encryption/beacons.md#asset-initialization +//= type=implication +//# On initialization of as AsSet, the caller MUST NOT provide any +//# additional parameters to the AsSet. +@javadoc("Attribute must be a Set. Beacon value will also be a Set.") +structure AsSet {} + +//= specification/searchable-encryption/beacons.md#twinned-initialization +//= type=implication +//# On initialization of a Twinned, the caller MUST provide: +//# +//# * other : a beacon name +@javadoc("This beacon should calculate values like another beacon, so they can be compared.") +structure Twinned { + @required + @javadoc("Calculate beacon values as for this beacon.") + other : String, +} + +//= specification/searchable-encryption/beacons.md#twinnedset-initialization +//= type=implication +//# On initialization of a TwinnedSet, the caller MUST provide: +//# +//# * other : a beacon name +@javadoc("Both Twinned and AsSet.") +structure TwinnedSet { + @required + @javadoc("Calculate beacon values as for this beacon.") + other : String, +} + +//= specification/searchable-encryption/beacons.md#beacon-style-initialization +//= type=implication +//# On initialization of a Beacon Style, the caller MUST provide exactly one of +//# +//# * a [PartOnly](#partonly-initialization) +//# * a [Twinned](#twinned-initialization) +//# * an [AsSet](#asset-initialization) +//# * a [TwinnedSet](#twinnedset-initialization) + +union BeaconStyle { + partOnly: PartOnly, + twinned: Twinned, + asSet: AsSet, + twinnedSet: TwinnedSet, +} + //= specification/searchable-encryption/beacons.md#encrypted-part-initialization //= type=implication //# On initialization of a [encrypted part](#encrypted-part-initialization), the caller MUST provide: @@ -552,7 +606,9 @@ structure StandardBeacon { @javadoc("The length of the calculated beacon.") length : BeaconBitLength, @javadoc("The DynamoDB document path to the value this beacon will calculate over. If not specified, the beacon will calculate values for the attribute with the name specified in 'name'.") - loc : TerminalLocation + loc : TerminalLocation, + @javadoc("Optional augmented behavior.") + style : BeaconStyle, } //= specification/searchable-encryption/beacons.md#compound-beacon-initialization diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy index 1f1e55743..5613bfd90 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy @@ -14,13 +14,13 @@ module BaseBeacon { import opened HexStrings import opened DynamoDbEncryptionUtil import opened DdbVirtualFields + import opened Seq import DynamoToStruct import DDB = ComAmazonawsDynamodbTypes import Prim = AwsCryptographyPrimitivesTypes import Aws.Cryptography.Primitives import UTF8 - import Seq import SortedSets import TermLoc @@ -108,7 +108,10 @@ module BaseBeacon { client: Primitives.AtomicPrimitivesClient, name: string, length : BeaconLength, - loc : string + loc : string, + partOnly : bool, + asSet : bool, + twin : Option ) : (ret : Result) ensures ret.Success? ==> @@ -125,13 +128,19 @@ module BaseBeacon { beaconName := beaconName ), length, - termLoc + termLoc, + partOnly, + asSet, + twin )) } datatype StandardBeacon = StandardBeacon ( base : BeaconBase, length : BeaconLength, - loc : TermLoc.TermLoc + loc : TermLoc.TermLoc, + partOnly : bool, + asSet : bool, + twin : Option ) { function method {:opaque} hash(val : Bytes, key : Bytes) : (ret : Result) @@ -145,6 +154,17 @@ module BaseBeacon { base.hash(val, key, length) } + // return the name of the hmac key to use + //= specification/searchable-encryption/beacons.md#twinned-initialization + //# This beacon MUST calculate its [value](#beacon-value) as if it were the `other` beacon. + function method keyName() : string + { + if twin.Some? then + twin.value + else + base.name + } + // Get the standard hash for the UTF8 encoded representation of this string. //= specification/searchable-encryption/beacons.md#string-hash //= type=implication @@ -159,47 +179,107 @@ module BaseBeacon { //# of the input string, the HMAC key from the [key materials](./search-config.md#get-beacon-key-materials) //# associated with this beacon, and the beacon length associated with this beacon. ensures res.Success? ==> - && base.name in keys + && keyName() in keys && UTF8.Encode(val).Success? && var str := UTF8.Encode(val).value; - && hash(str, keys[base.name]).Success? - && res.value == hash(str, keys[base.name]).value + && hash(str, keys[keyName()]).Success? + && res.value == hash(str, keys[keyName()]).value { - :- Need(base.name in keys, E("Internal Error, no key for " + base.name)); + :- Need(keyName() in keys, E("Internal Error, no key for " + keyName())); var str := UTF8.Encode(val); if str.Failure? then Failure(E(str.error)) else - hash(str.value, keys[base.name]) + hash(str.value, keys[keyName()]) + } + + function method {:opaque} ValueToSet(value : DDB.AttributeValue, key : Bytes) : (ret : Result) + requires asSet + ensures ret.Success? ==> ret.value.SS? + ensures !value.SS? && !value.NS? && !value.BS? ==> ret.Failure? + ensures ret.Success? ==> HasNoDuplicates(ret.value.SS) + { + reveal HasNoDuplicates(); + assert HasNoDuplicates([]); + var beaconSeq :- match value { + case SS(n) => BeaconizeStringSet(n, key) + case NS(n) => BeaconizeNumberSet(n, key) + case BS(n) => BeaconizeBinarySet(n, key) + case _ => Failure(E("Beacon " + base.name + " has style AsSet, but attribute has type " + AttrTypeToStr(value) + ".")) + }; + Success(DDB.AttributeValue.SS(beaconSeq)) } //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon //= type=implication - //# * This operation MUST take an [hmac key](./search-config.md#hmac-key-generation), a record as input, and produce an optional string. - function method {:opaque} getHash(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes) : (ret : Result, Error>) - ensures ret.Success? ==> - && VirtToBytes(loc, item, vf).Success? - //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon - //= type=implication - //# * This operation MUST convert the attribute value of the associated field to - //# a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md). - && var bytes := VirtToBytes(loc, item, vf).value; - //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon - //= type=implication - //# * This operation MUST return no value if the associated field does not exist in the record - && (bytes.None? ==> ret.value.None?) - //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon - //= type=implication - //# * This operation MUST return the [basicHash](#basichash) of the input and the configured [beacon length](#beacon-length). - && (bytes.Some? ==> ret.value.Some? && hash(bytes.value, key).Success? && ret.value.value == hash(bytes.value, key).value) - && (bytes.Some? ==> ret.value.Some? && base.hash(bytes.value, key, length).Success? && ret.value.value == base.hash(bytes.value, key, length).value) + //# * This operation MUST take an [hmac key](./search-config.md#hmac-key-generation), a record as input, and produce an optional [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html). + function method {:opaque} getHash(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes) : (ret : Result, Error>) + //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon + //= type=implication + //# * If this beacon is marked AsSet then this operation MUST return the + //# [set value](#value-for-a-set-standard-beacon), + //# otherwise it MUST return the [non-set value](#value-for-a-non-set-standard-beacon) + ensures asSet ==> ret == getHashSet(item, key) + ensures !asSet ==> ret == getHashNonSet(item, vf, key) { - var bytes :- VirtToBytes(loc, item, vf); - if bytes.None? then - Success(None) + if asSet then + getHashSet(item, key) else - var res :- hash(bytes.value, key); - Success(Some(res)) + getHashNonSet(item, vf, key) + } + + function method {:opaque} getHashSet(item : DDB.AttributeMap, key : Bytes) : (ret : Result, Error>) + requires asSet + ensures ret.Success? ==> + //= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon + //= type=implication + //# * The returned + //# [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html) + //# MUST be type "SS" StringSet. + && (ret.value.Some? ==> ret.value.value.SS?) + //= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon + //= type=implication + //# * The resulting set MUST NOT contain duplicates. + && (ret.value.Some? ==> HasNoDuplicates(ret.value.value.SS)) + { + var value := TermLoc.TermToAttr(loc, item, None); + if value.None? then + Success(None) + else + var setValue :- ValueToSet(value.value, key); + Success(Some(setValue)) + } + function method {:opaque} getHashNonSet(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes) : (ret : Result, Error>) + requires !asSet + ensures ret.Success? ==> + //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon + //= type=implication + //# * The returned + //# [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html) + //# MUST be type "S" String. + && (ret.value.Some? ==> ret.value.value.S?) + && VirtToBytes(loc, item, vf).Success? + && var bytes := VirtToBytes(loc, item, vf).value; + //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon + //= type=implication + //# * This operation MUST return no value if the associated field does not exist in the record + && (bytes.None? ==> ret.value.None?) + //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon + //= type=implication + //# * This operation MUST convert the attribute value of the associated field to + //# a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md). + && (bytes.Some? ==> ret.value.Some? && hash(bytes.value, key).Success? && ret.value.value == DDB.AttributeValue.S(hash(bytes.value, key).value)) + //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon + //= type=implication + //# * This operation MUST return the [basicHash](#basichash) of the resulting bytes and the configured [beacon length](#beacon-length). + && (bytes.Some? ==> ret.value.Some? && base.hash(bytes.value, key, length).Success? && ret.value.value == DDB.AttributeValue.S(base.hash(bytes.value, key, length).value)) + { + var bytes :- VirtToBytes(loc, item, vf); + if bytes.None? then + Success(None) + else + var res :- hash(bytes.value, key); + Success(Some(DDB.AttributeValue.S(res))) } function method {:opaque} getNaked(item : DDB.AttributeMap, vf : VirtualFieldMap) : Result, Error> @@ -215,11 +295,74 @@ module BaseBeacon { [loc[0].key] } - function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes) : Result + function method {:tailrecursion} BeaconizeStringSet(value : DDB.StringSetAttributeValue, key : Bytes, converted : seq := []) + : (ret : Result, Error>) + requires HasNoDuplicates(converted) + ensures ret.Success? ==> HasNoDuplicates(ret.value) { - var bytes :- DynamoToStruct.TopLevelAttributeToBytes(value).MapFailure(e => E(e)); - var h :- hash(bytes, key); - Success(DDB.AttributeValue.S(h)) + if |value| == 0 then + Success(converted) + else + var bytes :- DynamoToStruct.TopLevelAttributeToBytes(DDB.AttributeValue.S(value[0])).MapFailure(e => E(e)); + var h :- hash(bytes, key); + if h in converted then + BeaconizeStringSet(value[1..], key, converted) + else + reveal HasNoDuplicates(); + BeaconizeStringSet(value[1..], key, converted + [h]) + } + + function method {:tailrecursion} BeaconizeNumberSet(value : DDB.NumberSetAttributeValue, key : Bytes, converted : seq := []) + : (ret : Result, Error>) + requires HasNoDuplicates(converted) + ensures ret.Success? ==> HasNoDuplicates(ret.value) + { + if |value| == 0 then + Success(converted) + else + var bytes :- DynamoToStruct.TopLevelAttributeToBytes(DDB.AttributeValue.N(value[0])).MapFailure(e => E(e)); + var h :- hash(bytes, key); + if h in converted then + BeaconizeNumberSet(value[1..], key, converted) + else + reveal HasNoDuplicates(); + BeaconizeNumberSet(value[1..], key, converted + [h]) + } + + function method {:tailrecursion} BeaconizeBinarySet(value : DDB.BinarySetAttributeValue, key : Bytes, converted : seq := []) + : (ret : Result, Error>) + requires HasNoDuplicates(converted) + ensures ret.Success? ==> HasNoDuplicates(ret.value) + { + if |value| == 0 then + Success(converted) + else + var bytes :- DynamoToStruct.TopLevelAttributeToBytes(DDB.AttributeValue.B(value[0])).MapFailure(e => E(e)); + var h :- hash(bytes, key); + if h in converted then + BeaconizeBinarySet(value[1..], key, converted) + else + reveal HasNoDuplicates(); + BeaconizeBinarySet(value[1..], key, converted + [h]) + } + + function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes) + : (ret : Result) + //= specification/searchable-encryption/beacons.md#asset-initialization + //= type=implication + //# * Writing an item MUST fail if the item contains this beacon's attribute, + //# and that attribute is not of type Set. + ensures asSet && !value.SS? && !value.NS? && !value.BS? ==> ret.Failure? + { + //= specification/searchable-encryption/beacons.md#asset-initialization + //# * The Standard Beacon MUST be stored in the item as a Set, + //# comprised of the [beacon values](#beacon-value) of all the elements in the original Set. + if asSet then + ValueToSet(value, key) + else + var bytes :- DynamoToStruct.TopLevelAttributeToBytes(value).MapFailure(e => E(e)); + var h :- hash(bytes, key); + Success(DDB.AttributeValue.S(h)) } //= specification/searchable-encryption/beacons.md#getpart-for-a-standard-beacon diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy index 6045f22db..541232f5e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy @@ -140,6 +140,23 @@ module CompoundBeacon { :: OkPrefixPair(x, y) } + // Does these parts refer to `name` + predicate method {:tailrecursion} HasBeacon2(parts : seq, name : string) + { + if |parts| == 0 then + false + else if parts[0].getName() == name then + true + else + HasBeacon2(parts[1..], name) + } + + // Does this compound beacon refer to `name` + predicate method HasBeacon(name : string) + { + HasBeacon2(parts, name) + } + // Does this beacon have any encrypted parts predicate method isEncrypted() { numSigned < |parts| diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index c4100927a..4e475b014 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -22,6 +22,7 @@ module SearchConfigToInfo { import opened StandardLibrary.UInt import opened DynamoDbEncryptionUtil import opened TermLoc + import opened StandardLibrary.String import MaterialProviders import SortedSets @@ -385,6 +386,26 @@ module SearchConfigToInfo { Some(badSeq[0]) } + function method IsValidTwin(converted : I.BeaconMap, name : string, length : B.BeaconLength, twin : string) + : (ret : Result) + ensures ret.Success? ==> + && twin in converted + && converted[twin].Standard? + && converted[twin].std.length == length + { + if twin in converted then + if converted[twin].Standard? then + if converted[twin].std.length == length then + Success(true) + else + Failure(E("Beacon " + name + " is twinned to " + twin + " but " + name + " has length " + Base10Int2String(length as int) + + " and " + twin + " has length " + Base10Int2String(converted[twin].std.length as int) + ".")) + else + Failure(E("Beacon " + name + " is twinned to " + twin + " but " + twin + " is a compound beacon.")) + else + Failure(E("Beacon " + name + " is twinned to " + twin + " which is not defined.")) + } + // convert configured StandardBeacons to internal Beacons method {:tailrecursion} AddStandardBeacons( beacons : seq, @@ -435,7 +456,22 @@ module SearchConfigToInfo { :- Need(beacons[0].name !in converted, E("Duplicate StandardBeacon name : " + beacons[0].name)); var _ :- BeaconNameAllowed(outer, virtualFields, beacons[0].name, "StandardBeacon"); var locString := GetLocStr(beacons[0].name, beacons[0].loc); - var newBeacon :- B.MakeStandardBeacon(client, beacons[0].name, beacons[0].length as B.BeaconLength, locString); + var isPartOnly := false; + var isAsSet := false; + var twin : Option := None; + if beacons[0].style.Some? { + match beacons[0].style.value { + case partOnly(t) => isPartOnly := true; + case twinned(t) => twin := Some(t.other); + case asSet(t) => isAsSet := true; + //= specification/searchable-encryption/beacons.md#twinnedset-initialization + //# A TwinnedSet Beacon MUST behave both as [Twinned](#twinned-initialization) and [AsSet](#asset-initialization). + case twinnedSet(t) => twin := Some(t.other); isAsSet := true; + } + + } + var newBeacon :- B.MakeStandardBeacon(client, beacons[0].name, beacons[0].length as B.BeaconLength, locString, + isPartOnly, isAsSet, twin); //= specification/searchable-encryption/search-config.md#beacon-version-initialization //# Initialization MUST fail if the [terminal location](virtual.md#terminal-location) @@ -529,7 +565,8 @@ module SearchConfigToInfo { ghost origSize : nat, ghost numSigned : nat, converted : seq, - std : I.BeaconMap + std : I.BeaconMap, + name : string ) : (ret : Result, Error>) requires origSize == |parts| + |converted| @@ -541,15 +578,22 @@ module SearchConfigToInfo { //# The name MUST be the name of a configured standard beacon. ensures ret.Success? && 0 < |parts| ==> parts[0].name in std && std[parts[0].name].Standard? ensures ret.Success? ==> CB.OrderedParts(ret.value, numSigned) + + //= specification/searchable-encryption/beacons.md#asset-initialization + //= type=implication + //# * initialization MUST fail if any compound beacon has an AsSet beacon as a part. + ensures |parts| != 0 && parts[0].name in std && std[parts[0].name].Standard? && std[parts[0].name].std.asSet ==> ret.Failure? { if |parts| == 0 then Success(converted) else - if parts[0].name in std && std[parts[0].name].Standard? then + if parts[0].name in std && std[parts[0].name].Standard? && std[parts[0].name].std.asSet then + Failure(E("Compound beacon " + name + " uses " + parts[0].name + " which is an AsSet beacon, and therefore cannot be used in a Compound Beacon.")) + else if parts[0].name in std && std[parts[0].name].Standard? then var newPart := CB.Encrypted(parts[0].prefix, std[parts[0].name].std); - AddEncryptedParts(parts[1..], origSize, numSigned, converted + [newPart], std) + AddEncryptedParts(parts[1..], origSize, numSigned, converted + [newPart], std, name) else - Failure(E("Encrypted part needs standard beacon " + parts[0].name + " which is not configured.")) + Failure(E("Compound beacon " + name + " refers to standard beacon " + parts[0].name + " which is not configured.")) } // create the default constructor, if not constructor is specified @@ -741,7 +785,7 @@ module SearchConfigToInfo { var numNon := |parts|; assert CB.OrderedParts(parts, numNon); - var parts :- AddEncryptedParts(encrypted, |parts| + |encrypted|, numNon, parts, converted); + var parts :- AddEncryptedParts(encrypted, |parts| + |encrypted|, numNon, parts, converted, beacon.name); assert CB.OrderedParts(parts, numNon); :- Need(0 < |parts|, E("For beacon " + beacon.name + " no parts were supplied.")); :- Need(beacon.constructors.None? || 0 < |beacon.constructors.value|, E("For beacon " + beacon.name + " an empty constructor list was supplied.")); @@ -800,6 +844,63 @@ module SearchConfigToInfo { output := AddCompoundBeacons(beacons[1..], outer, client, virtualFields, converted[beacons[0].name := I.Compound(newBeacon)]); } + // Is `name` referred to by some compound beacon in `data` + predicate method ExistsInCompound(names : seq, name : string, data : I.BeaconMap) + requires forall x <- names :: x in data + { + if |names| == 0 then + false + else + var b := data[names[0]]; + if b.Compound? && b.cmp.HasBeacon(name) then + true + else + ExistsInCompound(names[1..], name, data) + } + + // Are all beacons internally consistent? + // Are all PartOnly beacons referred to by some compound beacon? + function method CheckAllBeacons(names : seq, allNames : seq, data : I.BeaconMap) : (ret : Result) + requires forall x <- names :: x in data + requires forall x <- allNames :: x in data + + //= specification/searchable-encryption/beacons.md#partonly-initialization + //= type=implication + //# Initialization MUST fail if the configuration does not use a PartOnly in a [compound beacon](#compound-beacon). + ensures |names| != 0 && I.IsPartOnly(data[names[0]]) && !ExistsInCompound(allNames, names[0], data) ==> ret.Failure? + + ensures ret.Success? && 0 < |names| && data[names[0]].Standard? && data[names[0]].std.twin.Some? ==> + && var twin := data[names[0]].std.twin.value; + && IsValidTwin(data, names[0], data[names[0]].std.length, twin).Success? + //= specification/searchable-encryption/beacons.md#twinned-initialization + //= type=implication + //# This name MUST be the name of a previously defined Standard Beacon. + && twin in data + && data[twin].Standard? + //= specification/searchable-encryption/beacons.md#twinned-initialization + //= type=implication + //# This beacon's [length](#beacon-length) MUST be equal to the `other` beacon's [length](#beacon-length). + && data[twin].std.length == data[names[0]].std.length + { + if |names| == 0 then + Success(true) + else + var b := data[names[0]]; + if I.IsPartOnly(b) && !ExistsInCompound(allNames, names[0], data) then + Failure(E("PartOnly beacon " + names[0] + " MUST be used in a compound beacon.")) + else if b.Standard? && b.std.twin.Some? then + IsValidTwin(data, names[0], b.std.length, b.std.twin.value) + else + CheckAllBeacons(names[1..], allNames, data) + } + + // Are all beacons internally consistent? + function method CheckBeacons(data : I.BeaconMap) : Result + { + var beaconNames := SortedSets.ComputeSetToOrderedSequence2(data.Keys, CharLess); + CheckAllBeacons(beaconNames, beaconNames, data) + } + // convert configured Beacons to internal BeaconMap method ConvertBeacons( outer : DynamoDbTableEncryptionConfig, @@ -818,5 +919,8 @@ module SearchConfigToInfo { } else { output := Success(std); } + if output.Success? { + var _ :- CheckBeacons(output.value); + } } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 8d281ed69..41fb54d4b 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -1088,17 +1088,17 @@ module DynamoToStruct { set k <- m | m[k].Failure? :: m[k].error } - lemma OneBadResult(m : map>) - requires ! forall v <- m.Values :: v.Success? - ensures exists v <- m.Values :: v.Failure? + lemma OneBadResult(m : map>) + requires ! forall k <- m :: m[k].Success? + ensures exists k <- m :: m[k].Failure? ensures |FlattenErrors(m)| > 0 { - assert exists v <- m.Values :: v.Failure?; + assert exists k <- m :: m[k].Failure?; var errors := FlattenErrors(m); - assert exists v :: v in m.Values && v.Failure? && (v.error in errors); + assert exists k :: k in m && m[k].Failure? && (m[k].error in errors); } - lemma MapKeysMatchItems(m : map) + lemma MapKeysMatchItems(m : map) ensures forall k :: k in m.Keys ==> (k, m[k]) in m.Items {} @@ -1111,7 +1111,7 @@ module DynamoToStruct { assert exists v :: v in bad && !f(v) && (v in bad); } - lemma SimplifyMapValueSuccess(m : map>) + lemma SimplifyMapValueSuccess(m : map>) ensures SimplifyMapValue(m).Success? <==> forall k <- m :: m[k].Success? ensures SimplifyMapValue(m).Success? ==> forall kv <- m.Items :: kv.1.Success? ensures SimplifyMapValue(m).Failure? <==> exists k : X | k in m.Keys :: m[k].Failure? diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy index 409444701..a26051f3c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy @@ -175,12 +175,21 @@ module DynamoDBFilterExpr { } function method GetBeacon2(b : SI.BeaconVersion, t : Token, names : Option) - : Result + : (ret : Result) requires HasBeacon(b, t, names) + //= specification/searchable-encryption/beacons.md#partonly-initialization + //= type=implication + //# A query MUST fail if it tries to search on a PartOnly beacon directly. + ensures + var name := RealName(t.s); + name in b.beacons && SI.IsPartOnly(b.beacons[name]) ==> ret.Failure? { var name := RealName(t.s); if name in b.beacons then - Success(b.beacons[name]) + if SI.IsPartOnly(b.beacons[name]) then + Failure(E("Field " + name + " is encrypted, and has a PartOnly beacon, and so can only be used as part of a compound beacon.")) + else + Success(b.beacons[name]) else if names.Some? && name in names.value && RealName(names.value[name]) in b.beacons then var name2 := RealName(names.value[name]); Success(b.beacons[name2]) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy index 2032154a5..c3ad7d649 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy @@ -384,7 +384,7 @@ module SearchableEncryptionInfo { cmp.isEncrypted() } function method hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap) - : (ret : Result, Error>) + : (ret : Result, Error>) requires !keys.DontUseKeys? //= specification/searchable-encryption/search-config.md#get-beacon-key-for-query @@ -394,13 +394,17 @@ module SearchableEncryptionInfo { ensures Standard? && keys.ShouldHaveKeys? ==> ret.Failure? { if Standard? then - :- Need(keys.Keys?, E("Need key for beacon " + std.base.name + " but no keyId found in query.")); - if std.base.name in keys.value then - std.getHash(item, vf, keys.value[std.base.name]) + :- Need(keys.Keys?, E("Need key for beacon " + std.keyName() + " but no keyId found in query.")); + if std.keyName() in keys.value then + std.getHash(item, vf, keys.value[std.keyName()]) else - Failure(E("Internal error. Beacon " + std.base.name + " has no key.")) + Failure(E("Internal error. Beacon " + std.keyName() + " has no key!")) else - cmp.hash(item, vf, keys) + var strHash :- cmp.hash(item, vf, keys); + if strHash.None? then + Success(None) + else + Success(Some(DDB.AttributeValue.S(strHash.value))) } function method naked(item : DDB.AttributeMap, vf : VirtualFieldMap) : Result, Error> { @@ -418,11 +422,7 @@ module SearchableEncryptionInfo { if keys.DontUseKeys? then naked(item, vf) else - var str :- hash(item, vf, keys); - if str.None? then - Success(None) - else - Success(Some(DS(str.value))) + hash(item, vf, keys) } function method getName() : string { @@ -446,17 +446,18 @@ module SearchableEncryptionInfo { cmp.GetFields(virtualFields) } - function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool) : Result + function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool) + : Result { if keys.DontUseKeys? then Success(value) else if Standard? then - :- Need(!keys.ShouldHaveKeys?, E("Need KeyId because of beacon " + std.base.name + " but no KeyId found in query")); + :- Need(!keys.ShouldHaveKeys?, E("Need KeyId because of beacon " + std.keyName() + " but no KeyId found in query")); var keys := keys.value; - if std.base.name in keys then - std.GetBeaconValue(value, keys[std.base.name]) + if std.keyName() in keys then + std.GetBeaconValue(value, keys[std.keyName()]) else - Failure(E("Internal error. Beacon " + std.base.name + " has no key.")) + Failure(E("Internal error. Beacon " + std.keyName() + " has no key.")) else cmp.GetBeaconValue(value, keys, forEquality) } @@ -482,6 +483,10 @@ module SearchableEncryptionInfo { | SignedBeacon | EncryptedBeacon + predicate method IsPartOnly(b : Beacon) + { + b.Standard? && b.std.partOnly + } predicate method IsBeaconOfType(b : Beacon, t : BeaconType) { match t { @@ -718,7 +723,9 @@ module SearchableEncryptionInfo { { if |names| == 0 then Success(acc) - else if IsBeaconOfType(beacons[names[0]], bType) then + //= specification/searchable-encryption/beacons.md#partonly-initialization + //# The Standard Beacon MUST NOT be stored in the item for a PartOnly beacon. + else if IsBeaconOfType(beacons[names[0]], bType) && !IsPartOnly(beacons[names[0]]) then var value :- GenerateBeacon(names[0], item, keys); if value.Some? then GenerateBeacons2(names[1..], item, keys, bType, acc[beacons[names[0]].getBeaconName() := value.value]) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index 5a020226f..4a3745329 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -16,12 +16,13 @@ module TestBaseBeacon { import I = SearchableEncryptionInfo import SI = SearchableEncryptionInfo import DDB = ComAmazonawsDynamodbTypes + import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes method {:test} TestBeacon() { var primitives :- expect Primitives.AtomicPrimitives(); var bb := BeaconBase(client := primitives, name := "foo", beaconName := "aws_dbe_b_foo"); - var b := StandardBeacon(bb, 8, TermLocMap("foo")); + var b := StandardBeacon(bb, 8, TermLocMap("foo"), false, false, None); var bytes :- expect bb.getHmac([1,2,3], key := [1,2]); expect bytes == [0x27, 0x93, 0x93, 0x8b, 0x26, 0xe9, 0x52, 0x7e]; var str :- expect b.hash([1,2,3], key := [1,2]); @@ -240,4 +241,357 @@ module TestBaseBeacon { expect newContext.names == None; //expect_equal(newContext.expr, Some("aws_dbe_b_std2 <> :A AND #Field4 = :B")); } + + method {:test} TestUnusedPartOnly() + { + var version := GetLotsaBeacons(); + var badBeacon := T.StandardBeacon(name := "badBeacon", length := 24, loc := None, + style := Some( + T.partOnly(T.PartOnly()) + )); + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["badBeacon" := SE.ENCRYPT_AND_SIGN]); + version := version.(standardBeacons := version.standardBeacons + [badBeacon]); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(newConfig, version, src); + expect bv.Failure?; + expect bv.error == E("PartOnly beacon badBeacon MUST be used in a compound beacon."); + } + + method {:test} TestCompoundWithUnknown() + { + var Unknown := T.EncryptedPart(name := "Unknown", prefix := "U_"); + + var NameUnknown := T.CompoundBeacon ( + name := "NameUnknown", + split := ".", + encrypted := Some([Name,Unknown]), + signed := None, + constructors := None + ); + var version := GetLotsaBeacons(); + expect version.compoundBeacons.Some?; + version := version.(compoundBeacons := Some(version.compoundBeacons.value + [NameUnknown])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(FullTableConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Compound beacon NameUnknown refers to standard beacon Unknown which is not configured."); + } + + method {:test} TesSetInCompound() + { + var version := GetLotsaBeacons(); + var setBeacon := T.StandardBeacon(name := "setBeacon", length := 24, loc := None, + style := Some( + T.asSet(T.AsSet()) + )); + var compoundSet := T.CompoundBeacon ( + name := "compoundSet", + split := ".", + encrypted := Some([Name,T.EncryptedPart(name := "setBeacon", prefix := "S_")]), + signed := None, + constructors := None + ); + + expect version.compoundBeacons.Some?; + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["setBeacon" := SE.ENCRYPT_AND_SIGN]); + version := version.(standardBeacons := version.standardBeacons + [setBeacon], + compoundBeacons := Some(version.compoundBeacons.value + [compoundSet])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(newConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Compound beacon compoundSet uses setBeacon which is an AsSet beacon, and therefore cannot be used in a Compound Beacon."); + } + + method {:test} TwinnedBadReferenceToCompound() + { + var version := GetLotsaBeacons(); + var twinBeacon := T.StandardBeacon(name := "twinBeacon", length := 24, loc := None, + style := Some( + T.twinned(T.Twinned(other := "NameTitle")) + )); + + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["twinBeacon" := SE.ENCRYPT_AND_SIGN]); + version := version.(standardBeacons := version.standardBeacons + [twinBeacon]); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(newConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Beacon twinBeacon is twinned to NameTitle but NameTitle is a compound beacon."); + } + + method {:test} TwinnedBadReferenceNonExistent() + { + var version := GetLotsaBeacons(); + var twinBeacon := T.StandardBeacon(name := "twinBeacon", length := 24, loc := None, + style := Some( + T.twinned(T.Twinned(other := "DoesNotExist")) + )); + + version := version.(standardBeacons := version.standardBeacons + [twinBeacon]); + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["twinBeacon" := SE.ENCRYPT_AND_SIGN]); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(newConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Beacon twinBeacon is twinned to DoesNotExist which is not defined."); + } + + + method {:test} TwinnedBadLength() + { + var version := GetLotsaBeacons(); + var twinBeacon := T.StandardBeacon(name := "twinBeacon", length := 23, loc := None, + style := Some( + T.twinned(T.Twinned(other := "std2")) + )); + + version := version.(standardBeacons := version.standardBeacons + [twinBeacon]); + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["twinBeacon" := SE.ENCRYPT_AND_SIGN]); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(newConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Beacon twinBeacon is twinned to std2 but twinBeacon has length 23 and std2 has length 24."); + } + + method {:test} TestPartOnlyNotStored() + { + var MyItem : DDB.AttributeMap := map[ + "std2" := DDB.AttributeValue.S("abc"), + "partOnly" := DDB.AttributeValue.S("def") + ]; + var compoundPart := T.CompoundBeacon ( + name := "compoundPart", + split := ".", + encrypted := Some([T.EncryptedPart(name := "partOnly", prefix := "S_")]), + signed := None, + constructors := None + ); + var context := ExprContext ( + None, + Some("partOnly = :val"), + Some(map[":val" := DDB.AttributeValue.S("foo")]), + None + ); + + var version := GetLotsaBeacons(); + expect version.compoundBeacons.Some?; + var partBeacon := T.StandardBeacon(name := "partOnly", length := 23, loc := None, style := None); + var newVersion := version.( + standardBeacons := version.standardBeacons + [partBeacon], + compoundBeacons := Some(version.compoundBeacons.value + [compoundPart]) + ); + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["partOnly" := SE.ENCRYPT_AND_SIGN]); + + var src := GetLiteralSource([1,2,3,4,5], newVersion); + var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); + + var goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + expect goodAttrs == map[ + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.S("405a51"), + "aws_dbe_b_compoundPart" := DDB.AttributeValue.S("S_405a51") + ]; + var goodQuery := Beaconize(bv, context, DontUseKeyId); + expect goodQuery.Success?; + + + partBeacon := T.StandardBeacon(name := "partOnly", length := 23, loc := None, + style := Some( + T.partOnly(T.PartOnly()) + )); + newVersion := version.( + standardBeacons := version.standardBeacons + [partBeacon], + compoundBeacons := Some(version.compoundBeacons.value + [compoundPart]) + ); + bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); + goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + + //= specification/searchable-encryption/beacons.md#partonly-initialization + //= type=test + //# The Standard Beacon MUST NOT be stored in the item for a PartOnly beacon. + expect goodAttrs == map[ + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_compoundPart" := DDB.AttributeValue.S("S_405a51") + ]; + + //= specification/searchable-encryption/beacons.md#partonly-initialization + //= type=test + //# A query MUST fail if it tries to search on a PartOnly beacon directly. + var badQuery := Beaconize(bv, context, DontUseKeyId); + expect badQuery.Failure?; + expect badQuery.error == E("Field partOnly is encrypted, and has a PartOnly beacon, and so can only be used as part of a compound beacon."); + } + + method {:test} TestTwinSameBeacon() + { + var MyItem : DDB.AttributeMap := map[ + "std2" := DDB.AttributeValue.S("abc"), + "partOnly" := DDB.AttributeValue.S("abc") + ]; + + var version := GetLotsaBeacons(); + expect version.compoundBeacons.Some?; + var partBeacon := T.StandardBeacon(name := "partOnly", length := 24, loc := None, style := None); + var newVersion := version.( + standardBeacons := version.standardBeacons + [partBeacon] + ); + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["partOnly" := SE.ENCRYPT_AND_SIGN]); + + var src := GetLiteralSource([1,2,3,4,5], newVersion); + var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); + + var goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + expect goodAttrs == map[ + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.S("928d9b") + ]; + + + partBeacon := T.StandardBeacon(name := "partOnly", length := 24, loc := None, + style := Some( + T.twinned(T.Twinned(other := "std2")) + )); + newVersion := version.( + standardBeacons := version.standardBeacons + [partBeacon] + ); + bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); + goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + + //= specification/searchable-encryption/beacons.md#twinned-initialization + //= type=test + //# This beacon MUST calculate its [value](#beacon-value) as if it were the `other` beacon. + expect goodAttrs == map[ + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.S("51e1da") + ]; + + // also check matching beacon value in query + var context := ExprContext ( + None, + Some("partOnly = :pVal AND std2 = :sVal"), + Some(map[":pVal" := DDB.AttributeValue.S("foo"), ":sVal" := DDB.AttributeValue.S("foo")]), + None + ); + var goodQuery :- expect Beaconize(bv, context, DontUseKeyId); + expect goodQuery.values == Some(map[":pVal" := DDB.AttributeValue.S("4379a7"), ":sVal" := DDB.AttributeValue.S("4379a7")]); + } + + method {:test} TestBeaconSetQuery() + { + var context := ExprContext ( + None, + Some("setAttr = :setVal"), + Some(map[":setVal" := DDB.AttributeValue.SS(["abc", "def", "ghi"])]), + None + ); + var setBeacon := T.StandardBeacon(name := "setAttr", length := 24, loc := None, + style := Some( + T.asSet(T.AsSet()) + )); + + var version := GetLotsaBeacons(); + var newVersion := version.( + standardBeacons := version.standardBeacons + [setBeacon] + ); + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["setAttr" := SE.ENCRYPT_AND_SIGN]); + + var src := GetLiteralSource([1,2,3,4,5], newVersion); + var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); + + // also check matching beacon value in query + var goodQuery :- expect Beaconize(bv, context, DontUseKeyId); + expect goodQuery.values == Some(map[":setVal" := DDB.AttributeValue.SS(["43c4d8", "2f3278", "f1972e"])]); + + context := ExprContext ( + None, + Some("setAttr = :setVal"), + Some(map[":setVal" := DDB.AttributeValue.S("abc")]), + None + ); + var badQuery := Beaconize(bv, context, DontUseKeyId); + expect badQuery.Failure?; + expect badQuery.error == E("Beacon setAttr has style AsSet, but attribute has type S."); + } + + method {:test} TestSetNotSet() + { + var MyItem : DDB.AttributeMap := map[ + "std2" := DDB.AttributeValue.S("abc"), + "partOnly" := DDB.AttributeValue.SS(["abc", "def", "ghi"]) + ]; + + var version := GetLotsaBeacons(); + expect version.compoundBeacons.Some?; + var partBeacon := T.StandardBeacon(name := "partOnly", length := 24, loc := None, + style := Some( + T.asSet(T.AsSet()) + )); + var newVersion := version.( + standardBeacons := version.standardBeacons + [partBeacon] + ); + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["partOnly" := SE.ENCRYPT_AND_SIGN]); + + var src := GetLiteralSource([1,2,3,4,5], newVersion); + var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); + expect "partOnly" in bv.beacons; + expect bv.beacons["partOnly"].Standard?; + var goodAttrs := bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + if goodAttrs.Failure? { + print "\n", goodAttrs.error, "\n"; + } + //= specification/searchable-encryption/beacons.md#asset-initialization + //= type=test + //# * The Standard Beacon MUST be stored in the item as a Set, + //# comprised of the [beacon values](#beacon-value) of all the elements in the original Set. + expect goodAttrs.Success?; + expect goodAttrs.value == map[ + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.SS(["928d9b", "405a51", "9c6c2e"]) + ]; + + //= specification/searchable-encryption/beacons.md#asset-initialization + //= type=test + //# * Writing an item MUST fail if the item contains this beacon's attribute, + //# and that attribute is not of type Set. + var BadItem := MyItem["partOnly" := DDB.AttributeValue.S("abc")]; + var badAttrs := bv.GenerateEncryptedBeacons(BadItem, DontUseKeyId); + expect badAttrs.Failure?; + expect badAttrs.error == E("Beacon partOnly has style AsSet, but attribute has type S."); + } + + method {:test} TestTwinnedSet() + { + var MyItem : DDB.AttributeMap := map[ + "std2" := DDB.AttributeValue.S("abc"), + "partOnly" := DDB.AttributeValue.SS(["abc", "def", "ghi"]) + ]; + + var version := GetLotsaBeacons(); + expect version.compoundBeacons.Some?; + var partBeacon := T.StandardBeacon(name := "partOnly", length := 24, loc := None, + style := Some( + T.twinnedSet(T.TwinnedSet(other := "std2")) + )); + var newVersion := version.( + standardBeacons := version.standardBeacons + [partBeacon] + ); + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["partOnly" := SE.ENCRYPT_AND_SIGN]); + + var src := GetLiteralSource([1,2,3,4,5], newVersion); + var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); + expect "partOnly" in bv.beacons; + expect bv.beacons["partOnly"].Standard?; + var goodAttrs := bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + if goodAttrs.Failure? { + print "\n", goodAttrs.error, "\n"; + } + + //= specification/searchable-encryption/beacons.md#twinnedset-initialization + //= type=test + //# A TwinnedSet Beacon MUST behave both as [Twinned](#twinned-initialization) and [AsSet](#asset-initialization). + expect goodAttrs.Success?; + expect goodAttrs.value == map[ + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.SS(["51e1da", "39ef85", "3ff06a"]) + ]; + } + } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index 0da7ef2c0..d4dbad813 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy @@ -31,12 +31,12 @@ module BeaconTestFixtures { expect a == b; } - const std2 := StandardBeacon(name := "std2", length := 24, loc := None) - const std4 := StandardBeacon(name := "std4", length := 24, loc := Some("std4")) - const std6 := StandardBeacon(name := "std6", length := 26, loc := Some("std6[0]")) - const NameB := StandardBeacon(name := "Name", length := 32, loc := None) - const TitleB := StandardBeacon(name := "Title", length := 32, loc := None) - const TooBadB := StandardBeacon(name := "TooBad", length := 32, loc := None) + const std2 := StandardBeacon(name := "std2", length := 24, loc := None, style := None) + const std4 := StandardBeacon(name := "std4", length := 24, loc := Some("std4"), style := None) + const std6 := StandardBeacon(name := "std6", length := 26, loc := Some("std6[0]"), style := None) + const NameB := StandardBeacon(name := "Name", length := 32, loc := None, style := None) + const TitleB := StandardBeacon(name := "Title", length := 32, loc := None, style := None) + const TooBadB := StandardBeacon(name := "TooBad", length := 32, loc := None, style := None) const Year := SignedPart(name := "Year", prefix := "Y_", loc := None) const Month := SignedPart(name := "Month", prefix := "M_", loc := Some("Date.Month")) @@ -116,7 +116,7 @@ module BeaconTestFixtures { const VPart1 := VirtualPart(loc := "Name", trans := Some([insert(Insert(literal := "__"))])) const VPart2 := VirtualPart(loc := "Title", trans := Some([lower(Lower)])) const NameTitleField := VirtualField(name := "NameTitleField", parts := [VPart1, VPart2]) - const NameTitleBeacon := StandardBeacon(name := "NameTitleField", length := 28, loc := None) + const NameTitleBeacon := StandardBeacon(name := "NameTitleField", length := 28, loc := None, style := None) const NameVirtField := VirtualField(name := "NameVirtField", parts := [VPart1]) method GetKeyStore() returns (output : SI.ValidStore) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/ConfigToInfo.dfy index 190ee68ee..948a11b34 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/ConfigToInfo.dfy @@ -16,7 +16,7 @@ module TestDynamoDBConfigToInfo { import opened DynamoDbEncryptionUtil method {:test} TestTwoBeaconsOneLoc() { - var fred := StandardBeacon(name := "fred", length := 16, loc := Some("std6[0]")); + var fred := StandardBeacon(name := "fred", length := 16, loc := Some("std6[0]"), style := None); var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var newBeacons := version.(standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB, fred]); diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java index 935f78b96..3d12ad645 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java @@ -15,7 +15,9 @@ import java.util.List; import java.util.Map; import java.util.Objects; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconStyle; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconVersion; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.CompoundBeacon; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Constructor; @@ -41,11 +43,14 @@ import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyPolicy; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Lower; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.PartOnly; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.PlaintextOverride; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SearchConfig; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SignedPart; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.StandardBeacon; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Twinned; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.TwinnedSet; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Upper; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.VirtualField; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.VirtualPart; @@ -89,6 +94,11 @@ public static Error Error(CollectionOfErrors nativeValue) { return Error.create_CollectionOfErrors(list, message); } + public static AsSet AsSet( + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.AsSet nativeValue) { + return new AsSet(); + } + public static BeaconVersion BeaconVersion( software.amazon.cryptography.dbencryptionsdk.dynamodb.model.BeaconVersion nativeValue) { Integer version; @@ -326,6 +336,11 @@ public static MultiKeyStore MultiKeyStore( return new MultiKeyStore(keyFieldName, cacheTTL, cache); } + public static PartOnly PartOnly( + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.PartOnly nativeValue) { + return new PartOnly(); + } + public static SearchConfig SearchConfig( software.amazon.cryptography.dbencryptionsdk.dynamodb.model.SearchConfig nativeValue) { DafnySequence versions; @@ -367,7 +382,25 @@ public static StandardBeacon StandardBeacon( loc = Objects.nonNull(nativeValue.loc()) ? Option.create_Some(software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.loc())) : Option.create_None(); - return new StandardBeacon(name, length, loc); + Option style; + style = Objects.nonNull(nativeValue.style()) ? + Option.create_Some(ToDafny.BeaconStyle(nativeValue.style())) + : Option.create_None(); + return new StandardBeacon(name, length, loc, style); + } + + public static Twinned Twinned( + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.Twinned nativeValue) { + DafnySequence other; + other = software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.other()); + return new Twinned(other); + } + + public static TwinnedSet TwinnedSet( + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.TwinnedSet nativeValue) { + DafnySequence other; + other = software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.other()); + return new TwinnedSet(other); } public static Upper Upper( @@ -448,6 +481,23 @@ public static BeaconKeySource BeaconKeySource( throw new IllegalArgumentException("Cannot convert " + nativeValue + " to software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource."); } + public static BeaconStyle BeaconStyle( + software.amazon.cryptography.dbencryptionsdk.dynamodb.model.BeaconStyle nativeValue) { + if (Objects.nonNull(nativeValue.partOnly())) { + return BeaconStyle.create_partOnly(ToDafny.PartOnly(nativeValue.partOnly())); + } + if (Objects.nonNull(nativeValue.twinned())) { + return BeaconStyle.create_twinned(ToDafny.Twinned(nativeValue.twinned())); + } + if (Objects.nonNull(nativeValue.asSet())) { + return BeaconStyle.create_asSet(ToDafny.AsSet(nativeValue.asSet())); + } + if (Objects.nonNull(nativeValue.twinnedSet())) { + return BeaconStyle.create_twinnedSet(ToDafny.TwinnedSet(nativeValue.twinnedSet())); + } + throw new IllegalArgumentException("Cannot convert " + nativeValue + " to software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconStyle."); + } + public static VirtualTransform VirtualTransform( software.amazon.cryptography.dbencryptionsdk.dynamodb.model.VirtualTransform nativeValue) { if (Objects.nonNull(nativeValue.upper())) { diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java index dc5596447..53710c30e 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java @@ -16,7 +16,9 @@ import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error_DynamoDbEncryptionException; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error_Opaque; import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.IDynamoDbEncryptionClient; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.AsSet; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.BeaconKeySource; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.BeaconStyle; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.BeaconVersion; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.CollectionOfErrors; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.CompoundBeacon; @@ -42,11 +44,14 @@ import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.Lower; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.MultiKeyStore; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.OpaqueError; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.PartOnly; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.PlaintextOverride; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.SearchConfig; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.SignedPart; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.SingleKeyStore; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.StandardBeacon; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.Twinned; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.TwinnedSet; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.Upper; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.VirtualField; import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.VirtualPart; @@ -103,6 +108,12 @@ public static RuntimeException Error(Error dafnyValue) { return nativeBuilder.build(); } + public static AsSet AsSet( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet dafnyValue) { + AsSet.Builder nativeBuilder = AsSet.builder(); + return nativeBuilder.build(); + } + public static BeaconVersion BeaconVersion( software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconVersion dafnyValue) { BeaconVersion.Builder nativeBuilder = BeaconVersion.builder(); @@ -311,6 +322,12 @@ public static MultiKeyStore MultiKeyStore( return nativeBuilder.build(); } + public static PartOnly PartOnly( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.PartOnly dafnyValue) { + PartOnly.Builder nativeBuilder = PartOnly.builder(); + return nativeBuilder.build(); + } + public static SearchConfig SearchConfig( software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SearchConfig dafnyValue) { SearchConfig.Builder nativeBuilder = SearchConfig.builder(); @@ -346,6 +363,23 @@ public static StandardBeacon StandardBeacon( if (dafnyValue.dtor_loc().is_Some()) { nativeBuilder.loc(software.amazon.smithy.dafny.conversion.ToNative.Simple.String(dafnyValue.dtor_loc().dtor_value())); } + if (dafnyValue.dtor_style().is_Some()) { + nativeBuilder.style(ToNative.BeaconStyle(dafnyValue.dtor_style().dtor_value())); + } + return nativeBuilder.build(); + } + + public static Twinned Twinned( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Twinned dafnyValue) { + Twinned.Builder nativeBuilder = Twinned.builder(); + nativeBuilder.other(software.amazon.smithy.dafny.conversion.ToNative.Simple.String(dafnyValue.dtor_other())); + return nativeBuilder.build(); + } + + public static TwinnedSet TwinnedSet( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.TwinnedSet dafnyValue) { + TwinnedSet.Builder nativeBuilder = TwinnedSet.builder(); + nativeBuilder.other(software.amazon.smithy.dafny.conversion.ToNative.Simple.String(dafnyValue.dtor_other())); return nativeBuilder.build(); } @@ -413,6 +447,24 @@ public static BeaconKeySource BeaconKeySource( return nativeBuilder.build(); } + public static BeaconStyle BeaconStyle( + software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconStyle dafnyValue) { + BeaconStyle.Builder nativeBuilder = BeaconStyle.builder(); + if (dafnyValue.is_partOnly()) { + nativeBuilder.partOnly(ToNative.PartOnly(dafnyValue.dtor_partOnly())); + } + if (dafnyValue.is_twinned()) { + nativeBuilder.twinned(ToNative.Twinned(dafnyValue.dtor_twinned())); + } + if (dafnyValue.is_asSet()) { + nativeBuilder.asSet(ToNative.AsSet(dafnyValue.dtor_asSet())); + } + if (dafnyValue.is_twinnedSet()) { + nativeBuilder.twinnedSet(ToNative.TwinnedSet(dafnyValue.dtor_twinnedSet())); + } + return nativeBuilder.build(); + } + public static VirtualTransform VirtualTransform( software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.VirtualTransform dafnyValue) { VirtualTransform.Builder nativeBuilder = VirtualTransform.builder(); diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/AsSet.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/AsSet.java new file mode 100644 index 000000000..0c217c8b6 --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/AsSet.java @@ -0,0 +1,36 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +/** + * Attribute must be a Set. Beacon value will also be a Set. + */ +public class AsSet { + protected AsSet(BuilderImpl builder) { + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + AsSet build(); + } + + static class BuilderImpl implements Builder { + protected BuilderImpl() { + } + + protected BuilderImpl(AsSet model) { + } + + public AsSet build() { + return new AsSet(this); + } + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconStyle.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconStyle.java new file mode 100644 index 000000000..280afaa4c --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconStyle.java @@ -0,0 +1,192 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +import java.util.Objects; + +public class BeaconStyle { + /** + * Attribute must be used as part of a Compound Beacon, never alone. + */ + private final PartOnly partOnly; + + /** + * This beacon should calculate values like another beacon, so they can be compared. + */ + private final Twinned twinned; + + /** + * Attribute must be a Set. Beacon value will also be a Set. + */ + private final AsSet asSet; + + /** + * Both Twinned and AsSet. + */ + private final TwinnedSet twinnedSet; + + protected BeaconStyle(BuilderImpl builder) { + this.partOnly = builder.partOnly(); + this.twinned = builder.twinned(); + this.asSet = builder.asSet(); + this.twinnedSet = builder.twinnedSet(); + } + + /** + * @return Attribute must be used as part of a Compound Beacon, never alone. + */ + public PartOnly partOnly() { + return this.partOnly; + } + + /** + * @return This beacon should calculate values like another beacon, so they can be compared. + */ + public Twinned twinned() { + return this.twinned; + } + + /** + * @return Attribute must be a Set. Beacon value will also be a Set. + */ + public AsSet asSet() { + return this.asSet; + } + + /** + * @return Both Twinned and AsSet. + */ + public TwinnedSet twinnedSet() { + return this.twinnedSet; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param partOnly Attribute must be used as part of a Compound Beacon, never alone. + */ + Builder partOnly(PartOnly partOnly); + + /** + * @return Attribute must be used as part of a Compound Beacon, never alone. + */ + PartOnly partOnly(); + + /** + * @param twinned This beacon should calculate values like another beacon, so they can be compared. + */ + Builder twinned(Twinned twinned); + + /** + * @return This beacon should calculate values like another beacon, so they can be compared. + */ + Twinned twinned(); + + /** + * @param asSet Attribute must be a Set. Beacon value will also be a Set. + */ + Builder asSet(AsSet asSet); + + /** + * @return Attribute must be a Set. Beacon value will also be a Set. + */ + AsSet asSet(); + + /** + * @param twinnedSet Both Twinned and AsSet. + */ + Builder twinnedSet(TwinnedSet twinnedSet); + + /** + * @return Both Twinned and AsSet. + */ + TwinnedSet twinnedSet(); + + BeaconStyle build(); + } + + static class BuilderImpl implements Builder { + protected PartOnly partOnly; + + protected Twinned twinned; + + protected AsSet asSet; + + protected TwinnedSet twinnedSet; + + protected BuilderImpl() { + } + + protected BuilderImpl(BeaconStyle model) { + this.partOnly = model.partOnly(); + this.twinned = model.twinned(); + this.asSet = model.asSet(); + this.twinnedSet = model.twinnedSet(); + } + + public Builder partOnly(PartOnly partOnly) { + this.partOnly = partOnly; + return this; + } + + public PartOnly partOnly() { + return this.partOnly; + } + + public Builder twinned(Twinned twinned) { + this.twinned = twinned; + return this; + } + + public Twinned twinned() { + return this.twinned; + } + + public Builder asSet(AsSet asSet) { + this.asSet = asSet; + return this; + } + + public AsSet asSet() { + return this.asSet; + } + + public Builder twinnedSet(TwinnedSet twinnedSet) { + this.twinnedSet = twinnedSet; + return this; + } + + public TwinnedSet twinnedSet() { + return this.twinnedSet; + } + + public BeaconStyle build() { + if (!onlyOneNonNull()) { + throw new IllegalArgumentException("`BeaconStyle` is a Union. A Union MUST have one and only one value set."); + } + return new BeaconStyle(this); + } + + private boolean onlyOneNonNull() { + Object[] allValues = {this.partOnly, this.twinned, this.asSet, this.twinnedSet}; + boolean haveOneNonNull = false; + for (Object o : allValues) { + if (Objects.nonNull(o)) { + if (haveOneNonNull) { + return false; + } + haveOneNonNull = true; + } + } + return haveOneNonNull; + } + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconVersion.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconVersion.java index 439905f94..2140ed8b8 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconVersion.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconVersion.java @@ -17,7 +17,7 @@ public class BeaconVersion { private final int version; /** - * The Key Store that contains the Becon Keys to use with searchable encryption. + * The Key Store that contains the Beacon Keys to use with searchable encryption. */ private final KeyStore keyStore; @@ -58,7 +58,7 @@ public int version() { } /** - * @return The Key Store that contains the Becon Keys to use with searchable encryption. + * @return The Key Store that contains the Beacon Keys to use with searchable encryption. */ public KeyStore keyStore() { return this.keyStore; @@ -112,12 +112,12 @@ public interface Builder { int version(); /** - * @param keyStore The Key Store that contains the Becon Keys to use with searchable encryption. + * @param keyStore The Key Store that contains the Beacon Keys to use with searchable encryption. */ Builder keyStore(KeyStore keyStore); /** - * @return The Key Store that contains the Becon Keys to use with searchable encryption. + * @return The Key Store that contains the Beacon Keys to use with searchable encryption. */ KeyStore keyStore(); diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/PartOnly.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/PartOnly.java new file mode 100644 index 000000000..dfd41a508 --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/PartOnly.java @@ -0,0 +1,36 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +/** + * Attribute must be used as part of a Compound Beacon, never alone. + */ +public class PartOnly { + protected PartOnly(BuilderImpl builder) { + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + PartOnly build(); + } + + static class BuilderImpl implements Builder { + protected BuilderImpl() { + } + + protected BuilderImpl(PartOnly model) { + } + + public PartOnly build() { + return new PartOnly(this); + } + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/StandardBeacon.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/StandardBeacon.java index 4a32f355d..bcd24a6ca 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/StandardBeacon.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/StandardBeacon.java @@ -24,10 +24,16 @@ public class StandardBeacon { */ private final String loc; + /** + * Optional augmented behavior. + */ + private final BeaconStyle style; + protected StandardBeacon(BuilderImpl builder) { this.name = builder.name(); this.length = builder.length(); this.loc = builder.loc(); + this.style = builder.style(); } /** @@ -51,6 +57,13 @@ public String loc() { return this.loc; } + /** + * @return Optional augmented behavior. + */ + public BeaconStyle style() { + return this.style; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -90,6 +103,16 @@ public interface Builder { */ String loc(); + /** + * @param style Optional augmented behavior. + */ + Builder style(BeaconStyle style); + + /** + * @return Optional augmented behavior. + */ + BeaconStyle style(); + StandardBeacon build(); } @@ -102,6 +125,8 @@ static class BuilderImpl implements Builder { protected String loc; + protected BeaconStyle style; + protected BuilderImpl() { } @@ -110,6 +135,7 @@ protected BuilderImpl(StandardBeacon model) { this.length = model.length(); this._lengthSet = true; this.loc = model.loc(); + this.style = model.style(); } public Builder name(String name) { @@ -140,6 +166,15 @@ public String loc() { return this.loc; } + public Builder style(BeaconStyle style) { + this.style = style; + return this; + } + + public BeaconStyle style() { + return this.style; + } + public StandardBeacon build() { if (Objects.isNull(this.name())) { throw new IllegalArgumentException("Missing value for required field `name`"); diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/Twinned.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/Twinned.java new file mode 100644 index 000000000..a7f91e640 --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/Twinned.java @@ -0,0 +1,76 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +import java.util.Objects; + +/** + * This beacon should calculate values like another beacon, so they can be compared. + */ +public class Twinned { + /** + * Calculate beacon values as for this beacon. + */ + private final String other; + + protected Twinned(BuilderImpl builder) { + this.other = builder.other(); + } + + /** + * @return Calculate beacon values as for this beacon. + */ + public String other() { + return this.other; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param other Calculate beacon values as for this beacon. + */ + Builder other(String other); + + /** + * @return Calculate beacon values as for this beacon. + */ + String other(); + + Twinned build(); + } + + static class BuilderImpl implements Builder { + protected String other; + + protected BuilderImpl() { + } + + protected BuilderImpl(Twinned model) { + this.other = model.other(); + } + + public Builder other(String other) { + this.other = other; + return this; + } + + public String other() { + return this.other; + } + + public Twinned build() { + if (Objects.isNull(this.other())) { + throw new IllegalArgumentException("Missing value for required field `other`"); + } + return new Twinned(this); + } + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/TwinnedSet.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/TwinnedSet.java new file mode 100644 index 000000000..9c382e11c --- /dev/null +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/TwinnedSet.java @@ -0,0 +1,76 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.dbencryptionsdk.dynamodb.model; + +import java.util.Objects; + +/** + * Both Twinned and AsSet. + */ +public class TwinnedSet { + /** + * Calculate beacon values as for this beacon. + */ + private final String other; + + protected TwinnedSet(BuilderImpl builder) { + this.other = builder.other(); + } + + /** + * @return Calculate beacon values as for this beacon. + */ + public String other() { + return this.other; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param other Calculate beacon values as for this beacon. + */ + Builder other(String other); + + /** + * @return Calculate beacon values as for this beacon. + */ + String other(); + + TwinnedSet build(); + } + + static class BuilderImpl implements Builder { + protected String other; + + protected BuilderImpl() { + } + + protected BuilderImpl(TwinnedSet model) { + this.other = model.other(); + } + + public Builder other(String other) { + this.other = other; + return this; + } + + public String other() { + return this.other; + } + + public TwinnedSet build() { + if (Objects.isNull(this.other())) { + throw new IllegalArgumentException("Missing value for required field `other`"); + } + return new TwinnedSet(this); + } + } +} diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/DynamoDbEncryptionTransforms.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/DynamoDbEncryptionTransforms.java index 94cb7d63b..7140ad9c4 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/DynamoDbEncryptionTransforms.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/DynamoDbEncryptionTransforms.java @@ -262,7 +262,7 @@ public QueryOutputTransformOutput QueryOutputTransform(QueryOutputTransformInput } /** - * Given an Item, show the intermediate values. + * Given an Item, show the intermediate values (e.g. compound beacons, virtual fields). * */ public ResolveAttributesOutput ResolveAttributes(ResolveAttributesInput input) { diff --git a/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/CompoundBeaconSearchableEncryptionExample.java b/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/CompoundBeaconSearchableEncryptionExample.java index 83897e2df..baabb5e03 100644 --- a/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/CompoundBeaconSearchableEncryptionExample.java +++ b/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/CompoundBeaconSearchableEncryptionExample.java @@ -328,16 +328,26 @@ public static void PutAndQueryItemWithCompoundBeacon(DynamoDbClient ddb, String .expressionAttributeValues(expressionAttributeValues) .build(); - QueryResponse queryResponse = ddb.query(queryRequest); - List> attributeValues = queryResponse.items(); - // Validate query was returned successfully - assert 200 == queryResponse.sdkHttpResponse().statusCode(); - // Validate only 1 item was returned: the item we just put - assert attributeValues.size() == 1; - Map returnedItem = attributeValues.get(0); - // Validate the item has the expected attributes - assert returnedItem.get("inspector_id_last4").s().equals("5678"); - assert returnedItem.get("unit").s().equals("011899988199"); + for (int i=0; i<10; ++i) { + QueryResponse queryResponse = ddb.query(queryRequest); + List> attributeValues = queryResponse.items(); + // Validate query was returned successfully + assert 200 == queryResponse.sdkHttpResponse().statusCode(); + + // if no results, sleep and try again + if (attributeValues.size() == 0) { + try {Thread.sleep(20);} catch (Exception e) {} + continue; + } + + // Validate only 1 item was returned: the item we just put + assert attributeValues.size() == 1; + Map returnedItem = attributeValues.get(0); + // Validate the item has the expected attributes + assert returnedItem.get("inspector_id_last4").s().equals("5678"); + assert returnedItem.get("unit").s().equals("011899988199"); + break; + } } public static void main(final String[] args) { diff --git a/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/VirtualBeaconSearchableEncryptionExample.java b/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/VirtualBeaconSearchableEncryptionExample.java index 138fb7306..d6ae06c77 100644 --- a/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/VirtualBeaconSearchableEncryptionExample.java +++ b/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/VirtualBeaconSearchableEncryptionExample.java @@ -436,16 +436,26 @@ public static void PutItemQueryItemWithVirtualBeacon(String ddbTableName, String .expressionAttributeValues(expressionAttributeValues) .build(); - final QueryResponse queryResponse = ddb.query(queryRequest); - List> attributeValues = queryResponse.items(); - // Validate query was returned successfully - assert 200 == queryResponse.sdkHttpResponse().statusCode(); - // Validate only 1 item was returned: the item with the expected attributes - assert attributeValues.size() == 1; - final Map returnedItem = attributeValues.get(0); - // Validate the item has the expected attributes - assert returnedItem.get("state").s().equals("CA"); - assert returnedItem.get("hasTestResult").bool().equals(true); + for (int i=0; i<10; ++i) { + final QueryResponse queryResponse = ddb.query(queryRequest); + List> attributeValues = queryResponse.items(); + // Validate query was returned successfully + assert 200 == queryResponse.sdkHttpResponse().statusCode(); + + // if no results, sleep and try again + if (attributeValues.size() == 0) { + try {Thread.sleep(20);} catch (Exception e) {} + continue; + } + + // Validate only 1 item was returned: the item with the expected attributes + assert attributeValues.size() == 1; + final Map returnedItem = attributeValues.get(0); + // Validate the item has the expected attributes + assert returnedItem.get("state").s().equals("CA"); + assert returnedItem.get("hasTestResult").bool().equals(true); + break; + } } public static void main(final String[] args) { diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 4baa2452c..506b6848d 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -19,6 +19,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { import opened Wrappers import opened StandardLibrary import opened StandardLibrary.UInt + import opened StandardLibrary.String import opened JSON.Values import opened DynamoDbEncryptionUtil import opened DdbItemJson @@ -1759,7 +1760,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { } :- Need(0 < |name|, "Each Standard Beacon needs a name."); :- Need(0 < length < 100 && Types.IsValid_BeaconBitLength(length as int32), "Each Standard Beacon needs a length between 1 and 63."); - return Success(Types.StandardBeacon(name := name, length := length as Types.BeaconBitLength, loc := loc)); + return Success(Types.StandardBeacon(name := name, length := length as Types.BeaconBitLength, loc := loc, style := None)); } method GetGSIs(data : JSON) returns (output : Result , string>) diff --git a/specification/searchable-encryption/beacons.md b/specification/searchable-encryption/beacons.md index a9ad70a04..99da07025 100644 --- a/specification/searchable-encryption/beacons.md +++ b/specification/searchable-encryption/beacons.md @@ -287,12 +287,64 @@ On initialization of a Standard Beacon, the caller MUST provide: On initialization of a Standard Beacon, the caller MAY provide: * a [terminal location](virtual.md#terminal-location) -- a string + * a [beacon style](beacon-style-initialization) If no [terminal location](virtual.md#terminal-location) is provided, the `name` MUST be used as the [terminal location](virtual.md#terminal-location). Initialization MUST fail if two standard beacons are configured with the same location. + ### Beacon Style Initialization + +On initialization of a Beacon Style, the caller MUST provide exactly one of + + * a [PartOnly](#partonly-initialization) + * a [Twinned](#twinned-initialization) + * an [AsSet](#asset-initialization) + * a [TwinnedSet](#twinnedset-initialization) + +### PartOnly Initialization + +On initialization of a PartOnly, the caller MUST NOT provide any +additional parameters to the PartOnly. + +Initialization MUST fail if the configuration does not use a PartOnly in a [compound beacon](#compound-beacon). + +The Standard Beacon MUST NOT be stored in the item for a PartOnly beacon. + +A query MUST fail if it tries to search on a PartOnly beacon directly. + +### AsSet Initialization + +On initialization of as AsSet, the caller MUST NOT provide any +additional parameters to the AsSet. + +* initialization MUST fail if any compound beacon has an AsSet beacon as a part. +* Writing an item MUST fail if the item contains this beacon's attribute, +and that attribute is not of type Set. +* The Standard Beacon MUST be stored in the item as a Set, +comprised of the [beacon values](#beacon-value) of all the elements in the original Set. + +### Twinned Initialization + +On initialization of a Twinned, the caller MUST provide: + +* other : a beacon name + +This name MUST be the name of a previously defined Standard Beacon. + +This beacon's [length](#beacon-length) MUST be equal to the `other` beacon's [length](#beacon-length). + +This beacon MUST calculate its [value](#beacon-value) as if it were the `other` beacon. + +### TwinnedSet Initialization + +On initialization of a TwinnedSet, the caller MUST provide: + +* other : a beacon name + +A TwinnedSet Beacon MUST behave both as [Twinned](#twinned-initialization) and [AsSet](#asset-initialization). + ### Compound Beacon Initialization @@ -398,11 +450,28 @@ of the input string, the HMAC key from the [key materials](./search-config.md#ge associated with this beacon, and the beacon length associated with this beacon. ### value for a standard beacon - * This operation MUST take an [hmac key](./search-config.md#hmac-key-generation), a record as input, and produce an optional string. + * This operation MUST take an [hmac key](./search-config.md#hmac-key-generation), a record as input, and produce an optional [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html). * This operation MUST return no value if the associated field does not exist in the record + * If this beacon is marked AsSet then this operation MUST return the + [set value](#value-for-a-set-standard-beacon), +otherwise it MUST return the [non-set value](#value-for-a-non-set-standard-beacon) + +### value for a non-set standard beacon * This operation MUST convert the attribute value of the associated field to a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md). - * This operation MUST return the [basicHash](#basichash) of the input and the configured [beacon length](#beacon-length). + * This operation MUST return the [basicHash](#basichash) of the resulting bytes and the configured [beacon length](#beacon-length). + * The returned +[AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html) +MUST be type "S" String. + +### value for a set standard beacon + * This operation MUST convert the value of each item in the set to +a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md). + * This operation MUST return a set containing the [basicHash](#basichash) of the resulting bytes and the configured [beacon length](#beacon-length). + * The resulting set MUST NOT contain duplicates. + * The returned +[AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html) +MUST be type "SS" StringSet. ### value for a compound beacon