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.
20	import Base
21	import ./insn.bend as I
22	
23	# BPF_MAXINSNS: the usual instruction limit
24	def 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
29	type 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
33	def 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
37	def BpfValidateOptions.permissive() -> BpfValidateOptions:
38	  BpfValidateOptions{bpf_maxinsns(), False{}}
39	
40	def 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	
47	def 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
55	def 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	
58	def 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	
65	def 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	
74	def 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	
77	def 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
81	def 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)
104	def 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
113	def 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)
129	def 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	
136	def bpf_count(xs: List<&2, I.BpfOp>) -> Nat:
137	  bpf_count.go(xs, 0n)
138	
139	def 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	
147	def 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	
154	def 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)
158	def 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	
169	def bpf_mem.meet(ahead: List<&2, U32>, n: Nat, +m: U32) -> List<&2, U32>:
170	  bpf_mem.meet.go(ahead, n, m, Nil{})
171	
172	type BpfInitStep is Data:
173	  BpfInitStep{ok: Result<&2, &2, I.BpfError, Unit>, fall: U32, ahead: List<&2, U32>}
174	
175	def 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
179	def 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	
196	def bpf_mem.head(ahead: List<&2, U32>) -> U32:
197	  match ahead:
198	    case Nil{}:
199	      65535
200	    case Con{h, t}:
201	      h
202	
203	def 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	
210	def 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
226	def 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	
233	def 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	
243	def 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	
250	def 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
259	def 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
266	def bpf_validate(limit: Nat, +prog: List<&2, I.BpfOp>) -> Result<&2, &2, I.BpfError, Unit>:
267	  bpf_validate_with(BpfValidateOptions{limit, True{}}, prog)
268	
269	def 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	
276	def 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
284	def 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
288	def 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)