feat: implement beacon styles #441

ajewellamz · 2023-09-21T13:55:59Z

Issue #, if available:

Description of changes:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

lavaleri

Doesn't have to be a part of this PR, but we need to add examples for each of these beacon styles. It's not immediately clear when/for what use cases a customers would want to utilize these options.

lavaleri · 2023-09-21T17:11:09Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

      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.


Need to update the spec with the new output type

lavaleri · 2023-09-21T17:12:04Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

-    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 ==>


Can we add specification for if it is asSet?

lavaleri · 2023-09-21T17:55:41Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

+        if h in converted then
+          BeaconizeStringSet(value[1..], key, converted)
+        else
+          BeaconizeStringSet(value[1..], key, converted + [h])


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?

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

lavaleri · 2023-09-21T17:57:14Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

+          BeaconizeStringSet(value[1..], key, converted + [h])
+    }
+
+    function method {:tailrecursion} BeaconizeNumberSet(value : DDB.StringSetAttributeValue, key : Bytes, converted : seq<string> := [])


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?

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

lavaleri · 2023-09-21T18:00:57Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy

@@ -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.


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?

Agreed. Reverted.

lavaleri · 2023-09-21T18:11:23Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

+  // Are all beacons internally consistent?
+  function method CheckBeacons(data : I.BeaconMap) : Result<bool, Error>
+  {
+    var beaconNames := SortedSets.ComputeSetToOrderedSequence2(data.Keys, CharLess);


Why do we sort the beacons?

We don't need to sort them, we just need to iterate over all the items in a map, and this is the only way I know to do that in a function.

lavaleri · 2023-09-21T18:24:50Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

+          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)))


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.

Good call. Refactored.

lavaleri · 2023-09-21T18:26:06Z

DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

+    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.");


Since we return this error in two places, it is not clear to me which code path this test case is exercising. Is it possible to test both code paths?

Done. This tested on the Write path, added test on the Query path.

lavaleri · 2023-09-21T18:27:08Z

DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

+    expect bv.error == E("Beacon twinBeacon is twinned to DoesNotExist but DoesNotExist has not yet been defined.");
+  }
+
+  method {:test} TwinnedBadLength()


What about testing that we throw the right error is configured with a compound beacon?

lavaleri · 2023-09-21T18:28:23Z

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

    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."))


I think we are missing a test for this case?

lavaleri · 2023-09-22T17:10:00Z

DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

+    expect bv.error == E("Beacon twinBeacon is twinned to NameTitle but NameTitle is a compound beacon.");
+  }
+
+  method {:test} TwinnedToCompound()


nit: name of this test appears to be swapped with L305

* feat: implement beacon styles

feat: implement beacon styles

bec4194

ajewellamz requested a review from a team as a code owner September 21, 2023 13:56

ajewellamz added 2 commits September 21, 2023 10:05

m

14652ab

m

fe66f4a

lavaleri reviewed Sep 21, 2023

View reviewed changes

ajewellamz added 2 commits September 21, 2023 16:56

respond to PR feedback

e8e7928

update spec

6c67bba

lavaleri reviewed Sep 22, 2023

View reviewed changes

m

ae3e691

lavaleri approved these changes Sep 22, 2023

View reviewed changes

ajewellamz merged commit 470eff9 into main Sep 22, 2023

ajewellamz deleted the beacon-styles branch September 22, 2023 18:09

ajewellamz added a commit that referenced this pull request Nov 14, 2023

feat: implement beacon styles (#441)

7b2a135

* feat: implement beacon styles

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: implement beacon styles #441

feat: implement beacon styles #441

ajewellamz commented Sep 21, 2023

lavaleri left a comment

lavaleri Sep 21, 2023

ajewellamz Sep 22, 2023

lavaleri Sep 21, 2023

lavaleri Sep 21, 2023

ajewellamz Sep 21, 2023

lavaleri Sep 21, 2023

ajewellamz Sep 21, 2023

lavaleri Sep 21, 2023

ajewellamz Sep 22, 2023

lavaleri Sep 21, 2023

ajewellamz Sep 21, 2023

lavaleri Sep 21, 2023

ajewellamz Sep 21, 2023

lavaleri Sep 21, 2023

ajewellamz Sep 21, 2023

lavaleri Sep 21, 2023

ajewellamz Sep 21, 2023

lavaleri Sep 21, 2023

ajewellamz Sep 21, 2023

lavaleri Sep 22, 2023

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

feat: implement beacon styles #441

feat: implement beacon styles #441

Conversation

ajewellamz commented Sep 21, 2023

lavaleri left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment