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 2 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
125 changes: 87 additions & 38 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -193,41 +193,87 @@ module BaseBeacon {
hash(str.value, keys[keyName()])
}

function method {:opaque} ValueToSet(value : DDB.AttributeValue, key : Bytes) : (ret : Result<DDB.AttributeValue, Error>)
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<string>([]);
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.
//# * 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<Option<DDB.AttributeValue>, Error>)
ensures ret.Success? && !asSet ==>
&& 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 == 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))
//= 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)
{
if asSet then
getHashSet(item, key)
else
getHashNonSet(item, vf, key)
}

function method {:opaque} getHashSet(item : DDB.AttributeMap, key : Bytes) : (ret : Result<Option<DDB.AttributeValue>, 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 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 setValue :- ValueToSet(value.value, key);
Success(Some(setValue))
}
function method {:opaque} getHashNonSet(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes) : (ret : Result<Option<DDB.AttributeValue>, 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)
Expand All @@ -250,7 +296,9 @@ module BaseBeacon {
}

function method {:tailrecursion} BeaconizeStringSet(value : DDB.StringSetAttributeValue, key : Bytes, converted : seq<string> := [])
: Result<seq<string>, Error>
: (ret : Result<seq<string>, Error>)
requires HasNoDuplicates(converted)
ensures ret.Success? ==> HasNoDuplicates(ret.value)
{
if |value| == 0 then
Success(converted)
Expand All @@ -260,11 +308,14 @@ module BaseBeacon {
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.StringSetAttributeValue, key : Bytes, converted : seq<string> := [])
: Result<seq<string>, Error>
function method {:tailrecursion} BeaconizeNumberSet(value : DDB.NumberSetAttributeValue, key : Bytes, converted : seq<string> := [])
: (ret : Result<seq<string>, Error>)
requires HasNoDuplicates(converted)
ensures ret.Success? ==> HasNoDuplicates(ret.value)
{
if |value| == 0 then
Success(converted)
Expand All @@ -274,11 +325,14 @@ module BaseBeacon {
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<string> := [])
: Result<seq<string>, Error>
: (ret : Result<seq<string>, Error>)
requires HasNoDuplicates(converted)
ensures ret.Success? ==> HasNoDuplicates(ret.value)
{
if |value| == 0 then
Success(converted)
Expand All @@ -288,6 +342,7 @@ module BaseBeacon {
if h in converted then
BeaconizeBinarySet(value[1..], key, converted)
else
reveal HasNoDuplicates();
BeaconizeBinarySet(value[1..], key, converted + [h])
}

Expand All @@ -303,13 +358,7 @@ module BaseBeacon {
//# * 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)))
};
Success(DDB.AttributeValue.SS(beaconSeq))
ValueToSet(value, key)
else
var bytes :- DynamoToStruct.TopLevelAttributeToBytes(value).MapFailure(e => E(e));
var h :- hash(bytes, key);
Expand Down
11 changes: 3 additions & 8 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -391,23 +391,18 @@ 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<DDB.AttributeValue>, Error>)
function method {:opaque} hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap) : (res : Result<Option<string>, 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.S?
&& |res.value.value.S| > 0
&& |res.value.value| > 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?
{
var strVal :- TryConstructors(construct, item, vf, keys);
if strVal.Some? then
Success(Some(DDB.AttributeValue.S(strVal.value)))
else
Success(None)
TryConstructors(construct, item, vf, keys)
}

// return the unhashed beacon value, necessary for final client-side filtering
Expand Down
46 changes: 19 additions & 27 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -386,24 +386,24 @@ module SearchConfigToInfo {
Some(badSeq[0])
}

function method IsValidTwin(converted : I.BeaconMap, name : string, length : BeaconBitLength, twin : string)
function method IsValidTwin(converted : I.BeaconMap, name : string, length : B.BeaconLength, twin : string)
: (ret : Result<bool, Error>)
ensures ret.Success? ==>
&& twin in converted
&& converted[twin].Standard?
&& converted[twin].std.length as BeaconBitLength == length
&& converted[twin].std.length == length
{
if twin in converted then
if converted[twin].Standard? then
if converted[twin].std.length as BeaconBitLength == length 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 + " but " + twin + " has not yet been defined."))
Failure(E("Beacon " + name + " is twinned to " + twin + " which is not defined."))
}

// convert configured StandardBeacons to internal Beacons
Expand Down Expand Up @@ -449,26 +449,6 @@ module SearchConfigToInfo {
//# Initialization MUST fail if a virtual field is defined with only one location,
//# and also a [standard beacon](beacons.md#standard-beacon) is defined with that same location.
&& FindVirtualFieldWithThisLocation(virtualFields, {loc}).None?

ensures output.Success? && 0 < |beacons| && beacons[0].style.Some? && beacons[0].style.value.twinned? ==>
&& var twin := beacons[0].style.value.twinned.other;
&& IsValidTwin(converted, beacons[0].name, beacons[0].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 converted
&& converted[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).
&& converted[twin].std.length as BeaconBitLength == beacons[0].length

ensures output.Success? && 0 < |beacons| && beacons[0].style.Some? && beacons[0].style.value.twinnedSet? ==>
&& var twin := beacons[0].style.value.twinnedSet.other;
&& IsValidTwin(converted, beacons[0].name, beacons[0].length, twin).Success?
&& twin in converted
&& converted[twin].Standard?
&& converted[twin].std.length as BeaconBitLength == beacons[0].length
{
if |beacons| == 0 {
return Success(converted);
Expand All @@ -490,9 +470,6 @@ module SearchConfigToInfo {
}

}
if twin.Some? {
var _ :- IsValidTwin(converted, beacons[0].name, beacons[0].length, twin.value);
}
var newBeacon :- B.MakeStandardBeacon(client, beacons[0].name, beacons[0].length as B.BeaconLength, locString,
isPartOnly, isAsSet, twin);

Expand Down Expand Up @@ -891,13 +868,28 @@ module SearchConfigToInfo {
//= 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)
}
Expand Down
6 changes: 5 additions & 1 deletion DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -400,7 +400,11 @@ module SearchableEncryptionInfo {
else
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<Option<DDB.AttributeValue>, Error>
{
Expand Down
Loading