Skip to content

Commit 2d7ff90

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
added new test case for policy minimization
1 parent a553440 commit 2d7ff90

4 files changed

Lines changed: 252 additions & 2 deletions

File tree

‎README.md‎

Lines changed: 91 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -270,7 +270,7 @@ You should see the following theorems:
270270
- `paper_example_cakeml_worstTheory.policy_trans_fwd_proof` : soundness of trans-fwd (Theorem 1)
271271
- `paper_example_cakeml_worstTheory.policy_BDD` : MTBDD1 result
272272
- `paper_example_cakeml_worstTheory.table_BDD` : MTBDD2 result
273-
- `paper_example_cakeml_worstTheory.table_trans_back` : trans-back soundness (Theorem 2)
273+
- `paper_example_cakeml_worstTheory.table_trans_back` : trans-back soundness (Theorem 2, you will see the tables here)
274274
- `paper_example_cakeml_worstTheory.final_proof` : end-to-end equivalence proof between policy and a table
275275

276276

@@ -401,7 +401,97 @@ The theorem will show the equivelnce.
401401

402402

403403

404+
### Policy Minimization Example
404405

406+
The policy minimization example is in `hol/polygram/reviewers_test_here/policy_min_exampleScript.sml`.
407+
408+
It demonstrates PolyGram's policy minimization on a bloated policy defined over three predicates.
409+
410+
The input policy has 9 rules with several issues that are hard to spot by hand:
411+
412+
- **Rule 2** : unsatisfiable . `y1 AND y2` is always false (disjoint port ranges)
413+
- **Rule 4** : unsatisfiable . `y1 AND NOT y1` is always false
414+
- **Rule 7** : unsatisfiable . `z AND NOT z` is always false
415+
- **Rule 9** : unreachable . Rule 8 (`NOT z → fwd(2)`) always fires first due to match-first semantics
416+
- **Rules 1, 3, 5, 6** : overlapping conditions that can be simplified
417+
418+
PolyGram automatically generates a minimized policy and produces a certified proof that the minimized policy is semantically equivalent to the original.
419+
420+
#### Running the Example
421+
422+
```bash
423+
cd hol/polygram/reviewers_test_here
424+
./prepp.sh
425+
```
426+
427+
#### Inspecting the Result
428+
429+
```bash
430+
cd hol/polygram/reviewers_test_here
431+
hol
432+
```
433+
434+
Then inside the HOL4 interactive session:
435+
436+
```sml
437+
load "policy_min_exampleTheory";
438+
open policy_min_exampleTheory;
439+
show_tags := true;
440+
```
441+
442+
The theorem to inspect is:
443+
444+
- `policy_min_exampleTheory.final_thm` : end-to-end equivalence between the original and minimized policy (there you can also see the minimized policy)
445+
446+
The theorem will show:
447+
448+
```
449+
[oracles: CakeML_policy_TCB, DISK_THM] [axioms: ] []
450+
⊢ THM_CONTENT
451+
```
452+
453+
We can modify the pipeline to get a non-oracle theorem. It is like Lego!
454+
455+
456+
#### Reproducing the Minimization
457+
458+
To modify the input policy and observe how PolyGram minimizes it, open the script:
459+
460+
```bash
461+
nano hol/polygram/reviewers_test_here/policy_min_exampleScript.sml
462+
```
463+
464+
You can add new rules, introduce unsatisfiable conditions, or reorder rules. For example, to add a redundant rule that is subsumed by Rule 1:
465+
466+
```sml
467+
(* New redundant rule: y1 AND z AND NOT y2 -> fwd(1)
468+
This is subsumed by Rule 1 since NOT y2 is always true when y1 holds *)
469+
val rule_new = "(arith_and ^a_y1 (arith_and ^a_z (arith_not ^a_y2)),
470+
action ("fwd",[1])):single_rule";
471+
```
472+
473+
Add it to the policy list:
474+
475+
```sml
476+
val arith_policy = "[
477+
^rule1;
478+
^rule_new; (* add here *)
479+
^rule2;
480+
...
481+
]:single_rule list";
482+
```
483+
484+
Then rerun:
485+
486+
```bash
487+
./prepp.sh
488+
```
489+
490+
PolyGram will produce the same minimized policy and a new equivalence proof, showing it correctly identified and removed the redundant rule.
491+
492+
To exit HOL4:
493+
494+
ctrl+d
405495

406496

407497
---

‎hol/polygram/policy_test_cases_cakeml_best/prepp.sh‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ echo "Done!"
1818

1919
cd ../policy_test_cases_cakeml_best
2020

21-
Holmake "paper_exampleTheory.uo"
21+
2222

2323

2424
for i in {1..7}; do

‎hol/polygram/reviewers_test_here/policy_min_exampleScript.sml‎

Lines changed: 156 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,156 @@
1+
open HolKernel boolLib liteLib simpLib Parse bossLib;
2+
open policy_arith_to_varTheory;
3+
open bdd_utilsLib;
4+
5+
val _ = new_theory "policy_min_example";
6+
7+
8+
(* ---------------------------------------------------------------------------
9+
Policy Minimization Example
10+
11+
This script demonstrates PolyGram's policy minimization on a
12+
policy defined over three predicates:
13+
14+
y1: tcp.dstport <= 1023 (standard service ports)
15+
y2: tcp.dstport >= 49152 (dynamic/ephemeral ports)
16+
z: ip.ttl >= 2 (packet has enough hops left)
17+
18+
19+
The input policy has 9 rules with several issues:
20+
- Rules that are unreachable due to match-first semantics
21+
- Rules with unsatisfiable conditions (e.g. y1 AND y2, which is empty)
22+
- Rules that are subsumed by earlier rules
23+
- Redundant conditions within a single rule
24+
25+
PolyGram generates a minimized policy and produces a certified proof
26+
that the minimized policy is semantically equivalent to the original.
27+
--------------------------------------------------------------------------- *)
28+
29+
30+
31+
Type single_rule = “:((string# num list) action_expr) arith_rule”;
32+
33+
34+
35+
(* Packet type descriptor: encodes the bit-vector width of each header field
36+
Used by trans-back to compute interval complements (Section IV-D) *)
37+
val test_pd_type = “["h", type_record [("ip", type_record [ ("ttl", type_length 8);]);
38+
("tcp", type_record [("dstPort", type_length 16)])]]”;
39+
40+
41+
42+
(* tcp.dstport <= 1023 (standard-service traffic) *)
43+
val y1 = “(arithm_le (lv_acc (lv_acc (lv_x "h") "tcp") "dstPort") ^(bdd_utilsLib.make_bv 1023 16))”;
44+
45+
(* tcp.dstport >= 49152 (dynamic-port traffic) *)
46+
val y2 = “(arithm_ge (lv_acc (lv_acc (lv_x "h") "tcp") "dstPort") ^(bdd_utilsLib.make_bv 49152 16))”;
47+
48+
(* ip.ttl >= 2 *)
49+
val z = “(arithm_ge (lv_acc (lv_acc (lv_x "h") "ip") "ttl") ^(bdd_utilsLib.make_bv 2 8))”;
50+
51+
52+
(* Lifted predicates *)
53+
54+
val a_y1 = “arith_a ^y1”;
55+
val a_y2 = “arith_a ^y2”;
56+
val a_z = “arith_a ^z”;
57+
58+
59+
(* -----------------------------------------------------------------------
60+
Bloated input policy (9 rules)
61+
62+
Rule 1: y1 AND z : fwd(1) standard ports, good TTL
63+
Rule 2: y1 AND z AND y2 ; fwd(1) UNSATISFIABLE: y1 AND y2 is empty
64+
(disjoint port ranges)
65+
Rule 3: y2 AND z : fwd(1) dynamic ports, good TTL
66+
Rule 4: y1 AND NOT y1: fwd(2) UNSATISFIABLE: always false
67+
Rule 5: y1 : fwd(1) subsumes Rule 1 (no z needed)
68+
but comes AFTER Rule 1 in match-first!
69+
Rule 6: NOT y1 AND NOT y2 AND z ; fwd(1) middle ports, good TTL
70+
Rule 7: y2 AND z AND NOT z ; fwd(1) UNSATISFIABLE: z AND NOT z is empty
71+
Rule 8: NOT z : fwd(2) bad TTL -> fwd(2)
72+
Rule 9: y1 AND NOT z : fwd(1) standard ports, bad TTL
73+
UNREACHABLE: Rule 8 fires first
74+
Default: drop
75+
----------------------------------------------------------------------- *)
76+
77+
78+
79+
80+
(* Rule 1: y1 AND z -> fwd(1) *)
81+
val rule1 = “(arith_and ^a_y1 ^a_z,
82+
action ("fwd",[1])):single_rule”;
83+
84+
(* Rule 2: y1 AND z AND y2 -> fwd(1) [UNSATISFIABLE: y1 AND y2 = empty] *)
85+
val rule2 = “(arith_and ^a_y1 (arith_and ^a_z ^a_y2),
86+
action ("fwd",[1])):single_rule”;
87+
88+
(* Rule 3: y2 AND z -> fwd(1) *)
89+
val rule3 = “(arith_and ^a_y2 ^a_z,
90+
action ("fwd",[1])):single_rule”;
91+
92+
(* Rule 4: y1 AND NOT y1 -> fwd(2) [UNSATISFIABLE: always false] *)
93+
val rule4 = “(arith_and ^a_y1 (arith_not ^a_y1),
94+
action ("fwd",[2])):single_rule”;
95+
96+
(* Rule 5: y1 -> fwd(1) [comes after Rule 1, partially subsumed] *)
97+
val rule5 = “(^a_y1,
98+
action ("fwd",[1])):single_rule”;
99+
100+
(* Rule 6: NOT y1 AND NOT y2 AND z -> fwd(1) middle ports, good TTL *)
101+
val rule6 = “(arith_and (arith_not ^a_y1) (arith_and (arith_not ^a_y2) ^a_z),
102+
action ("fwd",[1])):single_rule”;
103+
104+
(* Rule 7: y2 AND z AND NOT z -> fwd(1) [UNSATISFIABLE: z AND NOT z = empty] *)
105+
val rule7 = “(arith_and ^a_y2 (arith_and ^a_z (arith_not ^a_z)),
106+
action ("fwd",[1])):single_rule”;
107+
108+
(* Rule 8: NOT z -> fwd(2) bad TTL *)
109+
val rule8 = “(arith_not ^a_z,
110+
action ("fwd",[2])):single_rule”;
111+
112+
(* Rule 9: y1 AND NOT z -> fwd(1) [UNREACHABLE: Rule 8 fires first] *)
113+
val rule9 = “(arith_and ^a_y1 (arith_not ^a_z),
114+
action ("fwd",[1])):single_rule”;
115+
116+
val arith_policy_default = “(arith_a a_True, action ("drop",[])):single_rule”;
117+
118+
val arith_policy = “[
119+
^rule1;
120+
^rule2;
121+
^rule3;
122+
^rule4;
123+
^rule5;
124+
^rule6;
125+
^rule7;
126+
^rule8;
127+
^rule9;
128+
^arith_policy_default
129+
]:single_rule list”;
130+
131+
(* -----------------------------------------------------------------------
132+
Mapping m
133+
----------------------------------------------------------------------- *)
134+
135+
val policy_me = “[
136+
("y1", ^y1);
137+
("y2", ^y2);
138+
("z", ^z)
139+
]”;
140+
141+
(* Variable order *)
142+
val policy_order = “["y1"; "y2"; "z"]”;
143+
144+
(* -----------------------------------------------------------------------
145+
Policy minimization
146+
PolyGram generates a minimized policy and proves it equivalent to the
147+
bloated input policy above.
148+
----------------------------------------------------------------------- *)
149+
150+
val final_thm_res_eq_cake = fwd_proof_gen_eq_cake.gen_eq_policy_and_prove
151+
(arith_policy, policy_me, test_pd_type, policy_order,
152+
"policy_min_example");
153+
154+
155+
156+
val _ = export_theory ();

‎hol/polygram/reviewers_test_here/prepp.sh‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,3 +23,7 @@ for target in \
2323
done
2424

2525
Holmake "policy_equiv_exampleTheory.uo"
26+
27+
28+
Holmake "policy_min_exampleTheory.uo"
29+

0 commit comments

Comments
 (0)