validate.bend

bend-osdev-bpf@0.1.0.0 · 289 lines · 37 definitions

1# bend-osdev-bpf: validating a classic BPF program before it runs.
2#
3# The rules of the BSD bpf(4) manual page and McCanne and Jacobson (1993):
4#   * the program is not empty, and has at most limit instructions
5#     (BPF_MAXINSNS, 4096, by default);
6#   * every jump lands on an instruction of the program (jumps only move
7#     forward: their offsets are unsigned), and a conditional jump's offsets
8#     fit their 8-bit fields;
9#   * no instruction but a return or a jump can be the last, so the program
10#     ends in a return;
11#   * scratch memory indices are below BPF_MEMWORDS (16);
12#   * no division or modulo by a constant zero;
13#   * optionally (BpfValidateOptions.require_mem_init, on by default, as
14#     Linux checks socket filters and seccomp filters alike): a scratch slot
15#     is read only after every path from the start to the read has written
16#     it, where the instruction after a return counts as reached from the
17#     return (as Linux counts it: observed on the running kernel).
18# The opcodes themselves are checked when a program is decoded
19# (bpf_decode); bpf_prepare decodes and validates in one step.
20import Base
21import bend-osdev-bpf@0.1.0.0/insn.bend as I
22
23# BPF_MAXINSNS: the usual instruction limit
24def bpf_maxinsns() -> Nat:
25  4096n
26
27# the choices validation offers: the instruction limit, and whether every
28# scratch read must follow a write on every path
29type BpfValidateOptions is Data:
30  BpfValidateOptions{max_insns: Nat, require_mem_init: Bool}
31
32# what Linux checks: at most 4096 instructions, scratch written before read
33def BpfValidateOptions.default() -> BpfValidateOptions:
34  BpfValidateOptions{bpf_maxinsns(), True{}}
35
36# the rules of bpf(4) alone: scratch memory may be read before it is written
37def BpfValidateOptions.permissive() -> BpfValidateOptions:
38  BpfValidateOptions{bpf_maxinsns(), False{}}
39
40def bpf_chk(ok: Bool, e: I.BpfError) -> Result<&2, &2, I.BpfError, Unit>:
41  match ok:
42    case True{}:
43      Done{Unit{}}
44    case False{}:
45      Fail{e}
46
47def bpf_both(r: Result<&2, &2, I.BpfError, Unit>, s: Result<&2, &2, I.BpfError, Unit>) -> Result<&2, &2, I.BpfError, Unit>:
48  match r:
49    case Fail{e}:
50      Fail{e}
51    case Done{u}:
52      s
53
54# an instruction that goes on to the next one must not be the last
55def bpf_check.next(pc: Nat, r: Nat) -> Result<&2, &2, I.BpfError, Unit>:
56  bpf_chk(Nat.is_lt(0n, r), I.BpfErrNoReturn{pc})
57
58def bpf_check.k_div(src: I.BpfSrc, pc: Nat) -> Result<&2, &2, I.BpfError, Unit>:
59  match src:
60    case I.BpfK{k}:
61      bpf_chk(Bool.not(U32.is_zero(k)), I.BpfErrDivZero{pc})
62    case I.BpfX{}:
63      Done{Unit{}}
64
65def bpf_check.div(o: I.BpfAluOp, src: I.BpfSrc, pc: Nat) -> Result<&2, &2, I.BpfError, Unit>:
66  match o:
67    case I.BpfDiv{}:
68      bpf_check.k_div(src, pc)
69    case I.BpfMod{}:
70      bpf_check.k_div(src, pc)
71    case other:
72      Done{Unit{}}
73
74def bpf_check.mem(+k: U32, +pc: Nat, r: Nat) -> Result<&2, &2, I.BpfError, Unit>:
75  bpf_both(bpf_chk(U32.is_lt(k, I.bpf_memwords()), I.BpfErrScratch{pc}), bpf_check.next(pc, r))
76
77def bpf_check.jmp(+jt: U32, +jf: U32, +pc: Nat, +r: Nat) -> Result<&2, &2, I.BpfError, Unit>:
78  bpf_both(bpf_chk(U32.is_lt(jt, 256), I.BpfErrJumpField{pc}), bpf_both(bpf_chk(U32.is_lt(jf, 256), I.BpfErrJumpField{pc}), bpf_both(bpf_chk(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}), bpf_chk(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc}))))
79
80# the checks of one instruction at index pc, with r instructions after it
81def bpf_check.op(op: I.BpfOp, +pc: Nat, +r: Nat) -> Result<&2, &2, I.BpfError, Unit>:
82  match op:
83    case I.BpfLdMem{k}:
84      bpf_check.mem(k, pc, r)
85    case I.BpfLdxMem{k}:
86      bpf_check.mem(k, pc, r)
87    case I.BpfSt{k}:
88      bpf_check.mem(k, pc, r)
89    case I.BpfStx{k}:
90      bpf_check.mem(k, pc, r)
91    case I.BpfAlu{o, src}:
92      bpf_both(bpf_check.div(o, src, pc), bpf_check.next(pc, r))
93    case I.BpfJa{k}:
94      bpf_chk(Nat.is_lt(U32.to_nat(k), r), I.BpfErrJump{pc})
95    case I.BpfJmp{c, src, jt, jf}:
96      bpf_check.jmp(jt, jf, pc, r)
97    case I.BpfRet{v}:
98      Done{Unit{}}
99    case other:
100      bpf_check.next(pc, r)
101
102# the instructions' own checks, structurally: the reference the proofs
103# reason about (PROOF.bend: F_check ties bpf_check.go to it)
104def bpf_check.all(xs: List<&2, I.BpfOp>, +pc: Nat) -> Result<&2, &2, I.BpfError, Unit>:
105  match xs:
106    case Nil{}:
107      Done{Unit{}}
108    case Con{op, +t}:
109      bpf_both(bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), bpf_check.all(t, 1n+pc))
110
111# the same as a tail call: ok is the verdict so far, and n counts the
112# instructions from pc on; the loop stops at the instruction after a failure
113def bpf_check.go(xs: List<&2, I.BpfOp>, +pc: Nat, ok: Result<&2, &2, I.BpfError, Unit>, n: Nat) -> Result<&2, &2, I.BpfError, Unit>:
114  match xs:
115    case Nil{}:
116      ok
117    case Con{op, t}:
118      match ok:
119        case Fail{e}:
120          Fail{e}
121        case Done{u}:
122          match n:
123            case 0n:
124              bpf_check.go(t, 1n+pc, bpf_check.op(op, pc, 0n), 0n)
125            case 1n+(+r):
126              bpf_check.go(t, 1n+pc, bpf_check.op(op, pc, r), r)
127
128# the number of instructions, as a tail call (PROOF.bend: F_count)
129def bpf_count.go(xs: List<&2, I.BpfOp>, n: Nat) -> Nat:
130  match xs:
131    case Nil{}:
132      n
133    case Con{h, t}:
134      bpf_count.go(t, 1n+n)
135
136def bpf_count(xs: List<&2, I.BpfOp>) -> Nat:
137  bpf_count.go(xs, 0n)
138
139def bpf_check.len(+n: Nat, limit: Nat) -> Result<&2, &2, I.BpfError, Unit>:
140  bpf_both(bpf_chk(Nat.is_lt(0n, n), I.BpfErrEmpty{}), bpf_chk(Nat.is_le(n, limit), I.BpfErrTooLong{n}))
141
142# Scratch memory written before it is read. One pass over the instructions
143# keeps, for each instruction still ahead, the slots written on every jump to
144# it so far (a 16-bit mask, 65535 while no jump reaches it), and the slots
145# written on the path falling into the next one.
146
147def bpf_mem.bit.go(small: Bool, k: U32) -> U32:
148  match small:
149    case True{}:
150      U32.shln(1, U32.to_nat(k))
151    case False{}:
152      0
153
154def bpf_mem.bit(+k: U32) -> U32:
155  bpf_mem.bit.go(U32.is_lt(k, I.bpf_memwords()), k)
156
157# meet the n-th mask ahead with m (acc: the masks before it, last first)
158def bpf_mem.meet.go(ahead: List<&2, U32>, n: Nat, +m: U32, acc: List<&2, U32>) -> List<&2, U32>:
159  match ahead:
160    case Nil{}:
161      List.reverse(&2, U32, acc)
162    case Con{h, t}:
163      match n:
164        case 0n:
165          List.reverse.go(&2, U32, acc, Con{U32.and(h, m), t})
166        case 1n+p:
167          bpf_mem.meet.go(t, p, m, Con{h, acc})
168
169def bpf_mem.meet(ahead: List<&2, U32>, n: Nat, +m: U32) -> List<&2, U32>:
170  bpf_mem.meet.go(ahead, n, m, Nil{})
171
172type BpfInitStep is Data:
173  BpfInitStep{ok: Result<&2, &2, I.BpfError, Unit>, fall: U32, ahead: List<&2, U32>}
174
175def bpf_mem.read(+pc: Nat, +now: U32, +k: U32, ahead: List<&2, U32>) -> BpfInitStep:
176  BpfInitStep{bpf_chk(Bool.not(U32.is_zero(U32.and(now, bpf_mem.bit(k)))), I.BpfErrMemInit{pc}), now, ahead}
177
178# one instruction, given the slots written on every path to it
179def bpf_mem.step(op: I.BpfOp, +pc: Nat, +now: U32, ahead: List<&2, U32>) -> BpfInitStep:
180  match op:
181    case I.BpfLdMem{k}:
182      bpf_mem.read(pc, now, k, ahead)
183    case I.BpfLdxMem{k}:
184      bpf_mem.read(pc, now, k, ahead)
185    case I.BpfSt{k}:
186      BpfInitStep{Done{Unit{}}, U32.or(now, bpf_mem.bit(k)), ahead}
187    case I.BpfStx{k}:
188      BpfInitStep{Done{Unit{}}, U32.or(now, bpf_mem.bit(k)), ahead}
189    case I.BpfJa{k}:
190      BpfInitStep{Done{Unit{}}, 65535, bpf_mem.meet(ahead, U32.to_nat(k), now)}
191    case I.BpfJmp{c, src, jt, jf}:
192      BpfInitStep{Done{Unit{}}, 65535, bpf_mem.meet(bpf_mem.meet(ahead, U32.to_nat(jt), now), U32.to_nat(jf), now)}
193    case other:
194      BpfInitStep{Done{Unit{}}, now, ahead}
195
196def bpf_mem.head(ahead: List<&2, U32>) -> U32:
197  match ahead:
198    case Nil{}:
199      65535
200    case Con{h, t}:
201      h
202
203def bpf_mem.tail(ahead: List<&2, U32>) -> List<&2, U32>:
204  match ahead:
205    case Nil{}:
206      Nil{}
207    case Con{h, t}:
208      t
209
210def bpf_mem.go(xs: List<&2, I.BpfOp>, +pc: Nat, st: BpfInitStep) -> Result<&2, &2, I.BpfError, Unit>:
211  match xs:
212    case Nil{}:
213      match st:
214        case BpfInitStep{ok, fall, ahead}:
215          ok
216    case Con{op, t}:
217      match st:
218        case BpfInitStep{ok, fall, +ahead}:
219          match ok:
220            case Fail{e}:
221              Fail{e}
222            case Done{u}:
223              bpf_mem.go(t, 1n+pc, bpf_mem.step(op, pc, U32.and(fall, bpf_mem.head(ahead)), bpf_mem.tail(ahead)))
224
225# n masks of 65535: no jump reaches any instruction yet
226def bpf_mem.none(n: Nat, acc: List<&2, U32>) -> List<&2, U32>:
227  match n:
228    case 0n:
229      acc
230    case 1n+p:
231      bpf_mem.none(p, Con{65535, acc})
232
233def bpf_check.mem_init(need: Bool, n: Nat, +prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, Unit>:
234  match need:
235    case False{}:
236      Done{Unit{}}
237    case True{}:
238      bpf_mem.go(prog, 0n, BpfInitStep{Done{Unit{}}, 0, bpf_mem.none(n, Nil{})})
239
240# The rules in order, each pass only once the ones before it hold: the
241# length, the instructions' own rules, then scratch memory
242
243def bpf_validate.mem(v: Result<&2, &2, I.BpfError, Unit>, need: Bool, n: Nat, +prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, Unit>:
244  match v:
245    case Fail{e}:
246      Fail{e}
247    case Done{u}:
248      bpf_check.mem_init(need, n, prog)
249
250def bpf_validate.ops(v: Result<&2, &2, I.BpfError, Unit>, +n: Nat, need: Bool, +prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, Unit>:
251  match v:
252    case Fail{e}:
253      Fail{e}
254    case Done{u}:
255      bpf_validate.mem(bpf_check.go(prog, 0n, Done{Unit{}}, n), need, n, prog)
256
257# Done{Unit{}} if the program may run, or the first rule it breaks: the
258# length, then each instruction's own rules in order, then scratch memory
259def bpf_validate_with(opts: BpfValidateOptions, +prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, Unit>:
260  match opts:
261    case BpfValidateOptions{max, need}:
262      +n = bpf_count(prog)
263      bpf_validate.ops(bpf_check.len(n, max), n, need, prog)
264
265# the default options, with this instruction limit
266def bpf_validate(limit: Nat, +prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, Unit>:
267  bpf_validate_with(BpfValidateOptions{limit, True{}}, prog)
268
269def bpf_prepare.ok(v: Result<&2, &2, I.BpfError, Unit>, ops: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>:
270  match v:
271    case Fail{e}:
272      Fail{e}
273    case Done{u}:
274      Done{ops}
275
276def bpf_prepare.go(opts: BpfValidateOptions, d: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>:
277  match d:
278    case Fail{e}:
279      Fail{e}
280    case Done{+ops}:
281      bpf_prepare.ok(bpf_validate_with(opts, ops), ops)
282
283# decode a stored program and validate it: the instructions, ready to run
284def bpf_prepare_with(opts: BpfValidateOptions, rs: List<&2, I.BpfRaw>) -> Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>:
285  bpf_prepare.go(opts, I.bpf_decode(rs))
286
287# the same, with the default options and this instruction limit
288def bpf_prepare(limit: Nat, rs: List<&2, I.BpfRaw>) -> Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>:
289  bpf_prepare_with(BpfValidateOptions{limit, True{}}, rs)