diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy index a5ce41c25..d6544d233 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy @@ -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 @@ -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 { - AttributeLE(left, middle) && AttributeLE(middle, right) + var leftRet :- AttributeLE(left, middle); + var rightRet :- AttributeLE(middle, right); + Success(leftRet && rightRet) } // true if target in list @@ -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")) @@ -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 + { + 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 { 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 + { + var ret :- AttributeEQ(a, b); + Success(!ret) + } + + function method AttributeLE(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result + { + 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 { - !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 { - !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 { - 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 { 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")) } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy index afa5aca4a..f6a081955 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy @@ -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"), diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 11123038a..5e2e1d2f1 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -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 @@ -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; } } @@ -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); } } @@ -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..]); @@ -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..]); diff --git a/TestVectors/runtimes/java/configs.json b/TestVectors/runtimes/java/configs.json index d21701fe1..30ec452fe 100644 --- a/TestVectors/runtimes/java/configs.json +++ b/TestVectors/runtimes/java/configs.json @@ -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", @@ -36,6 +37,10 @@ { "Name": "Three", "Length": 32 + }, + { + "Name": "NumberTest", + "Length": 32 } ] } @@ -54,7 +59,8 @@ "One": "DO_NOTHING", "Seven": "DO_NOTHING", "Eight": "DO_NOTHING", - "Nine": "DO_NOTHING" + "Nine": "DO_NOTHING", + "NumberTest" : "SIGN_ONLY" }, "allowedUnsignedAttributes": [ "One", @@ -99,7 +105,8 @@ "One": "DO_NOTHING", "Seven": "DO_NOTHING", "Eight": "DO_NOTHING", - "Nine": "DO_NOTHING" + "Nine": "DO_NOTHING", + "NumberTest" : "SIGN_ONLY" }, "allowedUnsignedAttributes": [ "One", @@ -120,7 +127,8 @@ "One": "DO_NOTHING", "Seven": "DO_NOTHING", "Eight": "DO_NOTHING", - "Nine": "DO_NOTHING" + "Nine": "DO_NOTHING", + "NumberTest" : "SIGN_ONLY" }, "allowedUnsignedAttributes": [ "One", @@ -141,7 +149,8 @@ "One": "DO_NOTHING", "Seven": "DO_NOTHING", "Eight": "DO_NOTHING", - "Nine": "DO_NOTHING" + "Nine": "DO_NOTHING", + "NumberTest" : "SIGN_ONLY" }, "allowedUnsignedAttributes": [ "One", diff --git a/TestVectors/runtimes/java/data.json b/TestVectors/runtimes/java/data.json index 1cf394074..4bbc334ad 100644 --- a/TestVectors/runtimes/java/data.json +++ b/TestVectors/runtimes/java/data.json @@ -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", @@ -96,6 +97,9 @@ { "Filter": "Nine between :nine and :nine" }, + { + "Filter": "NumberTest = :NumberTest" + }, { "Filter": "RecNum in (:zero, :one)" }, diff --git a/TestVectors/runtimes/java/records.json b/TestVectors/runtimes/java/records.json index ee4e66ce9..e17792f93 100644 --- a/TestVectors/runtimes/java/records.json +++ b/TestVectors/runtimes/java/records.json @@ -13,7 +13,8 @@ "Six": "666", "Seven": "777", "Eight": "888", - "Nine": "999" + "Nine": "999", + "NumberTest" : {"N" : "0800.000e0"} }, { "RecNum": {