rule_network.bend

bend-osdev-apparmor@0.1.0.0 · 196 lines · 27 definitions

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.
7import Base
8import bend-osdev-apparmor@0.1.0.0/text.bend as X
9import bend-osdev-apparmor@0.1.0.0/perm.bend as P
10import bend-osdev-apparmor@0.1.0.0/token.bend as T
11import bend-osdev-apparmor@0.1.0.0/error.bend as E
12import bend-osdev-apparmor@0.1.0.0/rule.bend as R
13
14type 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)
19type AaNetQuery is Data:
20  AaNetQuery{domain: List<&2, U32>, stype: List<&2, U32>, proto: List<&2, U32>}
21
22def 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
25def AaNet.types() -> List<&2, String>:
26  ["stream", "dgram", "seqpacket", "rdm", "raw", "packet"]
27
28def AaNet.protos() -> List<&2, String>:
29  ["tcp", "udp", "icmp"]
30
31# the access permissions of fine-grained rules (not modelled)
32def 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
36def 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
39def 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
52def 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
63def 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
68def 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
73def 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
83def 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
102def 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
105def 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)
117def 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
128def 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
133def 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`
143def 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
148def 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
155def 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
162def 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
169def 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
176def 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
185def AaNetRule.grants(rs: List<&2, AaNetRule>, +q: AaNetQuery) -> List<&2, P.AaGrant>:
186  AaNetRule.grants.of(AaNetRule.matching(rs, q))
187
188def 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
195def AaNetQuery.req() -> P.AaPerms:
196  P.AaPerms.bit(0n)