Skip to content

Commit 169d01f

Browse files
ajewellamzajewellamz
authored
feat: correct unicode less than (#609)
* feat: correct unicode less than
1 parent 167d9c3 commit 169d01f

File tree

4 files changed

+209
-23
lines changed

4 files changed

+209
-23
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

Lines changed: 29 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1262,19 +1262,41 @@ module DynamoDBFilterExpr {
12621262
case _ => Failure(E("invalid op in apply_binary_bool"))
12631263
}
12641264

1265-
predicate method LexicographicLess<T(==)>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
1265+
predicate method IsHighSurrogate(ch : char)
12661266
{
1267-
!LexicographicLessOrEqual(b, a, less)
1267+
0xd800 as char <= ch <= 0xdbff as char
12681268
}
12691269

1270-
predicate method LexicographicGreater<T(==)>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
1270+
// If no surrogates are involved, comparison is normal
1271+
// If only surrogates are involved, comparison is normal
1272+
// if one surrogate is involved, the surrogate is larger
1273+
// results undefined if not valid UTF16 encodings, but the idea of 'less' is also undefined for invalid encodings.
1274+
predicate method {:tailrecursion} UnicodeLess(a : string, b : string)
12711275
{
1272-
!LexicographicLessOrEqual(a, b, less)
1276+
if |a| == 0 && |b| == 0 then
1277+
false
1278+
else if |a| == 0 then
1279+
true
1280+
else if |b| == 0 then
1281+
false
1282+
else
1283+
if a[0] == b[0] then
1284+
UnicodeLess(a[1..], b[1..]) // correct independent of surrogate status
1285+
else
1286+
var aIsHighSurrogate := IsHighSurrogate(a[0]);
1287+
var bIsHighSurrogate := IsHighSurrogate(b[0]);
1288+
if aIsHighSurrogate == bIsHighSurrogate then
1289+
a[0] < b[0]
1290+
else
1291+
bIsHighSurrogate
1292+
// we know aIsHighSurrogate != bIsHighSurrogate and a[0] != b[0]
1293+
// so if bIsHighSurrogate then a is less
1294+
// and if aIsHighSurrogate then a is greater
12731295
}
12741296

1275-
predicate method LexicographicGreaterOrEqual<T(==)>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
1297+
predicate method UnicodeLessOrEqual(a : string, b : string)
12761298
{
1277-
LexicographicLessOrEqual(b, a, less)
1299+
!UnicodeLess(b, a)
12781300
}
12791301

12801302
function method CompareFloat(x : string, y : string) : Result<FloatCompare.CompareType, Error>
@@ -1305,7 +1327,7 @@ module DynamoDBFilterExpr {
13051327
var ret :- CompareFloat(a.N, b.N);
13061328
Success(ret <= 0)
13071329
else if a.S? && b.S? then
1308-
Success(LexicographicLessOrEqual(a.S, b.S, CharLess))
1330+
Success(UnicodeLessOrEqual(a.S, b.S))
13091331
else if a.B? && b.B? then
13101332
Success(LexicographicLessOrEqual(a.B, b.B, ByteLess))
13111333
else

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,32 @@ module TestDynamoDBFilterExpr {
2929
expect does_contain(haystack, needle) == negate;
3030
}
3131

32+
method {:test} UnicodeLessTest() {
33+
// A..F must be strictly increasing
34+
var A := "A";
35+
var B := "퀀"; // Ud000"
36+
var C := "﹌"; // Ufe4c"
37+
var D := "𐀁"; // U10001
38+
var E := "𐀂"; // U10002 - same high surrogate as D
39+
var F := "𠀂"; // U20002 - different high surrogate as D
40+
assert |A| == 1;
41+
assert |B| == 1;
42+
assert |C| == 1;
43+
assert |D| == 2;
44+
assert |E| == 2;
45+
assert |F| == 2;
46+
47+
// strings in strs must be strictly increasing
48+
var strs := [A+B+C+D, B+C, C+D, D+C, D+C+B+A, E+D, F+D];
49+
50+
for i := 0 to |strs| {
51+
for j := 0 to |strs| {
52+
expect ((i < j) == UnicodeLess(strs[i], strs[j]));
53+
expect ((i <= j) == !UnicodeLess(strs[j], strs[i]));
54+
}
55+
}
56+
}
57+
3258
method {:test} LowLevelTests() {
3359
expect_equal(ParseExpr("and"), [And]);
3460
expect_equal(ParseExpr(" AnD "), [And]);

‎TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

Lines changed: 137 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
2828
import JSON.API
2929
import opened JSONHelpers
3030
import Norm = DynamoDbNormalizeNumber
31-
3231
import Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes
3332
import DDB = ComAmazonawsDynamodbTypes
3433
import Filter = DynamoDBFilterExpr
@@ -37,10 +36,15 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
3736
import KeyMaterial
3837
import UTF8
3938
import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
39+
import CMP = AwsCryptographyMaterialProvidersTypes
4040
import KeyVectors
4141
import CreateInterceptedDDBClient
4242
import SortedSets
4343
import Seq
44+
import SI = SearchableEncryptionInfo
45+
import MaterialProviders
46+
import MPT = AwsCryptographyMaterialProvidersTypes
47+
import Aws.Cryptography.Primitives
4448

4549
predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000}
4650
type ConfigName = string
@@ -121,7 +125,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
121125
configsForModTest : PairList,
122126
writeTests : seq<WriteTest>,
123127
roundTripTests : seq<RoundTripTest>,
124-
decryptTests : seq<DecryptTest>
128+
decryptTests : seq<DecryptTest>,
129+
strings : seq<string>
125130
) {
126131

127132
method RunAllTests()
@@ -137,13 +142,15 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
137142
print |ioTests|, " ioTests.\n";
138143
print |configsForIoTest|, " configsForIoTest.\n";
139144
print |configsForModTest|, " configsForModTest.\n";
145+
print |strings|, " strings.\n";
140146
if |roundTripTests| != 0 {
141147
print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n";
142148
}
143149
if |roundTripTests| > 1 {
144150
print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n";
145151
}
146152
Validate();
153+
StringOrdering();
147154
BasicIoTest();
148155
RunIoTests();
149156
BasicQueryTest();
@@ -156,6 +163,35 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
156163
DeleteTable(client);
157164
}
158165

166+
function NewOrderRecord(i : nat, str : string) : Record
167+
{
168+
var n := String.Base10Int2String(i);
169+
var m : DDB.AttributeMap := map[HashName := DDB.AttributeValue.N(n), "StrValue" := DDB.AttributeValue.S(str)];
170+
Record(i, m)
171+
}
172+
173+
method StringOrdering() {
174+
print "StringOrdering\n";
175+
var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
176+
var records : seq<Record> := [];
177+
for i := 0 to |strings| {
178+
records := records + [NewOrderRecord(i, strings[i])];
179+
}
180+
WriteAllRecords(client, records);
181+
var subRecords := Seq.Map((r : Record) => r.item, records);
182+
var ops := ["<", "<=", ">", ">=", "=", "<>"];
183+
for i := 0 to |strings| {
184+
for j := 0 to |ops| {
185+
var expr := Some("StrValue " + ops[j] + " :val");
186+
var vals := Some(map[":val" := DDB.AttributeValue.S(strings[i])]);
187+
var query := SimpleQuery(None, None, expr, []);
188+
var items1 := FullScan(client, query, Some(map[]), vals);
189+
var bv :- expect GetFakeBeaconVersion();
190+
var items2 :- expect Filter.FilterResults(bv, subRecords, None, expr, None, vals);
191+
CompareRecordsDisordered2(items1, items2);
192+
}
193+
}
194+
}
159195

160196
method Validate() {
161197
var bad := false;
@@ -531,7 +567,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
531567
}
532568
}
533569

534-
method OneRoundTripTest(client : DDB.IDynamoDBClient, record : Record) {
570+
method OneRoundTripTest(client : DDB.IDynamoDBClient, record : Record)
571+
requires client.ValidState()
572+
ensures client.ValidState()
573+
modifies client.Modifies
574+
{
535575
var putInput := DDB.PutItemInput(
536576
TableName := TableName,
537577
Item := record.item,
@@ -545,7 +585,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
545585
ExpressionAttributeValues := None
546586
);
547587
var _ :- expect client.PutItem(putInput);
548-
588+
expect HashName in record.item;
549589
var getInput := DDB.GetItemInput(
550590
TableName := TableName,
551591
Key := map[HashName := record.item[HashName]],
@@ -772,6 +812,19 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
772812
}
773813
expect !bad;
774814
}
815+
method CompareRecordsDisordered2(expected : DDB.ItemList, actual : DDB.ItemList)
816+
{
817+
expect |expected| == |actual|;
818+
var bad := false;
819+
for i := 0 to |expected| {
820+
var found := FindMatchingRecord(expected[i], actual);
821+
if !found {
822+
print "Did not find result for record ", expected[i], "\n";
823+
bad := true;
824+
}
825+
}
826+
expect !bad;
827+
}
775828

776829
method BasicIoTestScan(client : DDB.IDynamoDBClient, records : seq<Record>)
777830
requires client.ValidState()
@@ -863,9 +916,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
863916
var asSet := Seq.ToSet(s);
864917
DDB.AttributeValue.BS(SortedSets.ComputeSetToOrderedSequence2(asSet, ByteLess))
865918
case L(list) =>
866-
DDB.AttributeValue.L(Seq.Map(n => Normalize(n), list))
919+
// for some reason, Seq.Map() fails for verify, even when revealed
920+
var value := seq(|list|, i requires 0 <= i < |list| => Normalize(list[i]));
921+
DDB.AttributeValue.L(value)
867922
case M(m) =>
868-
DDB.AttributeValue.M(map k <- m :: k := Normalize(m[k]))
923+
DDB.AttributeValue.M(map k <- m :: k := Normalize(m[k]))
869924
case _ => value
870925
}
871926
}
@@ -1047,7 +1102,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10471102

10481103
function MakeEmptyTestVector() : TestVectorConfig
10491104
{
1050-
TestVectorConfig(MakeCreateTableInput(), [], map[], [], map[], map[], [], [], [], [], [], [], [], [])
1105+
TestVectorConfig(MakeCreateTableInput(), [], map[], [], map[], map[], [], [], [], [], [], [], [], [], [])
10511106
}
10521107

10531108
method ParseTestVector(data : JSON, prev : TestVectorConfig) returns (output : Result<TestVectorConfig, string>)
@@ -1067,6 +1122,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10671122
var writeTests : seq<WriteTest> := [];
10681123
var roundTripTests : seq<RoundTripTest> := [];
10691124
var decryptTests : seq<DecryptTest> := [];
1125+
var strings : seq<string> := [];
10701126

10711127
for i := 0 to |data.obj| {
10721128
match data.obj[i].0 {
@@ -1084,6 +1140,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
10841140
case "WriteTests" => writeTests :- GetWriteTests(data.obj[i].1);
10851141
case "RoundTripTest" => roundTripTests :- GetRoundTripTests(data.obj[i].1);
10861142
case "DecryptTests" => decryptTests :- GetDecryptTests(data.obj[i].1);
1143+
case "Strings" => strings :- GetStrings(data.obj[i].1);
10871144
case _ => return Failure("Unexpected top level tag " + data.obj[i].0);
10881145
}
10891146
}
@@ -1104,7 +1161,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
11041161
configsForModTest := prev.configsForModTest + queryPairs,
11051162
writeTests := prev.writeTests + writeTests,
11061163
roundTripTests := prev.roundTripTests + roundTripTests,
1107-
decryptTests := prev.decryptTests + decryptTests
1164+
decryptTests := prev.decryptTests + decryptTests,
1165+
strings := prev.strings + strings
11081166
)
11091167
);
11101168
}
@@ -1207,6 +1265,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
12071265
method GetOneTableConfig(name : string, data : JSON) returns (output : Result<TableConfig, string>)
12081266
{
12091267
:- Need(data.Object?, "A Table Config must be an object.");
1268+
var logicalTableName := TableName;
1269+
var partitionKeyName : DDB.KeySchemaAttributeName := HashName;
1270+
var sortKeyName : Option<DDB.KeySchemaAttributeName> := None;
1271+
var algorithmSuiteId : Option<CMP.DBEAlgorithmSuiteId> := None;
12101272
var encrypt : seq<string> := [];
12111273
var attributeActionsOnEncrypt : Types.AttributeActions := map[];
12121274
var allowed : seq<DDB.AttributeName> := [];
@@ -1216,13 +1278,47 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
12161278
var virtualFields : seq<Types.VirtualField> := [];
12171279
var keySource : Option<Types.BeaconKeySource> := None;
12181280
var search : Option<Types.SearchConfig> := None;
1281+
var legacyOverride: Option<Types.LegacyOverride> := None;
1282+
var plaintextOverride: Option<Types.PlaintextOverride> := None;
12191283

12201284
for i := 0 to |data.obj| {
12211285
var obj := data.obj[i];
12221286
match obj.0 {
1287+
case "logicalTableName" =>
1288+
:- Need(obj.1.String?, "logicalTableName must be of type String.");
1289+
logicalTableName := obj.1.str;
1290+
case "partitionKeyName" =>
1291+
:- Need(obj.1.String?, "partitionKeyName must be of type String.");
1292+
:- Need(DDB.IsValid_KeySchemaAttributeName(obj.1.str), "partitionKeyName '" + obj.1.str + "' is not a valid KeySchemaAttributeName.");
1293+
partitionKeyName := obj.1.str;
1294+
case "sortKeyName" =>
1295+
:- Need(obj.1.String?, "sortKeyName must be of type String.");
1296+
:- Need(DDB.IsValid_KeySchemaAttributeName(obj.1.str), "sortKeyName '" + obj.1.str + "' is not a valid KeySchemaAttributeName.");
1297+
sortKeyName := Some(obj.1.str);
1298+
case "algorithmSuiteId" =>
1299+
:- Need(obj.1.String?, "algorithmSuiteId must be of type String.");
1300+
if obj.1.str == "ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384" {
1301+
algorithmSuiteId := Some(CMP.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384);
1302+
} else if obj.1.str == "ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384" {
1303+
algorithmSuiteId := Some(CMP.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384);
1304+
} else {
1305+
return Failure("algorithmSuiteId '" + obj.1.str + "' must be either ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384 or ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384");
1306+
}
1307+
case "plaintextOverride" =>
1308+
:- Need(obj.1.String?, "plaintextOverride must be of type String.");
1309+
if obj.1.str == "FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ" {
1310+
plaintextOverride := Some(Types.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ);
1311+
} else if obj.1.str == "FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ" {
1312+
plaintextOverride := Some(Types.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ);
1313+
} else if obj.1.str == "FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ" {
1314+
plaintextOverride := Some(Types.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ);
1315+
} else {
1316+
return Failure("plaintextOverride '" + obj.1.str + "' must be one of FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ, FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ or FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ");
1317+
}
1318+
12231319
case "attributeActionsOnEncrypt" => attributeActionsOnEncrypt :- GetAttributeActions(obj.1);
12241320
case "allowedUnsignedAttributePrefix" =>
1225-
:- Need(obj.1.String?, "Prefix must be of type String.");
1321+
:- Need(obj.1.String?, "allowedUnsignedAttributePrefix must be of type String.");
12261322
prefix := obj.1.str;
12271323
case "allowedUnsignedAttributes" => allowed :- GetAttrNames(obj.1);
12281324
case "search" => var src :- GetOneSearchConfig(obj.1); search := Some(src);
@@ -1242,18 +1338,18 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
12421338

12431339
var config :=
12441340
Types.DynamoDbTableEncryptionConfig(
1245-
logicalTableName := TableName,
1246-
partitionKeyName := HashName,
1247-
sortKeyName := None,
1341+
logicalTableName := logicalTableName,
1342+
partitionKeyName := partitionKeyName,
1343+
sortKeyName := sortKeyName,
12481344
search := search,
12491345
attributeActionsOnEncrypt := attributeActionsOnEncrypt,
12501346
allowedUnsignedAttributes := OptSeq(allowed),
12511347
allowedUnsignedAttributePrefix := OptSeq(prefix),
1252-
algorithmSuiteId := None,
1348+
algorithmSuiteId := algorithmSuiteId,
12531349
keyring := Some(keyring),
12541350
cmm := None,
1255-
legacyOverride := None,
1256-
plaintextOverride := None
1351+
legacyOverride := legacyOverride,
1352+
plaintextOverride := plaintextOverride
12571353
);
12581354
return Success(TableConfig(name, config, |data.obj| == 0));
12591355
}
@@ -1327,6 +1423,32 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
13271423
);
13281424
}
13291425

1426+
method GetFakeBeaconVersion() returns (output : Result<SI.BeaconVersion, string>)
1427+
ensures output.Success? ==> output.value.ValidState() && fresh(output.value.Modifies())
1428+
{
1429+
var keyMaterial : KeyMaterial.KeyMaterial :=
1430+
KeyMaterial.StaticKeyStoreInformation("abc", UTF8.EncodeAscii("abc"), [1,2,3,4,5], [1,2,3,4,5]);
1431+
var store := SKS.CreateStaticKeyStore(keyMaterial);
1432+
var source : Types.BeaconKeySource := Types.single(Types.SingleKeyStore(keyId := "foo", cacheTTL := 42));
1433+
1434+
var sb := Types.StandardBeacon(name := "name", length := 5 as Types.BeaconBitLength, loc := None, style := None);
1435+
1436+
var mpl :- expect MaterialProviders.MaterialProviders();
1437+
1438+
var cacheType : MPT.CacheType := MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1));
1439+
1440+
var input := MPT.CreateCryptographicMaterialsCacheInput(
1441+
cache := cacheType
1442+
);
1443+
var cache :- expect mpl.CreateCryptographicMaterialsCache(input);
1444+
1445+
var client :- expect Primitives.AtomicPrimitives();
1446+
var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32);
1447+
1448+
var bv :- expect SI.MakeBeaconVersion(1, src, map[], map[], map[]);
1449+
return Success(bv);
1450+
}
1451+
13301452
method GetAttributeActions(data : JSON) returns (output : Result<Types.AttributeActions, string>)
13311453
{
13321454
:- Need(data.Object?, "attributeActionsOnEncrypt must be an object");

0 commit comments

Comments
 (0)