1	# bend-osdev-apparmor: network rules (apparmor.d(5), "NETWORK RULE",
2	# "Network Rules"): `network [DOMAIN] [TYPE | PROTOCOL]`, coarse-grained
3	# mediation by address family, socket type and protocol. Rules become more
4	# restrictive as more is given and accumulate as a union. Access lists and
5	# the ip, port and peer conditions (fine-grained inet mediation) are outside
6	# the model. One permission bit: use.
7	import Base
8	import ./text.bend as X
9	import ./perm.bend as P
10	import ./token.bend as T
11	import ./error.bend as E
12	import ./rule.bend as R
13	
14	type AaNetRule is Data:
15	  AaNetRule{qual: P.AaQual, domain: Maybe<&2, List<&2, U32>>, stype: Maybe<&2, List<&2, U32>>, proto: Maybe<&2, List<&2, U32>>}
16	
17	# a socket: its domain (inet, unix, ...), type (stream, dgram, ...) and
18	# protocol (tcp, udp, icmp, or empty)
19	type AaNetQuery is Data:
20	  AaNetQuery{domain: List<&2, U32>, stype: List<&2, U32>, proto: List<&2, U32>}
21	
22	def AaNet.domains() -> List<&2, String>:
23	  ["unix", "inet", "ax25", "ipx", "appletalk", "netrom", "bridge", "atmpvc", "x25", "inet6", "rose", "netbeui", "security", "key", "netlink", "packet", "ash", "econet", "atmsvc", "rds", "sna", "irda", "pppox", "wanpipe", "llc", "ib", "mpls", "can", "tipc", "bluetooth", "iucv", "rxrpc", "isdn", "phonet", "ieee802154", "caif", "alg", "nfc", "vsock", "kcm", "qipcrtr", "smc", "xdp", "mctp"]
24	
25	def AaNet.types() -> List<&2, String>:
26	  ["stream", "dgram", "seqpacket", "rdm", "raw", "packet"]
27	
28	def AaNet.protos() -> List<&2, String>:
29	  ["tcp", "udp", "icmp"]
30	
31	# the access permissions of fine-grained rules (not modelled)
32	def AaNet.accesses() -> List<&2, String>:
33	  ["create", "bind", "listen", "accept", "connect", "shutdown", "getattr", "setattr", "getopt", "setopt", "send", "receive", "r", "w", "rw"]
34	
35	# what a word of a network rule is: 0 a domain, 1 a type, 2 a protocol, 3 an access (unsupported), 4 unknown
36	def AaNet.kind(+w: List<&2, U32>) -> Nat:
37	  Bool.pick(Nat, X.AaText.one_of(AaNet.domains(), w), 0n, Bool.pick(Nat, X.AaText.one_of(AaNet.types(), w), 1n, Bool.pick(Nat, X.AaText.one_of(AaNet.protos(), w), 2n, Bool.pick(Nat, X.AaText.one_of(AaNet.accesses(), w), 3n, 4n))))
38	
39	def AaNet.word(t: T.AaTerm, src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, U32>>:
40	  match t:
41	    case T.AaTmWord{w}:
42	      Done{w}
43	    case T.AaTmQuoted{q}:
44	      Fail{E.AaSrc.syntax(src)}
45	    case T.AaTmList{xs}:
46	      Fail{E.AaSrc.unsupported(src)}
47	    case T.AaTmCond{k, v}:
48	      Fail{E.AaSrc.unsupported(src)}
49	    case T.AaTmArrow{}:
50	      Fail{E.AaSrc.syntax(src)}
51	
52	def AaNet.add.kind(ty: Maybe<&2, List<&2, U32>>, pr: Maybe<&2, List<&2, U32>>, r: AaNetRule, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
53	  match ty:
54	    case Some{x}:
55	      Fail{E.AaSrc.syntax(src)}
56	    case None{}:
57	      match pr:
58	        case Some{y}:
59	          Fail{E.AaSrc.syntax(src)}
60	        case None{}:
61	          Done{r}
62	
63	def AaNet.set_type(r: AaNetRule, w: List<&2, U32>, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
64	  match r:
65	    case AaNetRule{q, d, +ty, +pr}:
66	      AaNet.add.kind(ty, pr, AaNetRule{q, d, Some{w}, pr}, src)
67	
68	def AaNet.set_proto(r: AaNetRule, w: List<&2, U32>, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
69	  match r:
70	    case AaNetRule{q, d, +ty, +pr}:
71	      AaNet.add.kind(ty, pr, AaNetRule{q, d, ty, Some{w}}, src)
72	
73	def AaNet.set_domain(first: Bool, r: AaNetRule, w: List<&2, U32>, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
74	  match first:
75	    case True{}:
76	      match r:
77	        case AaNetRule{q, d, ty, pr}:
78	          Done{AaNetRule{q, Some{w}, ty, pr}}
79	    case False{}:
80	      Fail{E.AaSrc.syntax(src)}
81	
82	# the rule so far and the next word: a domain only first, then at most one type or protocol
83	def AaNet.add(k: Nat, first: Bool, r: AaNetRule, w: List<&2, U32>, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
84	  match k:
85	    case 0n:
86	      AaNet.set_domain(first, r, w, src)
87	    case 1n+k1:
88	      match k1:
89	        case 0n:
90	          AaNet.set_type(r, w, src)
91	        case 1n+k2:
92	          match k2:
93	            case 0n:
94	              AaNet.set_proto(r, w, src)
95	            case 1n+k3:
96	              match k3:
97	                case 0n:
98	                  Fail{E.AaSrc.unsupported(src)}
99	                case 1n+k4:
100	                  Fail{E.AaSrc.name(src)}
101	
102	def AaNet.add.word(+w: List<&2, U32>, first: Bool, r: AaNetRule, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
103	  AaNet.add(AaNet.kind(w), first, r, w, src)
104	
105	def AaNet.parse.go(ts: List<&2, T.AaTerm>, r: AaNetRule, +first: Bool, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
106	  match ts:
107	    case Nil{}:
108	      Done{r}
109	    case Con{t, rest}:
110	      do Result<&2, &2, E.AaError, AaNetRule>:
111	        w : List<&2, U32> <- AaNet.word(t, src)
112	        r2 : AaNetRule <- AaNet.add.word(w, first, r, src)
113	        AaNet.parse.go(rest, r2, False{}, src)
114	
115	# a protocol needs the inet or inet6 domain, or none, and icmp is not inet6's
116	# (apparmor_parser 4.0.1: "Invalid network entry" otherwise)
117	def AaNet.proto_ok(d: Maybe<&2, List<&2, U32>>, pr: Maybe<&2, List<&2, U32>>) -> Bool:
118	  match d:
119	    case None{}:
120	      True{}
121	    case Some{+x}:
122	      match pr:
123	        case None{}:
124	          True{}
125	        case Some{+y}:
126	          Bool.or(X.AaText.is(x, "inet"), Bool.and(X.AaText.is(x, "inet6"), Bool.not(X.AaText.is(y, "icmp"))))
127	
128	def AaNet.check(r: AaNetRule, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
129	  match r:
130	    case AaNetRule{q, +d, ty, +pr}:
131	      Bool.pick(Result<&2, &2, E.AaError, AaNetRule>, AaNet.proto_ok(d, pr), Done{AaNetRule{q, d, ty, pr}}, Fail{E.AaSrc.name(src)})
132	
133	def AaNet.parse.q(r: Result<&2, &2, E.AaError, P.AaQual>, ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
134	  match r:
135	    case Fail{e}:
136	      Fail{e}
137	    case Done{q}:
138	      do Result<&2, &2, E.AaError, AaNetRule>:
139	        x : AaNetRule <- AaNet.parse.go(ts, AaNetRule{q, None{}, None{}, None{}}, True{}, src)
140	        AaNet.check(x, src)
141	
142	# the terms after `network`
143	def AaNet.parse(ts: List<&2, T.AaTerm>, q: P.AaQual, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaNetRule>:
144	  AaNet.parse.q(R.AaRule.no_owner(q, src), ts, src)
145	
146	# Matching
147	
148	def AaNet.opt_eq(m: Maybe<&2, List<&2, U32>>, x: List<&2, U32>) -> Bool:
149	  match m:
150	    case None{}:
151	      True{}
152	    case Some{y}:
153	      X.AaText.eq(y, x)
154	
155	def AaNetRule.matches(r: AaNetRule, q: AaNetQuery) -> Bool:
156	  match r:
157	    case AaNetRule{qu, d, ty, pr}:
158	      match q:
159	        case AaNetQuery{qd, qt, qp}:
160	          Bool.and(AaNet.opt_eq(d, qd), Bool.and(AaNet.opt_eq(ty, qt), AaNet.opt_eq(pr, qp)))
161	
162	def AaNetRule.matching.go(hit: Bool, r: AaNetRule, rest: List<&2, AaNetRule>) -> List<&2, AaNetRule>:
163	  match hit:
164	    case True{}:
165	      Con{r, rest}
166	    case False{}:
167	      rest
168	
169	def AaNetRule.matching(rs: List<&2, AaNetRule>, +q: AaNetQuery) -> List<&2, AaNetRule>:
170	  match rs:
171	    case Nil{}:
172	      Nil{}
173	    case Con{+r, t}:
174	      AaNetRule.matching.go(AaNetRule.matches(r, q), r, AaNetRule.matching(t, q))
175	
176	def AaNetRule.grants.of(rs: List<&2, AaNetRule>) -> List<&2, P.AaGrant>:
177	  match rs:
178	    case Nil{}:
179	      Nil{}
180	    case Con{r, t}:
181	      match r:
182	        case AaNetRule{qu, d, ty, pr}:
183	          Con{P.AaGrant.of(qu, P.AaPerms.bit(0n)), AaNetRule.grants.of(t)}
184	
185	def AaNetRule.grants(rs: List<&2, AaNetRule>, +q: AaNetQuery) -> List<&2, P.AaGrant>:
186	  AaNetRule.grants.of(AaNetRule.matching(rs, q))
187	
188	def AaNetRule.append(xs: List<&2, AaNetRule>, ys: List<&2, AaNetRule>) -> List<&2, AaNetRule>:
189	  match xs:
190	    case Nil{}:
191	      ys
192	    case Con{h, t}:
193	      Con{h, AaNetRule.append(t, ys)}
194	
195	def AaNetQuery.req() -> P.AaPerms:
196	  P.AaPerms.bit(0n)