Skip to content

Commit 1388574

Browse files
ajewellamzajewellamz
committed
m
1 parent 90822df commit 1388574

File tree

34 files changed

+1575
-143
lines changed

34 files changed

+1575
-143
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy‎

Lines changed: 79 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,76 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
5555
}
5656
type BucketCount = x: int32 | IsValid_BucketCount(x) witness *
5757
predicate method IsValid_BucketCount(x: int32) {
58-
( 1 <= x )
58+
( 1 <= x <= 255 )
59+
}
60+
type BucketNumber = x: int32 | IsValid_BucketNumber(x) witness *
61+
predicate method IsValid_BucketNumber(x: int32) {
62+
( 0 <= x <= 254 )
63+
}
64+
class IBucketSelectorCallHistory {
65+
ghost constructor() {
66+
GetBucketNumber := [];
67+
}
68+
ghost var GetBucketNumber: seq<DafnyCallEvent<GetBucketNumberInput, Result<GetBucketNumberOutput, Error>>>
69+
}
70+
trait {:termination false} IBucketSelector
71+
{
72+
// Helper to define any additional modifies/reads clauses.
73+
// If your operations need to mutate state,
74+
// add it in your constructor function:
75+
// Modifies := {your, fields, here, History};
76+
// If you do not need to mutate anything:
77+
// Modifies := {History};
78+
79+
ghost const Modifies: set<object>
80+
// For an unassigned field defined in a trait,
81+
// Dafny can only assign a value in the constructor.
82+
// This means that for Dafny to reason about this value,
83+
// it needs some way to know (an invariant),
84+
// about the state of the object.
85+
// This builds on the Valid/Repr paradigm
86+
// To make this kind requires safe to add
87+
// to methods called from unverified code,
88+
// the predicate MUST NOT take any arguments.
89+
// This means that the correctness of this requires
90+
// MUST only be evaluated by the class itself.
91+
// If you require any additional mutation,
92+
// then you MUST ensure everything you need in ValidState.
93+
// You MUST also ensure ValidState in your constructor.
94+
predicate ValidState()
95+
ensures ValidState() ==> History in Modifies
96+
ghost const History: IBucketSelectorCallHistory
97+
predicate GetBucketNumberEnsuresPublicly(input: GetBucketNumberInput , output: Result<GetBucketNumberOutput, Error>)
98+
// The public method to be called by library consumers
99+
method GetBucketNumber ( input: GetBucketNumberInput )
100+
returns (output: Result<GetBucketNumberOutput, Error>)
101+
requires
102+
&& ValidState()
103+
modifies Modifies - {History} ,
104+
History`GetBucketNumber
105+
// Dafny will skip type parameters when generating a default decreases clause.
106+
decreases Modifies - {History}
107+
ensures
108+
&& ValidState()
109+
ensures GetBucketNumberEnsuresPublicly(input, output)
110+
ensures History.GetBucketNumber == old(History.GetBucketNumber) + [DafnyCallEvent(input, output)]
111+
{
112+
output := GetBucketNumber' (input);
113+
History.GetBucketNumber := History.GetBucketNumber + [DafnyCallEvent(input, output)];
114+
}
115+
// The method to implement in the concrete class.
116+
method GetBucketNumber' ( input: GetBucketNumberInput )
117+
returns (output: Result<GetBucketNumberOutput, Error>)
118+
requires
119+
&& ValidState()
120+
modifies Modifies - {History}
121+
// Dafny will skip type parameters when generating a default decreases clause.
122+
decreases Modifies - {History}
123+
ensures
124+
&& ValidState()
125+
ensures GetBucketNumberEnsuresPublicly(input, output)
126+
ensures unchanged(History)
127+
59128
}
60129
type Char = x: string | IsValid_Char(x) witness *
61130
predicate method IsValid_Char(x: string) {
@@ -250,7 +319,8 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
250319
nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring> := Option.None ,
251320
nameonly cmm: Option<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager> := Option.None ,
252321
nameonly legacyOverride: Option<LegacyOverride> := Option.None ,
253-
nameonly plaintextOverride: Option<PlaintextOverride> := Option.None
322+
nameonly plaintextOverride: Option<PlaintextOverride> := Option.None ,
323+
nameonly bucketSelector: Option<IBucketSelector> := Option.None
254324
)
255325
type DynamoDbTableEncryptionConfigList = map<ComAmazonawsDynamodbTypes.TableName, DynamoDbTableEncryptionConfig>
256326
datatype DynamoDbTablesEncryptionConfig = | DynamoDbTablesEncryptionConfig (
@@ -277,6 +347,13 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
277347
datatype GetBranchKeyIdFromDdbKeyOutput = | GetBranchKeyIdFromDdbKeyOutput (
278348
nameonly branchKeyId: string
279349
)
350+
datatype GetBucketNumberInput = | GetBucketNumberInput (
351+
nameonly item: ComAmazonawsDynamodbTypes.AttributeMap ,
352+
nameonly numberOfBuckets: BucketCount
353+
)
354+
datatype GetBucketNumberOutput = | GetBucketNumberOutput (
355+
nameonly bucketNumber: BucketNumber
356+
)
280357
datatype GetEncryptedDataKeyDescriptionInput = | GetEncryptedDataKeyDescriptionInput (
281358
nameonly input: GetEncryptedDataKeyDescriptionUnion
282359
)

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy‎

Lines changed: 32 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,30 @@ service DynamoDbEncryption {
4949
errors: [ DynamoDbEncryptionException ]
5050
}
5151

52+
resource BucketSelector {
53+
operations: [GetBucketNumber]
54+
}
55+
56+
@reference(resource: BucketSelector)
57+
structure BucketSelectorReference {}
58+
59+
operation GetBucketNumber {
60+
input: GetBucketNumberInput,
61+
output: GetBucketNumberOutput,
62+
}
63+
64+
structure GetBucketNumberInput {
65+
@required
66+
item: AttributeMap,
67+
@required
68+
numberOfBuckets : BucketCount
69+
}
70+
71+
structure GetBucketNumberOutput {
72+
@required
73+
bucketNumber: BucketNumber
74+
}
75+
5276
@javadoc("Returns encrypted data key description.")
5377
operation GetEncryptedDataKeyDescription {
5478
input: GetEncryptedDataKeyDescriptionInput,
@@ -206,7 +230,10 @@ structure DynamoDbTableEncryptionConfig {
206230
@javadoc("A configuration that override encryption and/or decryption to instead perform legacy encryption and/or decryption. Used as part of migration from version 2.x to version 3.x.")
207231
legacyOverride: LegacyOverride,
208232
@javadoc("A configuration that override encryption and/or decryption to instead passthrough and write and/or read plaintext. Used to update plaintext tables to fully use client-side encryption.")
209-
plaintextOverride: PlaintextOverride
233+
plaintextOverride: PlaintextOverride,
234+
235+
@javadoc("How to choose the bucket for an item. Default behavior is a random between 0 and numberOfBuckets.")
236+
bucketSelector: BucketSelectorReference,
210237
}
211238

212239
map AttributeActions {
@@ -286,9 +313,12 @@ integer BeaconBitLength
286313
@range(min: 1)
287314
integer VersionNumber
288315

289-
@range(min: 1)
316+
@range(min: 1, max: 255)
290317
integer BucketCount
291318

319+
@range(min: 0, max: 254)
320+
integer BucketNumber
321+
292322
@length(min: 1, max: 1)
293323
string Char
294324

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

Lines changed: 20 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ module BaseBeacon {
1515
import opened DynamoDbEncryptionUtil
1616
import opened DdbVirtualFields
1717
import opened Seq
18+
import opened StandardLibrary.MemoryMath
1819
import DynamoToStruct
1920

2021
import DDB = ComAmazonawsDynamodbTypes
@@ -111,7 +112,8 @@ module BaseBeacon {
111112
loc : string,
112113
partOnly : bool,
113114
asSet : bool,
114-
share : Option<string>
115+
share : Option<string>,
116+
numberOfBuckets : Option<BucketCount>
115117
)
116118
: (ret : Result<ValidStandardBeacon, Error>)
117119
ensures ret.Success? ==>
@@ -121,6 +123,8 @@ module BaseBeacon {
121123
var termLoc :- TermLoc.MakeTermLoc(loc);
122124
var beaconName := BeaconPrefix + name;
123125
:- Need(DDB.IsValid_AttributeName(beaconName), E(beaconName + " is not a valid attribute name."));
126+
var numBuckets : nat := if numberOfBuckets.Some? then numberOfBuckets.value as nat else 0;
127+
:- Need(numBuckets < 256, E(beaconName + " has numberOfBuckets greater than 255"));
124128
Success(StandardBeacon.StandardBeacon(
125129
BeaconBase (
126130
client := client,
@@ -131,7 +135,8 @@ module BaseBeacon {
131135
termLoc,
132136
partOnly,
133137
asSet,
134-
share
138+
share,
139+
numBuckets as uint8
135140
))
136141
}
137142
datatype StandardBeacon = StandardBeacon (
@@ -140,18 +145,27 @@ module BaseBeacon {
140145
loc : TermLoc.TermLoc,
141146
partOnly : bool,
142147
asSet : bool,
143-
share : Option<string>
148+
share : Option<string>,
149+
numberOfBuckets : uint8
144150
) {
151+
function method constrained_bucket(bucket : Bytes) : Bytes
152+
{
153+
SequenceIsSafeBecauseItIsInMemory(bucket);
154+
if numberOfBuckets == 0 || |bucket| as uint64 == 0 then
155+
bucket
156+
else
157+
[bucket[0] % numberOfBuckets]
158+
}
145159
function method {:opaque} hash(val : Bytes, key : Bytes, bucket : Bytes)
146160
: (ret : Result<string, Error>)
147161
ensures ret.Success? ==>
148162
&& |ret.value| > 0
149-
&& base.hash(val, key, length, bucket).Success?
150-
&& ret.value == base.hash(val, key, length, bucket).value
163+
&& base.hash(val, key, length, constrained_bucket(bucket)).Success?
164+
&& ret.value == base.hash(val, key, length, constrained_bucket(bucket)).value
151165

152166
&& |ret.value| == (((length as uint8) + 3) / 4) as nat
153167
{
154-
base.hash(val, key, length, bucket)
168+
base.hash(val, key, length, constrained_bucket(bucket))
155169
}
156170

157171
// return the name of the hmac key to use

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -526,6 +526,18 @@ module SearchConfigToInfo {
526526
Failure(E("Beacon " + name + " is shared to " + share + " which is not defined."))
527527
}
528528

529+
predicate method BucketConstraintOk(outer : DynamoDbTableEncryptionConfig, inner : Option<BucketCount>)
530+
{
531+
if inner.None? || outer.search.None? || |outer.search.value.versions| == 0 then
532+
true
533+
else
534+
var num := outer.search.value.versions[0].numberOfBuckets;
535+
if num.None? then
536+
false
537+
else
538+
inner.value < num.value
539+
}
540+
529541
// convert configured StandardBeacons to internal Beacons
530542
method {:tailrecursion} AddStandardBeacons(
531543
beacons : seq<StandardBeacon>,
@@ -588,10 +600,10 @@ module SearchConfigToInfo {
588600
//# A SharedSet Beacon MUST behave both as [Shared](#shared-initialization) and [AsSet](#asset-initialization).
589601
case sharedSet(t) => share := Some(t.other); isAsSet := true;
590602
}
591-
592603
}
604+
:- Need(BucketConstraintOk(outer, beacons[0].numberOfBuckets), E("Constrained numberOfBuckets for " + beacons[0].name + " must be less than the global numberOfBuckets."));
593605
var newBeacon :- B.MakeStandardBeacon(client, beacons[0].name, beacons[0].length as B.BeaconLength, locString,
594-
isPartOnly, isAsSet, share);
606+
isPartOnly, isAsSet, share, beacons[0].numberOfBuckets);
595607

596608
//= specification/searchable-encryption/search-config.md#beacon-version-initialization
597609
//# Initialization MUST fail if the [terminal location](virtual.md#terminal-location)

0 commit comments

Comments
 (0)