bpf.bend

bend-osdev-bpf@0.1.0.0 · 346 lines · 38 definitions

1# bend-osdev-bpf: the classic BPF interpreter.
2#
3# The machine of the BSD bpf(4) manual page and McCanne and Jacobson, "The
4# BSD Packet Filter" (USENIX 1993): a 32-bit accumulator A, an index
5# register X, a scratch memory M[0..15], and an implicit program counter.
6# A, X and M start at 0. Every instruction class and addressing mode:
7#   LD   A <- P[k:4], P[k:2], P[k:1] (ABS), the same at X + k (IND), k (IMM),
8#        the input's length (LEN), M[k] (MEM)
9#   LDX  X <- k, M[k], the length, or 4 * (P[k:1] & 0xf) (MSH)
10#   ST   M[k] <- A;  STX  M[k] <- X
11#   ALU  A <- A op k or A op X, for + - * / | & << >> % ^ (32-bit, wrapping;
12#        a shift by 32 or more gives 0), and A <- -A (NEG)
13#   JMP  pc += k (JA); pc += (A op k or A op X) ? jt : jf, for = > >= and
14#        "A & operand is not zero" (JSET)
15#   RET  answer k, or A
16#   MISC X <- A (TAX), A <- X (TXA)
17# P is the input, read in its byte order (big-endian for packets). A load
18# outside the input, and a division or modulo by X = 0, end the program with
19# the answer 0, as bpf(4) documents.
20#
21# bpf_run runs any program; on a validated one (bpf_validate) it always
22# answers Done (a law). Its errors are what an unvalidated program can do:
23# run past its last instruction, or use a scratch index above 15.
24import Base
25import bend-osdev-bytes@0.1.0.0/bytes.bend as B
26import bend-osdev-bpf@0.1.0.0/insn.bend as I
27
28# What a filter runs over: bytes, and the byte order its loads use
29type BpfInput is Data:
30  BpfInput{order: I.BpfOrder, data: B.Octets}
31
32# a packet: loads are big-endian (network order)
33def bpf_packet(o: B.Octets) -> BpfInput:
34  BpfInput{I.BpfBig{}, o}
35
36# The machine
37
38type BpfState is Data:
39  BpfState{a: U32, x: U32, mem: List<&2, U32>}
40
41# what an instruction leads to: skip some instructions and go on, answer,
42# or fail
43type BpfStep is Data:
44  BpfNext{skip: Nat, st: BpfState}
45  BpfStop{value: U32}
46  BpfFault{error: I.BpfError}
47
48def bpf_init() -> BpfState:
49  BpfState{0, 0, List.replicate(U32, 16n, 0)}
50
51def bpf_get_a(st: BpfState) -> U32:
52  match st:
53    case BpfState{a, x, mem}:
54      a
55
56def bpf_set_a(st: BpfState, v: U32) -> BpfState:
57  match st:
58    case BpfState{a, x, mem}:
59      BpfState{v, x, mem}
60
61def bpf_set_x(st: BpfState, v: U32) -> BpfState:
62  match st:
63    case BpfState{a, x, mem}:
64      BpfState{a, v, mem}
65
66def bpf_set_a.m(m: Maybe<&2, U32>, st: BpfState) -> Maybe<&2, BpfState>:
67  match m:
68    case None{}:
69      None{}
70    case Some{v}:
71      Some{bpf_set_a(st, v)}
72
73def bpf_set_x.m(m: Maybe<&2, U32>, st: BpfState) -> Maybe<&2, BpfState>:
74  match m:
75    case None{}:
76      None{}
77    case Some{v}:
78      Some{bpf_set_x(st, v)}
79
80def bpf_tax(st: BpfState) -> BpfState:
81  match st:
82    case BpfState{+a, x, mem}:
83      BpfState{a, a, mem}
84
85def bpf_txa(st: BpfState) -> BpfState:
86  match st:
87    case BpfState{a, +x, mem}:
88      BpfState{x, x, mem}
89
90def bpf_neg(st: BpfState) -> BpfState:
91  match st:
92    case BpfState{a, x, mem}:
93      BpfState{U32.sub(0, a), x, mem}
94
95# a step that goes on to the next instruction, or ends the program with 0
96def bpf_step.of(m: Maybe<&2, BpfState>) -> BpfStep:
97  match m:
98    case None{}:
99      BpfStop{0}
100    case Some{st}:
101      BpfNext{0n, st}
102
103# Loads
104
105def bpf_load.at(order: I.BpfOrder, size: I.BpfSize, data: B.Octets, n: Nat) -> Maybe<&2, U32>:
106  match order:
107    case I.BpfBig{}:
108      match size:
109        case I.BpfW{}:
110          B.Octets.be32_at(data, n)
111        case I.BpfH{}:
112          B.Octets.be16_at(data, n)
113        case I.BpfB{}:
114          B.Octets.at(data, n)
115    case I.BpfLittle{}:
116      match size:
117        case I.BpfW{}:
118          B.Octets.le32_at(data, n)
119        case I.BpfH{}:
120          B.Octets.le16_at(data, n)
121        case I.BpfB{}:
122          B.Octets.at(data, n)
123
124def bpf_load(inp: BpfInput, size: I.BpfSize, k: U32) -> Maybe<&2, U32>:
125  match inp:
126    case BpfInput{order, data}:
127      bpf_load.at(order, size, data, U32.to_nat(k))
128
129# X + k does not wrap: an offset past 2^32 is outside the input
130def bpf_load.ind(inp: BpfInput, size: I.BpfSize, x: U32, k: U32) -> Maybe<&2, U32>:
131  match inp:
132    case BpfInput{order, data}:
133      bpf_load.at(order, size, data, Nat.add(U32.to_nat(x), U32.to_nat(k)))
134
135def bpf_load.msh.fin(m: Maybe<&2, U32>) -> Maybe<&2, U32>:
136  match m:
137    case None{}:
138      None{}
139    case Some{b}:
140      Some{U32.shln(U32.and(b, 15), 2n)}
141
142def bpf_load.msh(inp: BpfInput, k: U32) -> Maybe<&2, U32>:
143  match inp:
144    case BpfInput{order, data}:
145      bpf_load.msh.fin(B.Octets.at(data, U32.to_nat(k)))
146
147def bpf_len(inp: BpfInput) -> U32:
148  match inp:
149    case BpfInput{order, data}:
150      U32.from_nat(B.Octets.len(data))
151
152# Scratch memory
153
154def bpf_mem.get(mem: List<&2, U32>, k: U32) -> U32:
155  Maybe.default(&2, U32, List.get(&2, U32, mem, U32.to_nat(k)), 0)
156
157def bpf_mem.set(mem: List<&2, U32>, k: U32, v: U32) -> List<&2, U32>:
158  List.set(&2, U32, mem, U32.to_nat(k), v)
159
160def bpf_mem.lda(st: BpfState, k: U32) -> BpfState:
161  match st:
162    case BpfState{a, x, +mem}:
163      BpfState{bpf_mem.get(mem, k), x, mem}
164
165def bpf_mem.ldx(st: BpfState, k: U32) -> BpfState:
166  match st:
167    case BpfState{a, x, +mem}:
168      BpfState{a, bpf_mem.get(mem, k), mem}
169
170def bpf_mem.st(st: BpfState, k: U32) -> BpfState:
171  match st:
172    case BpfState{+a, x, mem}:
173      BpfState{a, x, bpf_mem.set(mem, k, a)}
174
175def bpf_mem.stx(st: BpfState, k: U32) -> BpfState:
176  match st:
177    case BpfState{a, +x, mem}:
178      BpfState{a, x, bpf_mem.set(mem, k, x)}
179
180# a scratch access goes on only if its index is in range
181def bpf_scratch(ok: Bool, k: U32, st: BpfState) -> BpfStep:
182  match ok:
183    case True{}:
184      BpfNext{0n, st}
185    case False{}:
186      BpfFault{I.BpfErrBadScratch{k}}
187
188# Arithmetic
189
190def bpf_src(src: I.BpfSrc, x: U32) -> U32:
191  match src:
192    case I.BpfK{k}:
193      k
194    case I.BpfX{}:
195      x
196
197def bpf_shl(small: Bool, a: U32, n: U32) -> U32:
198  match small:
199    case True{}:
200      U32.shln(a, U32.to_nat(n))
201    case False{}:
202      0
203
204def bpf_shr(small: Bool, a: U32, n: U32) -> U32:
205  match small:
206    case True{}:
207      U32.shrn(a, U32.to_nat(n))
208    case False{}:
209      0
210
211def bpf_div(zero: Bool, a: U32, v: U32) -> Maybe<&2, U32>:
212  match zero:
213    case True{}:
214      None{}
215    case False{}:
216      Some{U32.div(a, v)}
217
218def bpf_mod(zero: Bool, a: U32, v: U32) -> Maybe<&2, U32>:
219  match zero:
220    case True{}:
221      None{}
222    case False{}:
223      Some{U32.mod(a, v)}
224
225# A op v, or None for a division or modulo by zero
226def bpf_alu(o: I.BpfAluOp, +a: U32, +v: U32) -> Maybe<&2, U32>:
227  match o:
228    case I.BpfAdd{}:
229      Some{U32.add(a, v)}
230    case I.BpfSub{}:
231      Some{U32.sub(a, v)}
232    case I.BpfMul{}:
233      Some{U32.mul(a, v)}
234    case I.BpfDiv{}:
235      bpf_div(U32.is_zero(v), a, v)
236    case I.BpfOr{}:
237      Some{U32.or(a, v)}
238    case I.BpfAnd{}:
239      Some{U32.and(a, v)}
240    case I.BpfLsh{}:
241      Some{bpf_shl(U32.is_lt(v, 32), a, v)}
242    case I.BpfRsh{}:
243      Some{bpf_shr(U32.is_lt(v, 32), a, v)}
244    case I.BpfMod{}:
245      bpf_mod(U32.is_zero(v), a, v)
246    case I.BpfXor{}:
247      Some{U32.xor(a, v)}
248
249def bpf_test(c: I.BpfCond, +a: U32, +v: U32) -> Bool:
250  match c:
251    case I.BpfJeq{}:
252      U32.is_eq(a, v)
253    case I.BpfJgt{}:
254      U32.is_gt(a, v)
255    case I.BpfJge{}:
256      U32.is_ge(a, v)
257    case I.BpfJset{}:
258      Bool.not(U32.is_zero(U32.and(a, v)))
259
260def bpf_jsel(hit: Bool, jt: U32, jf: U32) -> Nat:
261  match hit:
262    case True{}:
263      U32.to_nat(jt)
264    case False{}:
265      U32.to_nat(jf)
266
267# One instruction
268
269def bpf_exec(op: I.BpfOp, st: BpfState, +inp: BpfInput) -> BpfStep:
270  match op:
271    case I.BpfLdAbs{size, k}:
272      bpf_step.of(bpf_set_a.m(bpf_load(inp, size, k), st))
273    case I.BpfLdInd{size, k}:
274      match st:
275        case BpfState{a, +x, mem}:
276          bpf_step.of(bpf_set_a.m(bpf_load.ind(inp, size, x, k), BpfState{a, x, mem}))
277    case I.BpfLdImm{k}:
278      BpfNext{0n, bpf_set_a(st, k)}
279    case I.BpfLdLen{}:
280      BpfNext{0n, bpf_set_a(st, bpf_len(inp))}
281    case I.BpfLdMem{+k}:
282      bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, bpf_mem.lda(st, k))
283    case I.BpfLdxImm{k}:
284      BpfNext{0n, bpf_set_x(st, k)}
285    case I.BpfLdxMem{+k}:
286      bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, bpf_mem.ldx(st, k))
287    case I.BpfLdxLen{}:
288      BpfNext{0n, bpf_set_x(st, bpf_len(inp))}
289    case I.BpfLdxMsh{k}:
290      bpf_step.of(bpf_set_x.m(bpf_load.msh(inp, k), st))
291    case I.BpfSt{+k}:
292      bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, bpf_mem.st(st, k))
293    case I.BpfStx{+k}:
294      bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, bpf_mem.stx(st, k))
295    case I.BpfAlu{o, src}:
296      match st:
297        case BpfState{+a, +x, mem}:
298          bpf_step.of(bpf_set_a.m(bpf_alu(o, a, bpf_src(src, x)), BpfState{a, x, mem}))
299    case I.BpfNeg{}:
300      BpfNext{0n, bpf_neg(st)}
301    case I.BpfJa{k}:
302      BpfNext{U32.to_nat(k), st}
303    case I.BpfJmp{c, src, jt, jf}:
304      match st:
305        case BpfState{+a, +x, mem}:
306          BpfNext{bpf_jsel(bpf_test(c, a, bpf_src(src, x)), jt, jf), BpfState{a, x, mem}}
307    case I.BpfRet{v}:
308      match v:
309        case I.BpfRetK{k}:
310          BpfStop{k}
311        case I.BpfRetA{}:
312          BpfStop{bpf_get_a(st)}
313    case I.BpfTax{}:
314      BpfNext{0n, bpf_tax(st)}
315    case I.BpfTxa{}:
316      BpfNext{0n, bpf_txa(st)}
317
318# The run: one pass over the instructions, skipping the ones a jump passes
319# over, so every instruction is visited at most once
320
321def bpf_run.go(xs: List<&2, I.BpfOp>, cur: BpfStep, +inp: BpfInput) -> Result<&2, &2, I.BpfError, U32>:
322  match xs:
323    case Nil{}:
324      match cur:
325        case BpfNext{skip, st}:
326          Fail{I.BpfErrFellOff{}}
327        case BpfStop{v}:
328          Done{v}
329        case BpfFault{e}:
330          Fail{e}
331    case Con{op, t}:
332      match cur:
333        case BpfNext{skip, st}:
334          match skip:
335            case 0n:
336              bpf_run.go(t, bpf_exec(op, st, inp), inp)
337            case 1n+s:
338              bpf_run.go(t, BpfNext{s, st}, inp)
339        case BpfStop{v}:
340          Done{v}
341        case BpfFault{e}:
342          Fail{e}
343
344# the program's answer for this input
345def bpf_run(+inp: BpfInput, prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, U32>:
346  bpf_run.go(prog, BpfNext{0n, bpf_init()}, inp)