Skip to content

Commit a1814ee

Browse files
ajewellamzajewellamz
committed
m
1 parent d622567 commit a1814ee

File tree

12 files changed

+287
-251
lines changed

12 files changed

+287
-251
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

Lines changed: 23 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ module BaseBeacon {
4343
//= specification/searchable-encryption/beacons.md#basichash
4444
//= type=implication
4545
//# * basicHash MUST take an [hmac key](./search-config.md#hmac-key-generation), a [beacon length](#beacon-length) and a sequence of bytes as input.
46-
function method {:opaque} hash(val : Bytes, key : Bytes, length : BeaconLength, bucket : Bytes)
46+
function method {:opaque} hash(val : Bytes, key : Bytes, length : BeaconLength, bucket : BucketBytes)
4747
: (ret : Result<string, Error>)
4848
ensures ret.Success? ==>
4949
//= specification/searchable-encryption/beacons.md#basichash
@@ -70,7 +70,7 @@ module BaseBeacon {
7070
}
7171

7272
// Get the standard hash for the UTF8 encoded representation of this string.
73-
function method {:opaque} hashStr(val : string, key : Bytes, length : BeaconLength, bucket : Bytes) : (res : Result<string, Error>)
73+
function method {:opaque} hashStr(val : string, key : Bytes, length : BeaconLength, bucket : BucketBytes) : (res : Result<string, Error>)
7474
ensures res.Success? ==> |res.value| > 0
7575
{
7676
var str := UTF8.Encode(val);
@@ -124,7 +124,7 @@ module BaseBeacon {
124124
var beaconName := BeaconPrefix + name;
125125
:- Need(DDB.IsValid_AttributeName(beaconName), E(beaconName + " is not a valid attribute name."));
126126
var numBuckets : nat := if numberOfBuckets.Some? then numberOfBuckets.value as nat else 0;
127-
:- Need(numBuckets < 256, E(beaconName + " has numberOfBuckets greater than 255"));
127+
// :- Need(numBuckets < 256, E(beaconName + " has numberOfBuckets greater than 255"));
128128
Success(StandardBeacon.StandardBeacon(
129129
BeaconBase (
130130
client := client,
@@ -136,7 +136,7 @@ module BaseBeacon {
136136
partOnly,
137137
asSet,
138138
share,
139-
numBuckets as uint8
139+
numBuckets as OptBucketCount
140140
))
141141
}
142142
datatype StandardBeacon = StandardBeacon (
@@ -146,21 +146,19 @@ module BaseBeacon {
146146
partOnly : bool,
147147
asSet : bool,
148148
share : Option<string>,
149-
numberOfBuckets : uint8
149+
numberOfBuckets : OptBucketCount
150150
) {
151-
function method constrained_bucket(bucket : Bytes) : Bytes
151+
152+
function method constrained_bucket(bucket : BucketNumber) : BucketBytes
152153
{
153-
SequenceIsSafeBecauseItIsInMemory(bucket);
154-
if numberOfBuckets == 0 || |bucket| as uint64 == 0 then
155-
bucket
154+
if numberOfBuckets == 0 || bucket == 0 then
155+
BucketNumberToBytes(bucket)
156156
else
157-
var newBucket : uint8 := bucket[0] % numberOfBuckets;
158-
if newBucket == 0 then
159-
[]
160-
else
161-
[newBucket]
157+
var newBucket : BucketNumber := (bucket as OptBucketCount % numberOfBuckets) as BucketNumber;
158+
BucketNumberToBytes(newBucket)
162159
}
163-
function method {:opaque} hash(val : Bytes, key : Bytes, bucket : Bytes)
160+
161+
function method {:opaque} hash(val : Bytes, key : Bytes, bucket : BucketNumber)
164162
: (ret : Result<string, Error>)
165163
ensures ret.Success? ==>
166164
&& |ret.value| > 0
@@ -188,7 +186,7 @@ module BaseBeacon {
188186
//= type=implication
189187
//# * string hash MUST take a string and some [key materials](./search-config.md#get-beacon-key-materials)
190188
//# as input, and produce a string as output.
191-
function method {:opaque} hashStr(val : string, keys : HmacKeyMap, bucket : Bytes) : (res : Result<string, Error>)
189+
function method {:opaque} hashStr(val : string, keys : HmacKeyMap, bucket : BucketNumber) : (res : Result<string, Error>)
192190
ensures res.Success? ==> |res.value| > 0
193191

194192
//= specification/searchable-encryption/beacons.md#string-hash
@@ -211,7 +209,7 @@ module BaseBeacon {
211209
hash(str.value, keys[keyName()], bucket)
212210
}
213211

214-
function method {:opaque} ValueToSet(value : DDB.AttributeValue, key : Bytes, bucket : Bytes) : (ret : Result<DDB.AttributeValue, Error>)
212+
function method {:opaque} ValueToSet(value : DDB.AttributeValue, key : Bytes, bucket : BucketNumber) : (ret : Result<DDB.AttributeValue, Error>)
215213
ensures ret.Success? ==> ret.value.SS?
216214
ensures !value.SS? && !value.NS? && !value.BS? ==> ret.Failure?
217215
ensures ret.Success? ==> HasNoDuplicates(ret.value.SS)
@@ -230,7 +228,7 @@ module BaseBeacon {
230228
//= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon
231229
//= type=implication
232230
//# * 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).
233-
function method {:opaque} getHash(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes, bucket : Bytes) : (ret : Result<Option<DDB.AttributeValue>, Error>)
231+
function method {:opaque} getHash(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes, bucket : BucketNumber) : (ret : Result<Option<DDB.AttributeValue>, Error>)
234232
//= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon
235233
//= type=implication
236234
//# * If this beacon is marked AsSet then this operation MUST return the
@@ -245,7 +243,7 @@ module BaseBeacon {
245243
getHashNonSet(item, vf, key, bucket)
246244
}
247245

248-
function method {:opaque} getHashSet(item : DDB.AttributeMap, key : Bytes, bucket : Bytes) : (ret : Result<Option<DDB.AttributeValue>, Error>)
246+
function method {:opaque} getHashSet(item : DDB.AttributeMap, key : Bytes, bucket : BucketNumber) : (ret : Result<Option<DDB.AttributeValue>, Error>)
249247
requires asSet
250248
ensures ret.Success? ==>
251249
//= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon
@@ -275,7 +273,7 @@ module BaseBeacon {
275273
var setValue :- ValueToSet(value.value, key, bucket);
276274
Success(Some(setValue))
277275
}
278-
function method {:opaque} getHashNonSet(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes, bucket : Bytes) : (ret : Result<Option<DDB.AttributeValue>, Error>)
276+
function method {:opaque} getHashNonSet(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes, bucket : BucketNumber) : (ret : Result<Option<DDB.AttributeValue>, Error>)
279277
requires !asSet
280278
ensures ret.Success? ==>
281279
//= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
@@ -321,7 +319,7 @@ module BaseBeacon {
321319
[loc[0].key]
322320
}
323321

324-
function method {:tailrecursion} BeaconizeStringSet(value : DDB.StringSetAttributeValue, key : Bytes, bucket : Bytes, converted : seq<string> := [])
322+
function method {:tailrecursion} BeaconizeStringSet(value : DDB.StringSetAttributeValue, key : Bytes, bucket : BucketNumber, converted : seq<string> := [])
325323
: (ret : Result<seq<string>, Error>)
326324
requires HasNoDuplicates(converted)
327325
ensures ret.Success? ==> HasNoDuplicates(ret.value)
@@ -338,7 +336,7 @@ module BaseBeacon {
338336
BeaconizeStringSet(value[1..], key, bucket, converted + [h])
339337
}
340338

341-
function method {:tailrecursion} BeaconizeNumberSet(value : DDB.NumberSetAttributeValue, key : Bytes, bucket : Bytes, converted : seq<string> := [])
339+
function method {:tailrecursion} BeaconizeNumberSet(value : DDB.NumberSetAttributeValue, key : Bytes, bucket : BucketNumber, converted : seq<string> := [])
342340
: (ret : Result<seq<string>, Error>)
343341
requires HasNoDuplicates(converted)
344342
ensures ret.Success? ==> HasNoDuplicates(ret.value)
@@ -355,7 +353,7 @@ module BaseBeacon {
355353
BeaconizeNumberSet(value[1..], key, bucket, converted + [h])
356354
}
357355

358-
function method {:tailrecursion} BeaconizeBinarySet(value : DDB.BinarySetAttributeValue, key : Bytes, bucket : Bytes, converted : seq<string> := [])
356+
function method {:tailrecursion} BeaconizeBinarySet(value : DDB.BinarySetAttributeValue, key : Bytes, bucket : BucketNumber, converted : seq<string> := [])
359357
: (ret : Result<seq<string>, Error>)
360358
requires HasNoDuplicates(converted)
361359
ensures ret.Success? ==> HasNoDuplicates(ret.value)
@@ -372,7 +370,7 @@ module BaseBeacon {
372370
BeaconizeBinarySet(value[1..], key, bucket, converted + [h])
373371
}
374372

375-
function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes, forContains : bool, bucket : Bytes)
373+
function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes, forContains : bool, bucket : BucketNumber)
376374
: (ret : Result<DDB.AttributeValue, Error>)
377375
{
378376
// in query, allow beaconization of terminals
@@ -389,7 +387,7 @@ module BaseBeacon {
389387
//= specification/searchable-encryption/beacons.md#getpart-for-a-standard-beacon
390388
//= type=implication
391389
//# * getPart MUST take an [hmac key](./search-config.md#hmac-key-generation), a sequence of bytes as input, and produce a string.
392-
function method {:opaque} getPart(val : Bytes, key : Bytes, bucket : Bytes)
390+
function method {:opaque} getPart(val : Bytes, key : Bytes, bucket : BucketBytes)
393391
: (ret : Result<string, Error>)
394392
requires 0 < |val|
395393

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -294,7 +294,7 @@ module CompoundBeacon {
294294
}
295295

296296
// calculate value for a single piece of a compound beacon query string
297-
function method FindAndCalcPart(value : string, keys : MaybeKeyMap, bucket : Bytes) : Result<string, Error>
297+
function method FindAndCalcPart(value : string, keys : MaybeKeyMap, bucket : BucketNumber) : Result<string, Error>
298298
requires !keys.DontUseKeys?
299299
{
300300
var part :- partFromPrefix(parts, value);
@@ -309,7 +309,7 @@ module CompoundBeacon {
309309
}
310310

311311
// for the given attribute value, return the beacon value
312-
function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool, bucket : Bytes) : Result<DDB.AttributeValue, Error>
312+
function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool, bucket : BucketNumber) : Result<DDB.AttributeValue, Error>
313313
requires !keys.DontUseKeys?
314314
{
315315
if !value.S? then
@@ -334,7 +334,7 @@ module CompoundBeacon {
334334
item : DDB.AttributeMap,
335335
vf : VirtualFieldMap,
336336
keys : MaybeKeyMap,
337-
bucket : Bytes,
337+
bucket : BucketNumber,
338338
acc : string := "")
339339
: (ret : Result<Option<string>, Error>)
340340
ensures ret.Success? && ret.value.Some? ==> |ret.value.value| > 0
@@ -374,7 +374,7 @@ module CompoundBeacon {
374374
item : DDB.AttributeMap,
375375
vf : VirtualFieldMap,
376376
keys : MaybeKeyMap,
377-
bucket : Bytes
377+
bucket : BucketNumber
378378
)
379379
: (ret : Result<Option<string>, Error>)
380380
ensures ret.Success? && ret.value.Some? ==> |ret.value.value| > 0
@@ -394,7 +394,7 @@ module CompoundBeacon {
394394
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
395395
//= type=implication
396396
//# * This operation MUST take a record as input, and produce an optional string.
397-
function method {:opaque} hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap, bucket : Bytes) : (res : Result<Option<string>, Error>)
397+
function method {:opaque} hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap, bucket : BucketNumber) : (res : Result<Option<string>, Error>)
398398
ensures res.Success? && res.value.Some? ==>
399399
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
400400
//= type=implication
@@ -409,7 +409,7 @@ module CompoundBeacon {
409409
}
410410

411411
// return the unhashed beacon value, necessary for final client-side filtering
412-
function method {:opaque} getNaked(item : DDB.AttributeMap, vf : VirtualFieldMap, bucket : Bytes) : (res : Result<Option<string>, Error>)
412+
function method {:opaque} getNaked(item : DDB.AttributeMap, vf : VirtualFieldMap, bucket : BucketNumber) : (res : Result<Option<string>, Error>)
413413
ensures res.Success? && res.value.Some? ==>
414414
&& |res.value.value| > 0
415415
{
@@ -444,7 +444,7 @@ module CompoundBeacon {
444444
//= specification/searchable-encryption/beacons.md#getpart-for-a-compound-beacon
445445
//= type=implication
446446
//# * getPart MUST take a string as input and produce a string.
447-
function method {:opaque} getPart(val : string, keys : HmacKeyMap, bucket : Bytes)
447+
function method {:opaque} getPart(val : string, keys : HmacKeyMap, bucket : BucketNumber)
448448
: (ret : Result<string, Error>)
449449
//= specification/searchable-encryption/beacons.md#getpart-for-a-compound-beacon
450450
//= type=implication
@@ -465,7 +465,7 @@ module CompoundBeacon {
465465
calcParts(pieces, keys, bucket)
466466
}
467467

468-
function method calcPart(piece : string, keys : HmacKeyMap, bucket : Bytes)
468+
function method calcPart(piece : string, keys : HmacKeyMap, bucket : BucketNumber)
469469
: (ret : Result<string, Error>)
470470

471471
ensures ret.Success? ==>
@@ -486,7 +486,7 @@ module CompoundBeacon {
486486
PartValueCalc(piece, Keys(keys), thePart, bucket)
487487
}
488488

489-
function method calcParts(pieces : seq<string>, keys : HmacKeyMap, bucket : Bytes, acc : string := [])
489+
function method calcParts(pieces : seq<string>, keys : HmacKeyMap, bucket : BucketNumber, acc : string := [])
490490
: (ret : Result<string, Error>)
491491
requires |pieces| > 0 || |acc| > 0
492492
ensures ret.Success? ==> |ret.value| > 0
@@ -570,7 +570,7 @@ module CompoundBeacon {
570570
//# Part Value Calculation MUST take some [key materials](./search-config.md#get-beacon-key-materials),
571571
//# a string (the value for which the beacon is being calculated)
572572
//# and a [Part](#part) as input, and return a string as output.
573-
function method {:opaque} PartValueCalc(data : string, keys : MaybeKeyMap, part : BeaconPart, bucket : Bytes)
573+
function method {:opaque} PartValueCalc(data : string, keys : MaybeKeyMap, part : BeaconPart, bucket : BucketNumber)
574574
: (ret : Result<string, Error>)
575575
requires !keys.DontUseKeys?
576576

0 commit comments

Comments
 (0)