Skip to content

feat: error on query with impossible compound beacons #417

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 1 commit into from
Sep 14, 2023
Merged

feat: error on query with impossible compound beacons #417

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
79 changes: 79 additions & 0 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,83 @@ module CompoundBeacon {
partFromPrefix(parts, value)
}

function method PartsToString(p : seq<BeaconPart>) : string
{
var beaconParts := Seq.Map((s : BeaconPart) => s.getPrefix(), p);
if |beaconParts| == 0 then
""
else
Join(beaconParts, "")
}

function method CPartToString(s : ConstructorPart) : string
{
if s.required then
s.part.getPrefix()
else
"[" + s.part.getPrefix() + "]"
}

function method CPartsToString(p : seq<ConstructorPart>) : string
{
var beaconParts := Seq.Map((s : ConstructorPart) => CPartToString(s), p);
if |beaconParts| == 0 then
""
else
Join(beaconParts, "")
}

function method CListToString(p : ConstructorList) : string
{
var beaconParts := Seq.Map((s : Constructor) => CPartsToString(s.parts), p);
Join(beaconParts, ", ")
}

// Can this constructor produce this list of parts?
// e.g. if the constructor has A_.B_ then
// these are ok : A_foo, B_foo, A_foo.B_foo
// these are bad : B_foo.A_foo, A_foo.A_foo
// that is, we can skip a arbitrary number of parts,
// but once we match a part, the rest of inParts must be able to directly follow
predicate method CanConstruct(con : seq<ConstructorPart>, inParts : seq<BeaconPart>, matched : bool := false)
{
if |inParts| == 0 then
true
else if |con| == 0 then
false
else if con[0].part == inParts[0] then
CanConstruct(con[1..], inParts[1..], true)
else if !con[0].required || !matched then
CanConstruct(con[1..], inParts, matched)
else
false
}

// Fail unless one of these constructor can make a beacon composed of this sequence of parts
predicate method {:tailrecursion} IsValidPartOrder(candidates : seq<Constructor>, inParts : seq<BeaconPart>)
{
if |candidates| == 0 then
false
else if CanConstruct(candidates[0].parts, inParts) then
true
else
IsValidPartOrder(candidates[1..], inParts)
}

// Fail unless it is possible to construct a beacon composed of this sequence of parts
function method ValidatePartOrder(inParts : seq<BeaconPart>, orig : string) : Result<bool, Error>
{
if IsValidPartOrder(construct, inParts) then
Success(true)
else
var msg :=
"Compound Beacon value '" + orig +
"' cannot be constructed from any available constructor for " + base.name +
" value parsed as " + PartsToString(inParts) +
" available constructors are " + CListToString(construct) + ".";
Failure(E(msg))
}

// find the part whose prefix matches this value
function method {:tailrecursion} partFromPrefix(p : seq<BeaconPart>, value : string)
: (ret : Result<BeaconPart, Error>)
Expand Down Expand Up @@ -221,6 +298,8 @@ module CompoundBeacon {
Failure(E("CompoundBeacon " + base.name + " can only be queried as a string, not as " + AttrTypeToStr(value)))
else
var parts := Split(value.S, split);
var partsUsed :- Seq.MapWithResult(s => getPartFromPrefix(s), parts);
var _ :- ValidatePartOrder(partsUsed, value.S);
var beaconParts :- Seq.MapWithResult(s => FindAndCalcPart(s, keys), parts);
var lastIsPrefix :- justPrefix(Seq.Last(parts));
if !forEquality && lastIsPrefix then
Expand Down
44 changes: 42 additions & 2 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,6 +157,46 @@ module TestBaseBeacon {
}


method {:test} TestCompoundQueries() {
var context := ExprContext (
None,
Some("Mixed = :mixed"),
None,
None
);
var version := GetLotsaBeacons();
var src := GetLiteralSource([1,2,3,4,5], version);
var beaconVersion :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);

context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName.Y_1984")]));
var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName")]));
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("Y_1984")]));
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("T_foo")]));
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("M_bar")]));
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);
context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("T_foo.M_bar")]));
newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId);

context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName.N_MyName")]));
var badContext := Beaconize(beaconVersion, context, DontUseKeyId);
expect badContext.Failure?;
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_].");

context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("Y_1984.N_MyName")]));
badContext := Beaconize(beaconVersion, context, DontUseKeyId);
expect badContext.Failure?;
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_].");

context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("M_bar.T_foo")]));
badContext := Beaconize(beaconVersion, context, DontUseKeyId);
expect badContext.Failure?;
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_].");
}

method {:test} TestQueryBeacons() {
var context := ExprContext (
None,
Expand All @@ -173,7 +213,7 @@ module TestBaseBeacon {
":NameTitle" := DDB.AttributeValue.S("N_MyName.T_MyTitle"),
":NameTitleN" := DDB.AttributeValue.S("N_MyName"),
":NameTitleT" := DDB.AttributeValue.S("T_MyTitle"),
":NameTitleTN" := DDB.AttributeValue.S("T_MyTitle.N_MyName"),
":NameTitleTN" := DDB.AttributeValue.S("N_MyName.T_MyTitle"),
":NameTitleField" := DDB.AttributeValue.S("MyName__mytitle"),
":YearName" := DDB.AttributeValue.S("Y_1984.N_MyName")
]),
Expand All @@ -187,7 +227,7 @@ module TestBaseBeacon {
":Mixed" := DDB.AttributeValue.S("N_" + Name_beacon + ".Y_1984"),
":Name" := DDB.AttributeValue.S(Name_beacon),
":NameTitle" := DDB.AttributeValue.S("N_" + Name_beacon + ".T_" + Title_beacon),
":NameTitleTN" := DDB.AttributeValue.S("T_" + Title_beacon + ".N_" + Name_beacon),
":NameTitleTN" := DDB.AttributeValue.S("N_" + Name_beacon + ".T_" + Title_beacon),
":NameTitleN" := DDB.AttributeValue.S("N_" + Name_beacon),
":NameTitleT" := DDB.AttributeValue.S("T_" + Title_beacon),
":NameTitleField" := DDB.AttributeValue.S(NameTitle_beacon),
Expand Down