@@ -98,14 +98,24 @@ module {:options "-functionSyntax:4"} WriteManifest {
9898 },
9999 ""allowedUnsignedAttributes"" : [""Stuff"", ""Junk""]
100100 }"
101-
101+
102102 method TextToJson (x: string ) returns (output : JSON)
103103 {
104104 var str :- expect UTF8. Encode (x);
105105 var json :- expect API. Deserialize (str);
106106 return json;
107107 }
108108
109+ const QUOTE : string := "\""
110+
111+ const ConfigRecord :=
112+ "{\"RecNum\": 1,"
113+ + QUOTE + Attr1 + QUOTE + ": \"aaa\","
114+ + QUOTE + Attr2 + QUOTE + ": {\"M\" : {\"A\":\"B\", \"C\":\"D\"}},"
115+ + QUOTE + Attr3 + QUOTE + ": {\"L\" : [{\"M\" : {\"A\":\"B\", \"C\":\"D\"}}, {\"NS\":[\"00. 0011\", \"0000\", \"2000. 000\", \"10. 01\"]}, {\"SS\":[\"00. 0011\", \"0000\", \"2000. 000\", \"10. 01\"]}]},"
116+ + QUOTE + Attr4 + QUOTE + ": {\"SS\":[\"00. 0011\", \"0000\", \"2000. 000\", \"10. 01\"]},"
117+ + QUOTE + Attr5 + QUOTE + ": {\"NS\":[\"00. 0011\", \"0000\", \"2000. 000\", \"10. 01\"]}}"
118+
109119 const BasicRecord := @"{
110120 ""RecNum"": 1,
111121 ""Stuff"": ""StuffData"",
@@ -122,11 +132,11 @@ module {:options "-functionSyntax:4"} WriteManifest {
122132 }"
123133
124134 method MakeTest (
125- name : string ,
126- typ : string ,
127- desc : string ,
128- configJson : string ,
129- recordJson : string ,
135+ name : string ,
136+ typ : string ,
137+ desc : string ,
138+ configJson : string ,
139+ recordJson : string ,
130140 decryptConfigJson : Option <string > := None) returns (output : (string , JSON))
131141 {
132142 var config := TextToJson (configJson);
@@ -145,8 +155,164 @@ module {:options "-functionSyntax:4"} WriteManifest {
145155 return (name, Object (result));
146156 }
147157
158+ type CryptoAction = x : int | 0 <= x < 4
159+ type CryptoActions = x : seq < CryptoAction> | |x| == 6 witness [0,0,0,0,0,0]
160+ const CryptoActionStr : seq < string > := ["0", "1", "2", "3"]
161+ const MyActionNames : seq < string > := ["ENCRYPT_AND_SIGN", "SIGN_ONLY", "SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT", "DO_NOTHING"]
162+ const Encrypt : CryptoAction := 0
163+ const SignOnly : CryptoAction := 1
164+ const SignInclude : CryptoAction := 2
165+ const DoNothing : CryptoAction := 3
166+
167+ const A : string := "A"
168+ const B : string := "퀀" // Ud000"
169+ const C : string := "﹌" // Ufe4c"
170+ const D : string := "𐀁" // U10001
171+ const E : string := "𐀂" // U10002 - same high surrogate as D
172+ const F : string := "𠀂" // U20002 - different high surrogate as D
173+
174+ lemma CheckLengths ()
175+ ensures |A| == 1
176+ ensures |B| == 1
177+ ensures |C| == 1
178+ ensures |D| == 2
179+ ensures |E| == 2
180+ ensures |F| == 2
181+ {}
182+
183+ // Let's make attribute names with complex characters.
184+ // It shouldn't matter, but let's make sure
185+ const Attr1 : string := F+ D
186+ const Attr2 : string := A+ B+ C+ D
187+ const Attr3 : string := E+ D
188+ const Attr4 : string := C+ D
189+ const Attr5 : string := D+ C+ B+ A
190+ const MyAttrNames : seq < string > := ["RecNum", Attr1, Attr2, Attr3, Attr4, Attr5]
191+
192+
193+ method MakeConfig (actions : CryptoActions ) returns (output : JSON)
194+ ensures output. Object?
195+ {
196+ var configActions : seq < (string , JSON)> := [];
197+ var notSigned : seq < JSON> := [];
198+ for i := 0 to 6 {
199+ var myAction : CryptoAction := actions[i];
200+ configActions := configActions + [(MyAttrNames[i], String (MyActionNames[myAction]))];
201+ if myAction == DoNothing {
202+ notSigned := notSigned + [String (MyAttrNames[i])];
203+ }
204+ }
205+ var result : seq < (string , JSON)> := [
206+ ("attributeActionsOnEncrypt", Object (configActions)),
207+ ("allowedUnsignedAttributes", Array (notSigned))
208+ ];
209+
210+ return Object (result);
211+ }
212+
213+ method MakeConfigTest (
214+ name : string ,
215+ config : JSON ,
216+ record : JSON ,
217+ decryptConfigJson : Option <JSON > := None) returns (output : (string , JSON))
218+ {
219+ var result : seq < (string , JSON)> :=
220+ [
221+ ("type ", String ("positive-encrypt")),
222+ ("description", String ("config test")),
223+ ("config", config),
224+ ("record", record)
225+ ];
226+ if decryptConfigJson. Some? {
227+ var decryptConfig := decryptConfigJson. value;
228+ result := result + [("decryptConfig", decryptConfig)];
229+ }
230+ return (name, Object (result));
231+ }
232+
233+ function Increment (x : CryptoActions ) : CryptoActions
234+ {
235+ if x[5] < 3 then
236+ [x[0], x[1], x[2], x[3], x[4], x[5]+ 1]
237+ else if x[4] < 3 then
238+ [x[0], x[1], x[2], x[3], x[4]+ 1, 0]
239+ else if x[3] < 3 then
240+ [x[0], x[1], x[2], x[3]+ 1, 0, 0]
241+ else if x[2] < 3 then
242+ [x[0], x[1], x[2]+ 1, 0, 0, 0]
243+ else if x[1] < 3 then
244+ [x[0], x[1]+ 1, 0, 0, 0, 0]
245+ else if x[0] < 3 then
246+ [x[0]+ 1, 0, 0, 0, 0, 0]
247+ else
248+ [0, 0, 0, 0, 0, 0]
249+ }
250+
251+ predicate IsConsistent (actions : CryptoActions )
252+ {
253+ if actions[0] in [DoNothing, Encrypt] then
254+ false
255+ else if actions[0] == SignOnly && (exists x | x in actions :: x == SignInclude) then
256+ false
257+ else
258+ true
259+ }
260+
261+ predicate IsConsistentWith (oldActions : CryptoActions , newActions : CryptoActions )
262+ {
263+ if ! IsConsistent (oldActions) || ! IsConsistent (newActions) then
264+ false
265+ else
266+ ! exists i | 0 <= i < 6 :: (oldActions[i] == DoNothing) != (newActions[i] == DoNothing)
267+ }
268+
269+ // make a test for every valid combination of Crypto Actions
270+ method MakeConfigTests () returns (output : seq < (string , JSON)> )
271+ {
272+ var actions : CryptoActions := [0,0,0,0,0,0];
273+ var result : seq < (string , JSON)> := [];
274+ var record := TextToJson (ConfigRecord);
275+ var actionWrittenOuter := 0;
276+ var actionWrittenInner := 0;
277+ for i := 0 to 4096 {
278+ actions := Increment (actions);
279+ if IsConsistent (actions) {
280+ var name := "ConfigTest_";
281+ for j := 0 to 6 {
282+ name := name + CryptoActionStr[actions[j]];
283+ }
284+ var config := MakeConfig (actions);
285+ var theTest := MakeConfigTest (name, config, record);
286+ result := result + [theTest];
287+ actionWrittenOuter := actionWrittenOuter + 1;
288+
289+ // for a subset of these,
290+ // make a test to decrypt with every possible valid combination of Crypto Actions
291+ if (actionWrittenOuter % 100) == 0 {
292+ var otherActions : CryptoActions := [0,0,0,0,0,0];
293+ for j := 0 to 4096 {
294+ otherActions := Increment (otherActions);
295+ if IsConsistentWith (actions, otherActions) {
296+ var newConfig := MakeConfig (otherActions);
297+ var newName := name + "_";
298+ for k := 0 to 6 {
299+ newName := newName + CryptoActionStr[otherActions[k]];
300+ }
301+ var newTest := MakeConfigTest (newName, config, record, Some(newConfig));
302+ result := result + [newTest];
303+ actionWrittenInner := actionWrittenInner + 1;
304+ }
305+ }
306+ }
307+ }
308+ }
309+ print "MakeConfigTests : ", actionWrittenOuter, " outer and ", actionWrittenInner, " inner for ", |result|, " total. \n";
310+ return result;
311+ }
312+
148313 method Write (fileName : string ) returns (output : Result< bool , string > )
149314 {
315+ print "Write : ", fileName, "\n";
150316 var result : seq < (string , JSON)> :=
151317 [Manifest (), ("keys", String ("file://keys.json"))];
152318
@@ -163,7 +329,8 @@ module {:options "-functionSyntax:4"} WriteManifest {
163329 var test11 := MakeTest ("11", "positive-encrypt", "Basic encrypt V2", BasicV2Config, BasicRecord);
164330 var test12 := MakeTest ("12", "positive-encrypt", "Basic encrypt V2 switching1", LongerV2Config1, BasicRecord, Some(LongerV2Config2));
165331 var test13 := MakeTest ("13", "positive-encrypt", "Basic encrypt V2 switching2", LongerV2Config2, BasicRecord, Some(LongerV2Config1));
166- var tests : seq < (string , JSON)> := [test1, test2, test3, test4, test5, test6, test7, test8, test9, test10, test11, test12, test13];
332+ var configTests := MakeConfigTests ();
333+ var tests : seq < (string , JSON)> := [test1, test2, test3, test4, test5, test6, test7, test8, test9, test10, test11, test12, test13] + configTests;
167334 var final := Object (result + [("tests", Object(tests))]);
168335
169336 var jsonBytes :- expect API. Serialize (final);
0 commit comments