seccomp.bend

bend-osdev-bpf@0.1.0.0 · 329 lines · 39 definitions

1# bend-osdev-bpf: seccomp filters (the seccomp(2) manual page).
2#
3# A seccomp filter is a classic BPF program run over struct seccomp_data:
4#   int nr; __u32 arch; __u64 instruction_pointer; __u64 args[6];
5# 64 bytes, in the host's byte order, which is also the order of the
6# filter's loads (little-endian on x86-64 and arm64). Its answer is a
7# SECCOMP_RET_* value: the action in the high 16 bits, data in the low 16.
8# With several filters installed, every one runs, the most recently
9# installed first, and the answer is the first-seen action of the highest
10# precedence, with its data: KILL_PROCESS, KILL_THREAD, TRAP, ERRNO,
11# USER_NOTIF, TRACE, LOG, ALLOW, in decreasing order. An action value the
12# manual page does not name is treated as KILL_PROCESS.
13#
14# A seccomp filter loads only 32-bit words at aligned offsets inside
15# seccomp_data (BPF_LD | BPF_W | BPF_ABS), and Linux refuses BPF_MOD in a
16# seccomp filter (observed on the running kernel: the manual page does not
17# list the instructions); seccomp_validate adds those rules to
18# bpf_validate's. BPF_LEN loads give 64, the size of seccomp_data.
19import Base
20import bend-osdev-bytes@0.1.0.0/bytes.bend as B
21import bend-osdev-word64@0.1.0.0/word64.bend as W
22import bend-osdev-bpf@0.1.0.0/insn.bend as I
23import bend-osdev-bpf@0.1.0.0/validate.bend as V
24import bend-osdev-bpf@0.1.0.0/bpf.bend as R
25
26# The input
27
28type SeccompData is Data:
29  SeccompData{nr: U32, arch: U32, ip: W.W64, a0: W.W64, a1: W.W64, a2: W.W64, a3: W.W64, a4: W.W64, a5: W.W64}
30
31def SeccompData.field32(order: I.BpfOrder, v: U32) -> B.Octets:
32  match order:
33    case I.BpfLittle{}:
34      B.Octets.le32(v)
35    case I.BpfBig{}:
36      B.Octets.be32(v)
37
38def SeccompData.field64(order: I.BpfOrder, v: W.W64) -> B.Octets:
39  match order:
40    case I.BpfLittle{}:
41      B.Octets.le64(v)
42    case I.BpfBig{}:
43      B.Octets.be64(v)
44
45# the 64 bytes of struct seccomp_data, in the given byte order
46def SeccompData.to_octets(+order: I.BpfOrder, d: SeccompData) -> B.Octets:
47  match d:
48    case SeccompData{nr, arch, ip, a0, a1, a2, a3, a4, a5}:
49      B.Octets.concat([SeccompData.field32(order, nr), SeccompData.field32(order, arch), SeccompData.field64(order, ip), SeccompData.field64(order, a0), SeccompData.field64(order, a1), SeccompData.field64(order, a2), SeccompData.field64(order, a3), SeccompData.field64(order, a4), SeccompData.field64(order, a5)])
50
51def SeccompData.input(+order: I.BpfOrder, d: SeccompData) -> R.BpfInput:
52  R.BpfInput{order, SeccompData.to_octets(order, d)}
53
54# the byte order of x86-64 and arm64, the usual hosts
55def seccomp_order() -> I.BpfOrder:
56  I.BpfLittle{}
57
58def seccomp_data_size() -> U32:
59  64
60
61# AUDIT_ARCH_* values for seccomp_data.arch, and the x32 system call bit
62def seccomp_arch_x86_64() -> U32:
63  3221225534
64
65def seccomp_arch_i386() -> U32:
66  1073741827
67
68def seccomp_arch_aarch64() -> U32:
69  3221225655
70
71def seccomp_x32_syscall_bit() -> U32:
72  1073741824
73
74# Actions
75
76type SeccompAction is Data:
77  SeccompKillProcess{}
78  SeccompKillThread{}
79  SeccompTrap{data: U32}
80  SeccompErrno{data: U32}
81  SeccompUserNotif{}
82  SeccompTrace{data: U32}
83  SeccompLog{}
84  SeccompAllow{}
85
86def SeccompAction.pick(hit: Bool, a: SeccompAction, rest: SeccompAction) -> SeccompAction:
87  match hit:
88    case True{}:
89      a
90    case False{}:
91      rest
92
93# the action of a SECCOMP_RET_* value: SECCOMP_RET_ACTION_FULL (0xffff0000)
94# selects the action, SECCOMP_RET_DATA (0xffff) the data
95def SeccompAction.of_u32(+v: U32) -> SeccompAction:
96  +act = U32.and(4294901760, v)
97  +d = U32.and(65535, v)
98  SeccompAction.pick(U32.is_eq(act, 2147483648), SeccompKillProcess{},
99    SeccompAction.pick(U32.is_eq(act, 0), SeccompKillThread{},
100    SeccompAction.pick(U32.is_eq(act, 196608), SeccompTrap{d},
101    SeccompAction.pick(U32.is_eq(act, 327680), SeccompErrno{d},
102    SeccompAction.pick(U32.is_eq(act, 2143289344), SeccompUserNotif{},
103    SeccompAction.pick(U32.is_eq(act, 2146435072), SeccompTrace{d},
104    SeccompAction.pick(U32.is_eq(act, 2147221504), SeccompLog{},
105    SeccompAction.pick(U32.is_eq(act, 2147418112), SeccompAllow{},
106    SeccompKillProcess{}))))))))
107
108# the SECCOMP_RET_* value of an action, with the low 16 bits of its data
109def SeccompAction.to_u32(a: SeccompAction) -> U32:
110  match a:
111    case SeccompKillProcess{}:
112      2147483648
113    case SeccompKillThread{}:
114      0
115    case SeccompTrap{d}:
116      U32.or(196608, U32.and(65535, d))
117    case SeccompErrno{d}:
118      U32.or(327680, U32.and(65535, d))
119    case SeccompUserNotif{}:
120      2143289344
121    case SeccompTrace{d}:
122      U32.or(2146435072, U32.and(65535, d))
123    case SeccompLog{}:
124      2147221504
125    case SeccompAllow{}:
126      2147418112
127
128# the same action with its data cut to the 16 bits a return value holds
129def SeccompAction.clip(a: SeccompAction) -> SeccompAction:
130  match a:
131    case SeccompTrap{d}:
132      SeccompTrap{U32.and(65535, d)}
133    case SeccompErrno{d}:
134      SeccompErrno{U32.and(65535, d)}
135    case SeccompTrace{d}:
136      SeccompTrace{U32.and(65535, d)}
137    case other:
138      other
139
140# the precedence: 0 for KILL_PROCESS, the most restrictive, to 7 for ALLOW
141def SeccompAction.rank(a: SeccompAction) -> Nat:
142  match a:
143    case SeccompKillProcess{}:
144      0n
145    case SeccompKillThread{}:
146      1n
147    case SeccompTrap{d}:
148      2n
149    case SeccompErrno{d}:
150      3n
151    case SeccompUserNotif{}:
152      4n
153    case SeccompTrace{d}:
154      5n
155    case SeccompLog{}:
156      6n
157    case SeccompAllow{}:
158      7n
159
160def SeccompAction.show(a: SeccompAction) -> String:
161  match a:
162    case SeccompKillProcess{}:
163      "KILL_PROCESS"
164    case SeccompKillThread{}:
165      "KILL_THREAD"
166    case SeccompTrap{d}:
167      "TRAP(" ++ U32.show(d) ++ ")"
168    case SeccompErrno{d}:
169      "ERRNO(" ++ U32.show(d) ++ ")"
170    case SeccompUserNotif{}:
171      "USER_NOTIF"
172    case SeccompTrace{d}:
173      "TRACE(" ++ U32.show(d) ++ ")"
174    case SeccompLog{}:
175      "LOG"
176    case SeccompAllow{}:
177      "ALLOW"
178
179def seccomp_combine.pick(newer_wins: Bool, newer: SeccompAction, older: SeccompAction) -> SeccompAction:
180  match newer_wins:
181    case True{}:
182      newer
183    case False{}:
184      older
185
186# the answer of two filters, given each one's: the higher precedence, and on
187# a tie the newer filter's action (with its data)
188def seccomp_combine(+newer: SeccompAction, +older: SeccompAction) -> SeccompAction:
189  seccomp_combine.pick(Nat.is_le(SeccompAction.rank(newer), SeccompAction.rank(older)), newer, older)
190
191# Validation
192
193def seccomp_check.word(+k: U32, +pc: Nat) -> Result<&2, &2, I.BpfError, Unit>:
194  V.bpf_chk(Bool.and(U32.is_eq(U32.and(k, 3), 0), U32.is_lt(k, seccomp_data_size())), I.BpfErrSeccompLoad{pc})
195
196def seccomp_check.abs(size: I.BpfSize, +k: U32, +pc: Nat) -> Result<&2, &2, I.BpfError, Unit>:
197  match size:
198    case I.BpfW{}:
199      seccomp_check.word(k, pc)
200    case other:
201      Fail{I.BpfErrSeccompLoad{pc}}
202
203def seccomp_check.alu(o: I.BpfAluOp, pc: Nat) -> Result<&2, &2, I.BpfError, Unit>:
204  match o:
205    case I.BpfMod{}:
206      Fail{I.BpfErrSeccompInsn{pc}}
207    case other:
208      Done{Unit{}}
209
210def seccomp_check.op(op: I.BpfOp, +pc: Nat) -> Result<&2, &2, I.BpfError, Unit>:
211  match op:
212    case I.BpfLdAbs{size, k}:
213      seccomp_check.abs(size, k, pc)
214    case I.BpfLdInd{size, k}:
215      Fail{I.BpfErrSeccompLoad{pc}}
216    case I.BpfLdxMsh{k}:
217      Fail{I.BpfErrSeccompLoad{pc}}
218    case I.BpfAlu{o, src}:
219      seccomp_check.alu(o, pc)
220    case other:
221      Done{Unit{}}
222
223# ok is the verdict so far; the loop stops at the instruction after a failure
224def seccomp_check.go(xs: List<&2, I.BpfOp>, +pc: Nat, ok: Result<&2, &2, I.BpfError, Unit>) -> Result<&2, &2, I.BpfError, Unit>:
225  match xs:
226    case Nil{}:
227      ok
228    case Con{op, t}:
229      match ok:
230        case Fail{e}:
231          Fail{e}
232        case Done{u}:
233          seccomp_check.go(t, 1n+pc, seccomp_check.op(op, pc))
234
235def seccomp_validate.go(v: Result<&2, &2, I.BpfError, Unit>, +prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, Unit>:
236  match v:
237    case Fail{e}:
238      Fail{e}
239    case Done{u}:
240      seccomp_check.go(prog, 0n, Done{Unit{}})
241
242# bpf_validate's rules, only aligned 32-bit loads inside seccomp_data, and
243# no BPF_MOD (checked once bpf_validate's rules hold)
244def seccomp_validate_with(opts: V.BpfValidateOptions, +prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, Unit>:
245  seccomp_validate.go(V.bpf_validate_with(opts, prog), prog)
246
247# the default options (what Linux checks), with this instruction limit
248def seccomp_validate(limit: Nat, +prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, Unit>:
249  seccomp_validate_with(V.BpfValidateOptions{limit, True{}}, prog)
250
251# Running
252
253def seccomp_run.fin(r: Result<&2, &2, I.BpfError, U32>) -> Result<&2, &2, I.BpfError, SeccompAction>:
254  match r:
255    case Fail{e}:
256      Fail{e}
257    case Done{v}:
258      Done{SeccompAction.of_u32(v)}
259
260# one filter's action for a system call
261def seccomp_run(+order: I.BpfOrder, prog: List<&2, I.BpfOp>, d: SeccompData) -> Result<&2, &2, I.BpfError, SeccompAction>:
262  seccomp_run.fin(R.bpf_run(SeccompData.input(order, d), prog))
263
264def seccomp_eval.join(r: Result<&2, &2, I.BpfError, SeccompAction>, s: Result<&2, &2, I.BpfError, SeccompAction>) -> Result<&2, &2, I.BpfError, SeccompAction>:
265  match r:
266    case Fail{e}:
267      Fail{e}
268    case Done{a}:
269      match s:
270        case Fail{e}:
271          Fail{e}
272        case Done{b}:
273          Done{seccomp_combine(a, b)}
274
275# the action of a stack of filters, the most recently installed first; with
276# no filter, ALLOW
277def seccomp_eval(stack: List<&2, List<&2, I.BpfOp>>, +order: I.BpfOrder, +d: SeccompData) -> Result<&2, &2, I.BpfError, SeccompAction>:
278  match stack:
279    case Nil{}:
280      Done{SeccompAllow{}}
281    case Con{f, rest}:
282      seccomp_eval.join(seccomp_run(order, f, d), seccomp_eval(rest, order, d))
283
284# Installing
285
286# the limits on one filter (BPF_MAXINSNS) and on all the filters of a
287# thread together (MAX_INSNS_PER_PATH), where each filter already installed
288# counts 4 instructions more than its length
289type SeccompLimits is Data:
290  SeccompLimits{filter: Nat, path: Nat}
291
292def seccomp_limits() -> SeccompLimits:
293  SeccompLimits{V.bpf_maxinsns(), 32768n}
294
295def seccomp_path_len(stack: List<&2, List<&2, I.BpfOp>>) -> Nat:
296  match stack:
297    case Nil{}:
298      0n
299    case Con{f, rest}:
300      Nat.add(Nat.add(V.bpf_count(f), 4n), seccomp_path_len(rest))
301
302def seccomp_install.fit(fits: Bool, total: Nat, ops: List<&2, I.BpfOp>, stack: List<&2, List<&2, I.BpfOp>>) -> Result<&2, &2, I.BpfError, List<&2, List<&2, I.BpfOp>>>:
303  match fits:
304    case True{}:
305      Done{Con{ops, stack}}
306    case False{}:
307      Fail{I.BpfErrPathTooLong{total}}
308
309def seccomp_install.ok(v: Result<&2, &2, I.BpfError, Unit>, path: Nat, +ops: List<&2, I.BpfOp>, +stack: List<&2, List<&2, I.BpfOp>>) -> Result<&2, &2, I.BpfError, List<&2, List<&2, I.BpfOp>>>:
310  match v:
311    case Fail{e}:
312      Fail{e}
313    case Done{u}:
314      +total = Nat.add(V.bpf_count(ops), seccomp_path_len(stack))
315      seccomp_install.fit(Nat.is_le(total, path), total, ops, stack)
316
317def seccomp_install.go(lim: SeccompLimits, d: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, stack: List<&2, List<&2, I.BpfOp>>) -> Result<&2, &2, I.BpfError, List<&2, List<&2, I.BpfOp>>>:
318  match lim:
319    case SeccompLimits{filter, path}:
320      match d:
321        case Fail{e}:
322          Fail{e}
323        case Done{+ops}:
324          seccomp_install.ok(seccomp_validate(filter, ops), path, ops, stack)
325
326# decode a stored filter, validate it for seccomp, and put it on top of the
327# stack, as SECCOMP_SET_MODE_FILTER does
328def seccomp_install(lim: SeccompLimits, stack: List<&2, List<&2, I.BpfOp>>, rs: List<&2, I.BpfRaw>) -> Result<&2, &2, I.BpfError, List<&2, List<&2, I.BpfOp>>>:
329  seccomp_install.go(lim, I.bpf_decode(rs), stack)