check.bend

bend-osdev-bpf@0.1.0.0 · 197 lines · 30 definitions

1import Base
2import bend-osdev-bytes@0.1.0.0/bytes.bend as B
3import bend-osdev-word64@0.1.0.0/word64.bend as W
4import bend-osdev-bpf@0.1.0.0/insn.bend as I
5import bend-osdev-bpf@0.1.0.0/validate.bend as V
6import bend-osdev-bpf@0.1.0.0/bpf.bend as R
7import bend-osdev-bpf@0.1.0.0/seccomp.bend as S
8
9def show_run(r: Result<&2, &2, I.BpfError, U32>) -> String:
10  match r:
11    case Fail{e}:
12      "error: " ++ I.BpfError.show(e)
13    case Done{v}:
14      U32.show(v)
15
16def show_ok(r: Result<&2, &2, I.BpfError, Unit>) -> String:
17  match r:
18    case Fail{e}:
19      "error: " ++ I.BpfError.show(e)
20    case Done{u}:
21      "ok"
22
23def show_act(r: Result<&2, &2, I.BpfError, S.SeccompAction>) -> String:
24  match r:
25    case Fail{e}:
26      "error: " ++ I.BpfError.show(e)
27    case Done{a}:
28      S.SeccompAction.show(a)
29
30# bpf(4), EXAMPLES: accept only Reverse ARP requests, as BPF_STMT and
31# BPF_JUMP lines (0x8035 = 32821, ETHERTYPE_REVARP; 3, REVARP_REQUEST)
32def rarp() -> List<&2, I.BpfRaw>:
33  [I.bpf_stmt(40, 12), I.bpf_jump(21, 32821, 0, 3), I.bpf_stmt(40, 20), I.bpf_jump(21, 3, 0, 1), I.bpf_stmt(6, 42), I.bpf_stmt(6, 0)]
34
35def run_raw.go(o: B.Octets, p: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> Result<&2, &2, I.BpfError, U32>:
36  match p:
37    case Fail{e}:
38      Fail{e}
39    case Done{ops}:
40      R.bpf_run(R.bpf_packet(o), ops)
41
42def run_raw(o: B.Octets, rs: List<&2, I.BpfRaw>) -> Result<&2, &2, I.BpfError, U32>:
43  run_raw.go(o, V.bpf_prepare(V.bpf_maxinsns(), rs))
44
45# bpf(4): accept IP packets between 128.3.112.15 and 128.3.112.35
46def hosts() -> List<&2, I.BpfOp>:
47  [I.BpfLdAbs{I.BpfH{}, 12}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2048}, 0, 8}, I.BpfLdAbs{I.BpfW{}, 26}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2147708943}, 0, 2}, I.BpfLdAbs{I.BpfW{}, 30}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2147708963}, 3, 4}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2147708963}, 0, 3}, I.BpfLdAbs{I.BpfW{}, 30}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2147708943}, 0, 1}, I.BpfRet{I.BpfRetK{4294967295}}, I.BpfRet{I.BpfRetK{0}}]
48
49# bpf(4): accept TCP finger packets (port 79), skipping IP fragments
50def finger() -> List<&2, I.BpfOp>:
51  [I.BpfLdAbs{I.BpfH{}, 12}, I.BpfJmp{I.BpfJeq{}, I.BpfK{2048}, 0, 10}, I.BpfLdAbs{I.BpfB{}, 23}, I.BpfJmp{I.BpfJeq{}, I.BpfK{6}, 0, 8}, I.BpfLdAbs{I.BpfH{}, 20}, I.BpfJmp{I.BpfJset{}, I.BpfK{8191}, 6, 0}, I.BpfLdxMsh{14}, I.BpfLdInd{I.BpfH{}, 14}, I.BpfJmp{I.BpfJeq{}, I.BpfK{79}, 2, 0}, I.BpfLdInd{I.BpfH{}, 16}, I.BpfJmp{I.BpfJeq{}, I.BpfK{79}, 0, 1}, I.BpfRet{I.BpfRetK{4294967295}}, I.BpfRet{I.BpfRetK{0}}]
52
53def pkt_rarp() -> B.Octets:
54  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 128, 53, 0, 1, 8, 0, 6, 4, 0, 3, 2, 0, 0, 0, 0, 1, 10, 0, 0, 1, 0, 0, 0, 0, 0, 0, 10, 0, 0, 2])
55
56def pkt_arp() -> B.Octets:
57  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 6, 0, 1, 8, 0, 6, 4, 0, 1, 2, 0, 0, 0, 0, 1, 10, 0, 0, 1, 0, 0, 0, 0, 0, 0, 10, 0, 0, 2])
58
59def pkt_ip(src: List<&2, U32>, dst: List<&2, U32>) -> B.Octets:
60  B.Octets.concat([B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 69, 0, 0, 40, 0, 0, 64, 0, 64, 6, 0, 0]), B.Octets.of_list(src), B.Octets.of_list(dst), B.Octets.of_list([3, 232, 0, 80]), B.Octets.zeros(16n)])
61
62def pkt_finger() -> B.Octets:
63  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 69, 0, 0, 40, 0, 0, 64, 0, 64, 6, 0, 0, 10, 0, 0, 1, 128, 3, 112, 15, 3, 255, 0, 79, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
64
65def pkt_web() -> B.Octets:
66  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 69, 0, 0, 40, 0, 0, 64, 0, 64, 6, 0, 0, 10, 0, 0, 1, 128, 3, 112, 15, 3, 255, 0, 80, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
67
68def pkt_frag() -> B.Octets:
69  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 69, 0, 0, 40, 0, 0, 32, 1, 64, 6, 0, 0, 10, 0, 0, 1, 128, 3, 112, 15, 3, 255, 0, 79, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
70
71def pkt_finger_opts() -> B.Octets:
72  B.Octets.of_list([255, 255, 255, 255, 255, 255, 2, 0, 0, 0, 0, 1, 8, 0, 70, 0, 0, 40, 0, 0, 64, 0, 64, 6, 0, 0, 10, 0, 0, 1, 128, 3, 112, 15, 1, 2, 3, 4, 0, 79, 3, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
73
74def pkt_run(o: B.Octets, prog: List<&2, I.BpfOp>) -> String:
75  show_run(R.bpf_run(R.bpf_packet(o), prog))
76
77# seccomp(2), EXAMPLES: install_filter(59, AUDIT_ARCH_X86_64, 99): execve
78# (59) fails with errno 99, other calls are allowed, and another
79# architecture or an x32 call kills the process
80def example() -> List<&2, I.BpfOp>:
81  [I.BpfLdAbs{I.BpfW{}, 4}, I.BpfJmp{I.BpfJeq{}, I.BpfK{S.seccomp_arch_x86_64()}, 0, 5}, I.BpfLdAbs{I.BpfW{}, 0}, I.BpfJmp{I.BpfJgt{}, I.BpfK{U32.sub(S.seccomp_x32_syscall_bit(), 1)}, 3, 0}, I.BpfJmp{I.BpfJeq{}, I.BpfK{59}, 0, 1}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompErrno{99})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompAllow{})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompKillProcess{})}}]
82
83def sc_call(nr: U32, arch: U32) -> S.SeccompData:
84  S.SeccompData{nr, arch, W.W64.zero(), W.W64.zero(), W.W64.zero(), W.W64.zero(), W.W64.zero(), W.W64.zero(), W.W64.zero()}
85
86def sc(prog: List<&2, I.BpfOp>, d: S.SeccompData) -> String:
87  show_act(S.seccomp_run(S.seccomp_order(), prog, d))
88
89def ret_only(a: S.SeccompAction) -> List<&2, I.BpfOp>:
90  [I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(a)}}]
91
92# a filter that answers ERRNO(e) for system call nr and ALLOW otherwise
93def deny(nr: U32, e: U32) -> List<&2, I.BpfOp>:
94  [I.BpfLdAbs{I.BpfW{}, 0}, I.BpfJmp{I.BpfJeq{}, I.BpfK{nr}, 0, 1}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompErrno{e})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompAllow{})}}]
95
96# A full-size program, as a regression test for long inputs: 4096
97# instructions (BPF_MAXINSNS), stored as Octets, read back, prepared and run
98# on 64 KB of pseudo-random bytes (a linear congruential generator). Block j
99# of eight: ld [4j mod 65532]; add #j; st M[j mod 16]; ldx M[j mod 16];
100# ldx #(7j mod 65000); ldb [x + 3]; jeq #j, 0, 0; ja 0 (ret a in the last).
101def big.last(last: Bool) -> I.BpfRaw:
102  match last:
103    case True{}:
104      I.bpf_stmt(22, 0)
105    case False{}:
106      I.bpf_stmt(5, 0)
107
108def big.block(+j: U32, last: Bool, acc: List<&2, I.BpfRaw>) -> List<&2, I.BpfRaw>:
109  +m = U32.mod(j, 16)
110  Con{I.bpf_stmt(32, U32.mod(U32.mul(4, j), 65532)), Con{I.bpf_stmt(4, j), Con{I.bpf_stmt(2, m), Con{I.bpf_stmt(97, m), Con{I.bpf_stmt(1, U32.mod(U32.mul(j, 7), 65000)), Con{I.bpf_stmt(80, 3), Con{I.bpf_jump(21, j, 0, 0), Con{big.last(last), acc}}}}}}}}
111
112# blocks 0 to j, the last ending in ret a (top is the last block's j)
113def big.prog(n: Nat, +j: U32, +top: U32, acc: List<&2, I.BpfRaw>) -> List<&2, I.BpfRaw>:
114  match n:
115    case 0n:
116      acc
117    case 1n+p:
118      big.prog(p, U32.sub(j, 1), top, big.block(j, U32.is_eq(j, top), acc))
119
120def big.packet(n: Nat, +s: U32, acc: List<&2, U32>) -> List<&2, U32>:
121  match n:
122    case 0n:
123      acc
124    case 1n+p:
125      +s2 = U32.add(U32.mul(s, 1103515245), 12345)
126      big.packet(p, s2, Con{U32.and(U32.shrn(s2, 16n), 255), acc})
127
128def big.run(r: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, pk: B.Octets) -> String:
129  match r:
130    case Done{ops}:
131      show_run(R.bpf_run(R.bpf_packet(pk), ops))
132    case Fail{e}:
133      "error: " ++ I.BpfError.show(e)
134
135def big.prep(r: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> Result<&2, &2, I.BpfError, Unit>:
136  match r:
137    case Done{ops}:
138      Done{Unit{}}
139    case Fail{e}:
140      Fail{e}
141
142def big.read(r: Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>, pk: B.Octets) -> String:
143  match r:
144    case Done{raws}:
145      big.run(V.bpf_prepare(V.bpf_maxinsns(), raws), pk)
146    case Fail{e}:
147      "error: " ++ I.BpfError.show(e)
148
149# Untrusted input of 32768 instructions (256 KB): refused by bpf_of_octets
150# at its default limit (8 * BPF_MAXINSNS bytes) before the rest is read, and,
151# read with a higher limit, decoded and refused by validation as too long
152def huge.read(r: Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>) -> String:
153  match r:
154    case Done{raws}:
155      show_ok(big.prep(V.bpf_prepare(V.bpf_maxinsns(), raws)))
156    case Fail{e}:
157      "error: " ++ I.BpfError.show(e)
158
159def main() -> IO(Unit):
160  +big = I.bpf_to_octets(I.BpfBig{}, big.prog(512n, 511, 511, Nil{}))
161  +huge = I.bpf_to_octets(I.BpfLittle{}, big.prog(4096n, 4095, 4095, Nil{}))
162  do IO<Unit>:
163    IO.print("rarp " ++ show_run(run_raw(pkt_rarp(), rarp())) ++ " " ++ show_run(run_raw(pkt_arp(), rarp())))
164    IO.print("hosts " ++ pkt_run(pkt_ip([128, 3, 112, 15], [128, 3, 112, 35]), hosts()) ++ " " ++ pkt_run(pkt_ip([128, 3, 112, 35], [128, 3, 112, 15]), hosts()) ++ " " ++ pkt_run(pkt_ip([128, 3, 112, 15], [10, 0, 0, 1]), hosts()) ++ " " ++ pkt_run(pkt_arp(), hosts()))
165    IO.print("finger " ++ pkt_run(pkt_finger(), finger()) ++ " " ++ pkt_run(pkt_web(), finger()) ++ " " ++ pkt_run(pkt_frag(), finger()) ++ " " ++ pkt_run(pkt_finger_opts(), finger()))
166    IO.print("short " ++ pkt_run(B.Octets.of_list([1, 2, 3]), finger()))
167    IO.print("len " ++ pkt_run(pkt_rarp(), [I.BpfLdLen{}, I.BpfRet{I.BpfRetA{}}]))
168    IO.print("div0 " ++ pkt_run(pkt_rarp(), [I.BpfLdImm{7}, I.BpfAlu{I.BpfDiv{}, I.BpfX{}}, I.BpfRet{I.BpfRetK{1}}]))
169    IO.print("mem " ++ pkt_run(pkt_rarp(), [I.BpfLdImm{5}, I.BpfSt{15}, I.BpfLdxImm{3}, I.BpfLdMem{15}, I.BpfAlu{I.BpfMul{}, I.BpfX{}}, I.BpfStx{0}, I.BpfLdxMem{15}, I.BpfAlu{I.BpfSub{}, I.BpfX{}}, I.BpfNeg{}, I.BpfRet{I.BpfRetA{}}]))
170    IO.print("bytes " ++ B.Octets.hex(I.bpf_to_octets(I.BpfLittle{}, rarp())))
171    IO.print("validate " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), finger())) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [])) ++ ", " ++ show_ok(V.bpf_validate(1n, finger())) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfJa{1}, I.BpfRet{I.BpfRetA{}}])) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{1}])) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfSt{16}, I.BpfRet{I.BpfRetA{}}])) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfAlu{I.BpfMod{}, I.BpfK{0}}, I.BpfRet{I.BpfRetA{}}])))
172    IO.print("mem init " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}])) ++ ", " ++ show_ok(V.bpf_validate_with(V.BpfValidateOptions.permissive(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}])))
173    IO.print("decode " ++ show_run(run_raw(pkt_rarp(), [I.bpf_stmt(14, 0)])))
174    IO.print("seccomp " ++ sc(example(), sc_call(59, S.seccomp_arch_x86_64())) ++ " " ++ sc(example(), sc_call(1, S.seccomp_arch_x86_64())) ++ " " ++ sc(example(), sc_call(59, S.seccomp_arch_i386())) ++ " " ++ sc(example(), sc_call(1073741883, S.seccomp_arch_x86_64())))
175    IO.print("seccomp validate " ++ show_ok(S.seccomp_validate(V.bpf_maxinsns(), example())) ++ ", " ++ show_ok(S.seccomp_validate(V.bpf_maxinsns(), finger())) ++ ", " ++ show_ok(S.seccomp_validate(V.bpf_maxinsns(), [I.BpfLdAbs{I.BpfW{}, 6}, I.BpfRet{I.BpfRetA{}}])))
176    IO.print("stack " ++ show_act(S.seccomp_eval([deny(39, 1), deny(39, 2), deny(110, 3)], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64()))) ++ " " ++ show_act(S.seccomp_eval([deny(39, 1), ret_only(S.SeccompTrap{5}), deny(110, 3)], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64()))) ++ " " ++ show_act(S.seccomp_eval([deny(39, 1), deny(110, 3)], S.seccomp_order(), sc_call(110, S.seccomp_arch_x86_64()))) ++ " " ++ show_act(S.seccomp_eval([], S.seccomp_order(), sc_call(110, S.seccomp_arch_x86_64()))))
177    IO.print("action " ++ S.SeccompAction.show(S.SeccompAction.of_u32(196613)) ++ " " ++ S.SeccompAction.show(S.SeccompAction.of_u32(65536)) ++ " " ++ S.SeccompAction.show(S.SeccompAction.of_u32(0)) ++ " " ++ U32.show(S.SeccompAction.to_u32(S.SeccompErrno{65549})))
178    IO.print("big " ++ Nat.show(B.Octets.len(big)) ++ " bytes, answer " ++ big.read(I.bpf_of_octets(I.BpfBig{}, big), B.Octets.of_list(big.packet(65536n, 7, Nil{}))))
179    IO.print("huge " ++ Nat.show(B.Octets.len(huge)) ++ " bytes: " ++ huge.read(I.bpf_of_octets(I.BpfLittle{}, huge)) ++ "; with a limit of 1 MB: " ++ huge.read(I.bpf_of_octets_with(1048576n, I.BpfLittle{}, huge)))
180
181#|rarp 42 0
182#|hosts 4294967295 4294967295 0 0
183#|finger 4294967295 0 0 4294967295
184#|short 0
185#|len 42
186#|div0 0
187#|mem 4294967286
188#|bytes 280000000c000000150000033580000028000000140000001500000103000000060000002a0000000600000000000000
189#|validate ok, error: empty program, error: program too long: 13, error: jump out of range at 0, error: no return after 0, error: scratch index out of range at 0, error: division by constant zero at 0
190#|mem init error: scratch read before write at 0, ok
191#|decode error: bad opcode 14 at 0
192#|seccomp ERRNO(99) ALLOW KILL_PROCESS KILL_PROCESS
193#|seccomp validate ok, error: load not allowed in seccomp at 0, error: load not allowed in seccomp at 0
194#|stack ERRNO(1) TRAP(5) ERRNO(3) ALLOW
195#|action TRAP(5) KILL_PROCESS KILL_THREAD 327693
196#|big 32768 bytes, answer 180
197#|huge 262144 bytes: error: stored program over 32768 bytes; with a limit of 1 MB: error: program too long: 32768