Skip to content

Commit 9b2e41c

Browse files
ajewellamzajewellamz
authored
feat: error on query with impossible compound beacons (#417)
1 parent 26f3eba commit 9b2e41c

File tree

2 files changed

+121
-2
lines changed

2 files changed

+121
-2
lines changed

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

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,83 @@ module CompoundBeacon {
153153
partFromPrefix(parts, value)
154154
}
155155

156+
function method PartsToString(p : seq<BeaconPart>) : string
157+
{
158+
var beaconParts := Seq.Map((s : BeaconPart) => s.getPrefix(), p);
159+
if |beaconParts| == 0 then
160+
""
161+
else
162+
Join(beaconParts, "")
163+
}
164+
165+
function method CPartToString(s : ConstructorPart) : string
166+
{
167+
if s.required then
168+
s.part.getPrefix()
169+
else
170+
"[" + s.part.getPrefix() + "]"
171+
}
172+
173+
function method CPartsToString(p : seq<ConstructorPart>) : string
174+
{
175+
var beaconParts := Seq.Map((s : ConstructorPart) => CPartToString(s), p);
176+
if |beaconParts| == 0 then
177+
""
178+
else
179+
Join(beaconParts, "")
180+
}
181+
182+
function method CListToString(p : ConstructorList) : string
183+
{
184+
var beaconParts := Seq.Map((s : Constructor) => CPartsToString(s.parts), p);
185+
Join(beaconParts, ", ")
186+
}
187+
188+
// Can this constructor produce this list of parts?
189+
// e.g. if the constructor has A_.B_ then
190+
// these are ok : A_foo, B_foo, A_foo.B_foo
191+
// these are bad : B_foo.A_foo, A_foo.A_foo
192+
// that is, we can skip a arbitrary number of parts,
193+
// but once we match a part, the rest of inParts must be able to directly follow
194+
predicate method CanConstruct(con : seq<ConstructorPart>, inParts : seq<BeaconPart>, matched : bool := false)
195+
{
196+
if |inParts| == 0 then
197+
true
198+
else if |con| == 0 then
199+
false
200+
else if con[0].part == inParts[0] then
201+
CanConstruct(con[1..], inParts[1..], true)
202+
else if !con[0].required || !matched then
203+
CanConstruct(con[1..], inParts, matched)
204+
else
205+
false
206+
}
207+
208+
// Fail unless one of these constructor can make a beacon composed of this sequence of parts
209+
predicate method {:tailrecursion} IsValidPartOrder(candidates : seq<Constructor>, inParts : seq<BeaconPart>)
210+
{
211+
if |candidates| == 0 then
212+
false
213+
else if CanConstruct(candidates[0].parts, inParts) then
214+
true
215+
else
216+
IsValidPartOrder(candidates[1..], inParts)
217+
}
218+
219+
// Fail unless it is possible to construct a beacon composed of this sequence of parts
220+
function method ValidatePartOrder(inParts : seq<BeaconPart>, orig : string) : Result<bool, Error>
221+
{
222+
if IsValidPartOrder(construct, inParts) then
223+
Success(true)
224+
else
225+
var msg :=
226+
"Compound Beacon value '" + orig +
227+
"' cannot be constructed from any available constructor for " + base.name +
228+
" value parsed as " + PartsToString(inParts) +
229+
" available constructors are " + CListToString(construct) + ".";
230+
Failure(E(msg))
231+
}
232+
156233
// find the part whose prefix matches this value
157234
function method {:tailrecursion} partFromPrefix(p : seq<BeaconPart>, value : string)
158235
: (ret : Result<BeaconPart, Error>)
@@ -221,6 +298,8 @@ module CompoundBeacon {
221298
Failure(E("CompoundBeacon " + base.name + " can only be queried as a string, not as " + AttrTypeToStr(value)))
222299
else
223300
var parts := Split(value.S, split);
301+
var partsUsed :- Seq.MapWithResult(s => getPartFromPrefix(s), parts);
302+
var _ :- ValidatePartOrder(partsUsed, value.S);
224303
var beaconParts :- Seq.MapWithResult(s => FindAndCalcPart(s, keys), parts);
225304
var lastIsPrefix :- justPrefix(Seq.Last(parts));
226305
if !forEquality && lastIsPrefix then

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

Lines changed: 42 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -157,6 +157,46 @@ module TestBaseBeacon {
157157
}
158158

159159

160+
method {:test} TestCompoundQueries() {
161+
var context := ExprContext (
162+
None,
163+
Some("Mixed = :mixed"),
164+
None,
165+
None
166+
);
167+
var version := GetLotsaBeacons();
168+
var src := GetLiteralSource([1,2,3,4,5], version);
169+
var beaconVersion :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
170+
171+
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName.Y_1984")]));
172+
var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
173+
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName")]));
174+
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
175+
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("Y_1984")]));
176+
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
177+
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("T_foo")]));
178+
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
179+
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("M_bar")]));
180+
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
181+
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("T_foo.M_bar")]));
182+
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
183+
184+
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName.N_MyName")]));
185+
var badContext := Beaconize(beaconVersion, context, DontUseKeyId);
186+
expect badContext.Failure?;
187+
expect badContext.error == E("Compound Beacon value 'N_MyName.N_MyName' cannot be constructed from any available constructor for Mixed value parsed as N_N_ available constructors are N_Y_, T_[M_].");
188+
189+
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("Y_1984.N_MyName")]));
190+
badContext := Beaconize(beaconVersion, context, DontUseKeyId);
191+
expect badContext.Failure?;
192+
expect badContext.error == E("Compound Beacon value 'Y_1984.N_MyName' cannot be constructed from any available constructor for Mixed value parsed as Y_N_ available constructors are N_Y_, T_[M_].");
193+
194+
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("M_bar.T_foo")]));
195+
badContext := Beaconize(beaconVersion, context, DontUseKeyId);
196+
expect badContext.Failure?;
197+
expect badContext.error == E("Compound Beacon value 'M_bar.T_foo' cannot be constructed from any available constructor for Mixed value parsed as M_T_ available constructors are N_Y_, T_[M_].");
198+
}
199+
160200
method {:test} TestQueryBeacons() {
161201
var context := ExprContext (
162202
None,
@@ -173,7 +213,7 @@ module TestBaseBeacon {
173213
":NameTitle" := DDB.AttributeValue.S("N_MyName.T_MyTitle"),
174214
":NameTitleN" := DDB.AttributeValue.S("N_MyName"),
175215
":NameTitleT" := DDB.AttributeValue.S("T_MyTitle"),
176-
":NameTitleTN" := DDB.AttributeValue.S("T_MyTitle.N_MyName"),
216+
":NameTitleTN" := DDB.AttributeValue.S("N_MyName.T_MyTitle"),
177217
":NameTitleField" := DDB.AttributeValue.S("MyName__mytitle"),
178218
":YearName" := DDB.AttributeValue.S("Y_1984.N_MyName")
179219
]),
@@ -187,7 +227,7 @@ module TestBaseBeacon {
187227
":Mixed" := DDB.AttributeValue.S("N_" + Name_beacon + ".Y_1984"),
188228
":Name" := DDB.AttributeValue.S(Name_beacon),
189229
":NameTitle" := DDB.AttributeValue.S("N_" + Name_beacon + ".T_" + Title_beacon),
190-
":NameTitleTN" := DDB.AttributeValue.S("T_" + Title_beacon + ".N_" + Name_beacon),
230+
":NameTitleTN" := DDB.AttributeValue.S("N_" + Name_beacon + ".T_" + Title_beacon),
191231
":NameTitleN" := DDB.AttributeValue.S("N_" + Name_beacon),
192232
":NameTitleT" := DDB.AttributeValue.S("T_" + Title_beacon),
193233
":NameTitleField" := DDB.AttributeValue.S(NameTitle_beacon),

0 commit comments

Comments
 (0)