1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
#http://www.securityfocus.com/infocus/1711
#http://coombs.anu.edu.au/ipfilter/examples.html
#http://hr.uoregon.edu/davidrl/rc.icmp
#http://www.cs.iupui.edu/~ddillow/N301/deMorgan.html
#demorgans law: ~(a + b) = ~a . ~b and ~(a . b) = ~a + ~b
#input eth0 proto tcp dport http:https accept;
#input eth0 proto icmp icmptype { echo-request timestamp-request } accept;
#input eth0 dest monitors.anchor.net.au accept;
#input eth0 dest localhost accept;
#input eth0 proto icmp icmptype host-unreachable accept;
#input eth+ {
# ! source { a b } proto icmp icmptype echo-request accept;
# };
#input eth+ and ( source a or source b ) and proto icmp and icmptype echo-request and target accept;
#input eth+ and not ( source a or source b ) and proto icmp and icmptypte er and accept;
# demorgans:
#input e and not source a and not source b and proto icmp and it er and a;
# semicolons = OR
# sibs = OR
# braces and chains = ()
# implicit gap between specifier = AND
# ! = NOT
# specifiers are predicates
# targets are actions to perform. actions have side effects, predicates do not
# guarded expressions
# filtergen:
input eth0 source { c d } accept;
input eth0 ! source { a b } accept;
#||
# lisp-like:
#(and (input eth0) (not ((source a) or (source b))) (accept));
#
#input eth0 accept;
#output eth0 accept;
#||
#(or (and (input eth0) (accept)) (and (output eth0) (accept)))
# also:
#{input eth0; output eth0} accept;
#||
#(and (or (input eth0) (output eth0)) (accept))
#which by factorisation of the above:
#(or (and input accept) (and output accept))
#||
#(input eth0) * (accept) + (output eth0) * (accept)
#||
#(accept) * ((input eth0) + (output eth0))
#||
#(and accept (or input output)
# expands to:
#input accept
#output accept
#
#
# ORDER MATTERS when factoring/expanding, e.g.:
#
# order of targets matters, actions on same predicates
# are not swappable (commutative?)
#
# input eth0 {
# proto icmp accept;
# proto tcp dport auth reject;
# proto { tcp udp } dport domain accept;
#};
#=
#(and input (or (and proto accept) (and proto dport reject) (and (or proto proto) dport accept)))
#expands to:
#input proto accept [1]
#input proto dport reject [2]
#input proto dport accept [3]
#input proto dport accept [4]
# where 3,4's target is explicitly after [2] target inthe initial input
#
# TODO: prove that reordering targets has congruence
COMMUTATIVITY OF RULES
if two consecutive rules are sufficiently different, i.e. they are non overlapping predicate sets (???) then their order may be swapped
# expression reduction:
# fold duplicates, e.g.: (list reduction)
# (and x x) = x
# (or x x) = x
# pull out common factors, e.g.:
# (or (and x y) (and y z)) = (and y (or x z))
# special case optimisations:
# (or (host a) (host b)) = (host a+b) iff a and b are the sole elements of
# a CIDR set
# (or (port a) (port b)) = (port a:b) iff a and b are consecutive ports
# common factor puller outerer
# at each binary operator node (i.e. "and" or "or")
# if both children are binary operators of the opposite kind (i.e. "or" or "and" respectively
# for each item in the first list:
# if item in second list
# pull out item from both lists
# reverse operators
# place item in top list
# place sublists in new
#two list reductions
# common factor extraction
# (or (and x y) (and y z))
# y (or (and x) (and z))
# (and y (or (and x) (and z)))
# (and y (or x z))
# (or (and x y z) (and a y z))
# ^^ ^ ^
# x in (a y z)? no
# (or (and x y z) (and a y z))
# ^^ ^ ^
# y in (a y z)? yes
# (and y (or (and x z) (and a z)))
# ^ ^ ^ ^
# z in (a z)? yes
# (and y (or (and x z) (and a z)))
# ^ ^ ^ ^
# (and y z (or (and x) (and z)
# (and y z (or x z)) # singles reduction
#one list reductions
# duplicate reduction
# (and x x)
# (and x)
#
# (or x y x)
# (or x y)
#
# singles reduction
# (and x)
# x
http://hopper.unco.edu/KARNAUGH/Algorithm.html
http://134.193.15.25/vu/course/cs281/lectures/boolean-algebra/boolean-algebra.html
http://sunsite.wits.ac.za/math/firewall.htm
http://www.cisco.com/univercd/cc/td/doc/product/software/
http://arxiv.org/abs/cs.NI/0008006
|
