Skip to content

feat: implement beacon styles #441

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Sep 22, 2023
Merged

feat: implement beacon styles #441

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
bec4194
feat: implement beacon styles
ajewellamz Sep 21, 2023
14652ab
m
ajewellamz Sep 21, 2023
fe66f4a
m
ajewellamz Sep 21, 2023
e8e7928
respond to PR feedback
ajewellamz Sep 21, 2023
6c67bba
update spec
ajewellamz Sep 22, 2023
ae3e691
m
ajewellamz Sep 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 19 additions & 1 deletion ...Encryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,9 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"

// Begin Generated Types

datatype AsSet = | AsSet (

)
type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
type BeaconBitLength = x: int32 | IsValid_BeaconBitLength(x) witness *
predicate method IsValid_BeaconBitLength(x: int32) {
Expand All @@ -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 ,
Expand Down Expand Up @@ -310,6 +318,9 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
nameonly keyFieldName: string ,
nameonly cacheTTL: int32 ,
nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType>
)
datatype PartOnly = | PartOnly (

)
datatype PlaintextOverride =
| FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ
Expand Down Expand Up @@ -339,7 +350,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
datatype StandardBeacon = | StandardBeacon (
nameonly name: string ,
nameonly length: BeaconBitLength ,
nameonly loc: Option<TerminalLocation>
nameonly loc: Option<TerminalLocation> ,
nameonly style: Option<BeaconStyle>
)
type StandardBeaconList = x: seq<StandardBeacon> | IsValid_StandardBeaconList(x) witness *
predicate method IsValid_StandardBeaconList(x: seq<StandardBeacon>) {
Expand All @@ -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 (

)
Expand Down
58 changes: 57 additions & 1 deletion DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down
136 changes: 115 additions & 21 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,10 @@ module BaseBeacon {
client: Primitives.AtomicPrimitivesClient,
name: string,
length : BeaconLength,
loc : string
loc : string,
partOnly : bool,
asSet : bool,
twin : Option<string>
)
: (ret : Result<ValidStandardBeacon, Error>)
ensures ret.Success? ==>
Expand All @@ -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<string>
) {
function method {:opaque} hash(val : Bytes, key : Bytes)
: (ret : Result<string, Error>)
Expand All @@ -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
Expand All @@ -159,25 +179,25 @@ 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()])
}

//= 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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Need to update the spec with the new output type

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done

function method {:opaque} getHash(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes) : (ret : Result<Option<string>, Error>)
ensures ret.Success? ==>
function method {:opaque} getHash(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes) : (ret : Result<Option<DDB.AttributeValue>, Error>)
ensures ret.Success? && !asSet ==>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we add specification for if it is asSet?

&& VirtToBytes(loc, item, vf).Success?
//= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon
//= type=implication
Expand All @@ -191,15 +211,29 @@ module BaseBeacon {
//= 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)
&& (bytes.Some? ==> ret.value.Some? && hash(bytes.value, key).Success? && ret.value.value == DDB.AttributeValue.S(hash(bytes.value, key).value))
&& (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)
if asSet then
var value := TermLoc.TermToAttr(loc, item, None);
if value.None? then
Success(None)
else
var value := value.value;
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(Some(DDB.AttributeValue.SS(beaconSeq)))
else
var res :- hash(bytes.value, key);
Success(Some(res))
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<Option<DDB.AttributeValue>, Error>
Expand All @@ -215,11 +249,71 @@ module BaseBeacon {
[loc[0].key]
}

function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes) : Result<DDB.AttributeValue, Error>
function method {:tailrecursion} BeaconizeStringSet(value : DDB.StringSetAttributeValue, key : Bytes, converted : seq<string> := [])
: Result<seq<string>, Error>
{
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
BeaconizeStringSet(value[1..], key, converted + [h])
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can DDB Sets contain duplicates? If so, isn't this collapsing them when calculating beacons? Would a customer want to be able to distinguish between [A, A, B] and [A, B]? Or are we accepting that this may be one of the "false positives" we filter out?

Is this behavior surprising to the customer, if they are trying to reason about the distribution of their data, and don't realize that the same beacon value will be created for the above example?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, sets are not supposed to contain duplicates. You made me add code to DynamoToStruct to fail if a set contains duplicates.

}

function method {:tailrecursion} BeaconizeNumberSet(value : DDB.StringSetAttributeValue, key : Bytes, converted : seq<string> := [])
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this be?

Suggested change
function method {:tailrecursion} BeaconizeNumberSet(value : DDB.StringSetAttributeValue, key : Bytes, converted : seq<string> := [])
function method {:tailrecursion} BeaconizeNumberSet(value : DDB.NumberSetAttributeValue, key : Bytes, converted : seq<string> := [])

Or does that not exist, and the number set just reuses the StringSetAttributeValue in DDB?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

They're the same type, but yes, that should be changed.

: Result<seq<string>, Error>
{
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
BeaconizeNumberSet(value[1..], key, converted + [h])
}

function method {:tailrecursion} BeaconizeBinarySet(value : DDB.BinarySetAttributeValue, key : Bytes, converted : seq<string> := [])
: Result<seq<string>, Error>
{
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
BeaconizeBinarySet(value[1..], key, converted + [h])
}

function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes)
: (ret : Result<DDB.AttributeValue, Error>)
//= 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
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)))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: We have this same error on L227, which to me implies that we could factor out similar logic in these two places. I recognize that there might be ergonomic/verification reasons that make this difficult though.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good call. Refactored.

};
Success(DDB.AttributeValue.SS(beaconSeq))
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
Expand Down
28 changes: 25 additions & 3 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,23 @@ module CompoundBeacon {
:: OkPrefixPair(x, y)
}

// Does these parts refer to `name`
predicate method {:tailrecursion} HasBeacon2(parts : seq<BeaconPart>, 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|
Expand Down Expand Up @@ -374,18 +391,23 @@ module CompoundBeacon {
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
//= type=implication
//# * This operation MUST take a record as input, and produce an optional string.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we make this change, the spec needs to update it's output type. But do we need to change the type here? Why not have this contain to work with strings, and callers to this method deal with unpacking attribute values?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed. Reverted.

function method {:opaque} hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap) : (res : Result<Option<string>, Error>)
function method {:opaque} hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap) : (res : Result<Option<DDB.AttributeValue>, Error>)
ensures res.Success? && res.value.Some? ==>
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
//= type=implication
//# * If a string is returned, it MUST NOT be empty.
&& |res.value.value| > 0
&& res.value.value.S?
&& |res.value.value.S| > 0
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
//= type=implication
//# * This operation MUST iterate through all constructors, in order, using the first that succeeds.
&& TryConstructors(construct, item, vf, keys).Success?
{
TryConstructors(construct, item, vf, keys)
var strVal :- TryConstructors(construct, item, vf, keys);
if strVal.Some? then
Success(Some(DDB.AttributeValue.S(strVal.value)))
else
Success(None)
}

// return the unhashed beacon value, necessary for final client-side filtering
Expand Down
Loading