Skip to content

feat: repair numeric equality #228

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 5 commits into from
Jun 6, 2023
Merged

feat: repair numeric equality #228

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f217fd0
feat: repair numeric equality
ajewellamz Jun 2, 2023
fafc090
add numeruc test to test vectors
ajewellamz Jun 2, 2023
a3701da
validate numbers in queries
ajewellamz Jun 2, 2023
c7980ae
add failure test for malformed number
ajewellamz Jun 5, 2023
c0a3a9e
Merge branch 'main' into repair-numeric-equal
ajewellamz Jun 5, 2023
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
71 changes: 49 additions & 22 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ module DynamoDBFilterExpr {
import StandardLibrary.String
import CompoundBeacon
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
import Norm = DynamoDbNormalizeNumber

// extract all the attributes from a filter expression
// except for those which do not need the attribute's value
Expand Down Expand Up @@ -1125,9 +1126,11 @@ module DynamoDBFilterExpr {
}

// true if middle between left and right
predicate method is_between(middle : DDB.AttributeValue, left : DDB.AttributeValue, right : DDB.AttributeValue)
function method is_between(middle : DDB.AttributeValue, left : DDB.AttributeValue, right : DDB.AttributeValue) : Result<bool, Error>
{
AttributeLE(left, middle) && AttributeLE(middle, right)
var leftRet :- AttributeLE(left, middle);
var rightRet :- AttributeLE(middle, right);
Success(leftRet && rightRet)
}

// true if target in list
Expand Down Expand Up @@ -1166,7 +1169,8 @@ module DynamoDBFilterExpr {
Failure(E("No Stack for Between"))
else
if stack[|stack|-1].Str? && stack[|stack|-2].Str? && stack[|stack|-3].Str? then
Success(Bool(is_between(stack[|stack|-3].s, stack[|stack|-2].s, stack[|stack|-1].s)))
var ret :- is_between(stack[|stack|-3].s, stack[|stack|-2].s, stack[|stack|-1].s);
Success(Bool(ret))
else
Failure(E("Wrong Types for contains"))

Expand Down Expand Up @@ -1257,43 +1261,66 @@ module DynamoDBFilterExpr {
LexicographicLessOrEqual(b, a, less)
}

predicate method CharLess(a: char, b: char) { a < b }
predicate method ByteLess(a: uint8, b: uint8) { a < b }
function method CompareFloat(x : string, y : string) : Result<FloatCompare.CompareType, Error>
{
var newX :- Norm.NormalizeNumber(x).MapFailure(e => E(e));
var newY :- Norm.NormalizeNumber(y).MapFailure(e => E(e));
Success(FloatCompare.CompareFloat(newX, newY))
}

predicate method AttributeLE(a : DDB.AttributeValue, b : DDB.AttributeValue)
function method AttributeEQ(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
{
if a.N? && b.N? then
FloatCompare.CompareFloat(a.N, b.N) <= 0
var ret :- CompareFloat(a.N, b.N);
Success(ret == 0)
else
Success(a == b)
}

function method AttributeNE(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
{
var ret :- AttributeEQ(a, b);
Success(!ret)
}

function method AttributeLE(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
{
if a.N? && b.N? then
var ret :- CompareFloat(a.N, b.N);
Success(ret <= 0)
else if a.S? && b.S? then
LexicographicLessOrEqual(a.S, b.S, CharLess)
Success(LexicographicLessOrEqual(a.S, b.S, CharLess))
else if a.B? && b.B? then
LexicographicLessOrEqual(a.B, b.B, ByteLess)
Success(LexicographicLessOrEqual(a.B, b.B, ByteLess))
else
false
Success(false)
}
predicate method AttributeLT(a : DDB.AttributeValue, b : DDB.AttributeValue)
function method AttributeLT(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
{
!AttributeLE(b,a)
var ret :- AttributeLE(b,a);
Success(!ret)
}
predicate method AttributeGT(a : DDB.AttributeValue, b : DDB.AttributeValue)
function method AttributeGT(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
{
!AttributeLE(a,b)
var ret :- AttributeLE(a,b);
Success(!ret)
}
predicate method AttributeGE(a : DDB.AttributeValue, b : DDB.AttributeValue)
function method AttributeGE(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
{
AttributeLE(b,a)
var ret :- AttributeLE(b,a);
Success(ret)
}

// apply the comparison function
function method apply_binary_comp(input : Token, x : DDB.AttributeValue, y : DDB.AttributeValue) : Result<bool, Error>
{
match input
case Eq => Success(x == y)
case Ne => Success(x != y)
case Le => Success(AttributeLE(x, y))
case Lt => Success(AttributeLT(x, y))
case Ge => Success(AttributeGE(x, y))
case Gt => Success(AttributeGT(x, y))
case Eq => AttributeEQ(x, y)
case Ne => AttributeNE(x, y)
case Le => AttributeLE(x, y)
case Lt => AttributeLT(x, y)
case Ge => AttributeGE(x, y)
case Gt => AttributeGT(x, y)
case _ => Failure(E("invalid op in apply_binary_bool"))
}

Expand Down
53 changes: 53 additions & 0 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,6 +274,59 @@ module TestDynamoDBFilterExpr {
newItems :- expect FilterResults(bv, [item1], None, Some("three = two"), None, None);
expect_equal(newItems, [item1]);
}

method {:test} TestFilterFailNumeric() {
var item1 : DDB.AttributeMap := map[
"one" := DN("800")
];
var values : DDB.ExpressionAttributeValueMap := map [
":two" := DN("foo")
];
var version := GetLotsaBeacons();
var src := GetLiteralSource([1,2,3,4,5], version);
var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src);
var newItems := FilterResults(bv, [item1], None, Some("one < :two"), None, Some(values));
expect newItems.Failure?;
expect newItems.error == E("Number needs digits either before or after the decimal point. when parsing 'foo'.");
}

method {:test} TestFilterCompareNumeric() {
var item1 : DDB.AttributeMap := map[
"one" := DN("800")
];
var values : DDB.ExpressionAttributeValueMap := map [
":two" := DN("0800.000e0")
];
var version := GetLotsaBeacons();
var src := GetLiteralSource([1,2,3,4,5], version);
var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src);
var newItems :- expect FilterResults(bv, [item1], None, Some("one < :two"), None, Some(values));
expect_equal(newItems, []);
newItems :- expect FilterResults(bv, [item1], None, Some("one > :two"), None, Some(values));
expect_equal(newItems, []);
newItems :- expect FilterResults(bv, [item1], None, Some("one <= :two"), None, Some(values));
expect_equal(newItems, [item1]);
newItems :- expect FilterResults(bv, [item1], None, Some("one >= :two"), None, Some(values));
expect_equal(newItems, [item1]);
newItems :- expect FilterResults(bv, [item1], None, Some("one <> :two"), None, Some(values));
expect_equal(newItems, []);
newItems :- expect FilterResults(bv, [item1], None, Some("one = :two"), None, Some(values));
expect_equal(newItems, [item1]);

newItems :- expect FilterResults(bv, [item1], None, Some(":two < one"), None, Some(values));
expect_equal(newItems, []);
newItems :- expect FilterResults(bv, [item1], None, Some(":two > one"), None, Some(values));
expect_equal(newItems, []);
newItems :- expect FilterResults(bv, [item1], None, Some(":two <= one"), None, Some(values));
expect_equal(newItems, [item1]);
newItems :- expect FilterResults(bv, [item1], None, Some(":two >= one"), None, Some(values));
expect_equal(newItems, [item1]);
newItems :- expect FilterResults(bv, [item1], None, Some(":two <> one"), None, Some(values));
expect_equal(newItems, []);
newItems :- expect FilterResults(bv, [item1], None, Some(":two = one"), None, Some(values));
expect_equal(newItems, [item1]);
}

method {:test} TestFilterIn() {
var item1 : DDB.AttributeMap := map[
"one" := DS("abc"),
Expand Down
27 changes: 23 additions & 4 deletions TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
import FileIO
import JSON.API
import opened JSONHelpers
import Norm = DynamoDbNormalizeNumber

import Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes
import DDB = ComAmazonawsDynamodbTypes
Expand Down Expand Up @@ -681,8 +682,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {

method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool)
{
var exp := NormalizeItem(expected);
for i := 0 to |actual| {
if actual[i] == expected {
if actual[i] == exp {
return true;
}
}
Expand Down Expand Up @@ -740,7 +742,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
);
var out :- expect client.GetItem(input);
expect out.Item.Some?;
expect out.Item.value == records[i].item;
expect out.Item.value == NormalizeItem(records[i].item);
}
}

Expand All @@ -764,13 +766,30 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
}
}

function NormalizeItem(value : DDB.AttributeMap) : DDB.AttributeMap
{
map k <- value :: k := Normalize(value[k])
}

function Normalize(value : DDB.AttributeValue) : DDB.AttributeValue
{
match value {
case N(n) =>
var nn := Norm.NormalizeNumber(n);
if nn.Success? then
DDB.AttributeValue.N(nn.value)
else
value
case _ => value
}
}

method ItemExists(number : DDB.AttributeValue, record : Record, resp : DDB.ItemList) returns (output : bool)
{
if |resp| == 0 {
return false;
} else if HashName in resp[0] && resp[0][HashName] == number {
expect resp[0] == record.item;
expect resp[0] == NormalizeItem(record.item);
return true;
} else {
output := ItemExists(number, record, resp[1..]);
Expand All @@ -781,7 +800,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
if |resp| == 0 {
return false;
} else if resp[0].Item.Some? && HashName in resp[0].Item.value && resp[0].Item.value[HashName] == number {
expect resp[0].Item.value == record.item;
expect resp[0].Item.value == NormalizeItem(record.item);
return true;
} else {
output := ItemExists2(number, record, resp[1..]);
Expand Down
19 changes: 14 additions & 5 deletions TestVectors/runtimes/java/configs.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@
"One": "DO_NOTHING",
"Seven": "DO_NOTHING",
"Eight": "DO_NOTHING",
"Nine": "DO_NOTHING"
"Nine": "DO_NOTHING",
"NumberTest" : "ENCRYPT_AND_SIGN"
},
"allowedUnsignedAttributes": [
"One",
Expand All @@ -36,6 +37,10 @@
{
"Name": "Three",
"Length": 32
},
{
"Name": "NumberTest",
"Length": 32
}
]
}
Expand All @@ -54,7 +59,8 @@
"One": "DO_NOTHING",
"Seven": "DO_NOTHING",
"Eight": "DO_NOTHING",
"Nine": "DO_NOTHING"
"Nine": "DO_NOTHING",
"NumberTest" : "SIGN_ONLY"
},
"allowedUnsignedAttributes": [
"One",
Expand Down Expand Up @@ -99,7 +105,8 @@
"One": "DO_NOTHING",
"Seven": "DO_NOTHING",
"Eight": "DO_NOTHING",
"Nine": "DO_NOTHING"
"Nine": "DO_NOTHING",
"NumberTest" : "SIGN_ONLY"
},
"allowedUnsignedAttributes": [
"One",
Expand All @@ -120,7 +127,8 @@
"One": "DO_NOTHING",
"Seven": "DO_NOTHING",
"Eight": "DO_NOTHING",
"Nine": "DO_NOTHING"
"Nine": "DO_NOTHING",
"NumberTest" : "SIGN_ONLY"
},
"allowedUnsignedAttributes": [
"One",
Expand All @@ -141,7 +149,8 @@
"One": "DO_NOTHING",
"Seven": "DO_NOTHING",
"Eight": "DO_NOTHING",
"Nine": "DO_NOTHING"
"Nine": "DO_NOTHING",
"NumberTest" : "SIGN_ONLY"
},
"allowedUnsignedAttributes": [
"One",
Expand Down
4 changes: 4 additions & 0 deletions TestVectors/runtimes/java/data.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@
":six": "Seis",
":seven": "Siete",
":eight": "Ocho",
":NumberTest" : {"N" : "0800.000e0"},
":nine": "Nueve",
":cmp1a": "F_Cuatro.S_Junk",
":cmp1b": "F_444.S_Junk",
Expand Down Expand Up @@ -96,6 +97,9 @@
{
"Filter": "Nine between :nine and :nine"
},
{
"Filter": "NumberTest = :NumberTest"
},
{
"Filter": "RecNum in (:zero, :one)"
},
Expand Down
3 changes: 2 additions & 1 deletion TestVectors/runtimes/java/records.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@
"Six": "666",
"Seven": "777",
"Eight": "888",
"Nine": "999"
"Nine": "999",
"NumberTest" : {"N" : "0800.000e0"}
},
{
"RecNum": {
Expand Down