LAWS.bend

bend-osdev-bpf@0.1.0.0 · 353 lines · 82 definitions

1# Properties, for every input:
2#   * a validated program always answers, whatever the validator's options:
3#     bpf_run gives Done, whatever the input (it never runs past its end or
4#     misuses scratch memory), and
5#     instructions after it are never reached; the same for seccomp filters;
6#   * RET k answers k;
7#   * jumps move forward over exactly the instructions they skip;
8#   * decoding an encoded instruction or program gives it back;
9#   * a stored program longer than the limit is refused, whatever its bytes;
10#   * stacked seccomp filters answer the most restrictive action, the newer
11#     filter's on a tie, and the grouping does not matter.
12#
13# Vectors: the bpf(4) and seccomp(2) examples, one case of each rule, and a
14# witness for each hypothesis.
15import Base
16import bend-osdev-bytes@0.1.0.0/bytes.bend as B
17import bend-osdev-word64@0.1.0.0/word64.bend as W
18import bend-osdev-bpf@0.1.0.0/insn.bend as I
19import bend-osdev-bpf@0.1.0.0/validate.bend as V
20import bend-osdev-bpf@0.1.0.0/bpf.bend as R
21import bend-osdev-bpf@0.1.0.0/seccomp.bend as S
22
23law validated_returns:
24  for +opts: V.BpfValidateOptions
25  for +prog: List<&2, I.BpfOp>
26  for +inp: R.BpfInput
27  for +ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
28  {Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run(inp, prog)) == True{} : Bool}
29
30law validated_ignores_tail:
31  for +opts: V.BpfValidateOptions
32  for +prog: List<&2, I.BpfOp>
33  for +rest: List<&2, I.BpfOp>
34  for +inp: R.BpfInput
35  for +ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
36  {R.bpf_run(inp, List.append(&2, I.BpfOp, prog, rest)) == R.bpf_run(inp, prog) : Result<&2, &2, I.BpfError, U32>}
37
38law ret_k:
39  for k: U32
40  for +inp: R.BpfInput
41  {R.bpf_run(inp, [I.BpfRet{I.BpfRetK{k}}]) == Done{k} : Result<&2, &2, I.BpfError, U32>}
42
43law ja_skips:
44  for k: U32
45  for +skipped: List<&2, I.BpfOp>
46  for +rest: List<&2, I.BpfOp>
47  for +inp: R.BpfInput
48  for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(k) : Nat}
49  {R.bpf_run(inp, Con{I.BpfJa{k}, List.append(&2, I.BpfOp, skipped, rest)}) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}
50
51law jeq_taken_skips:
52  for jt: U32
53  for jf: U32
54  for +skipped: List<&2, I.BpfOp>
55  for +rest: List<&2, I.BpfOp>
56  for +inp: R.BpfInput
57  for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(jt) : Nat}
58  {R.bpf_run(inp, Con{I.BpfJmp{I.BpfJeq{}, I.BpfK{0}, jt, jf}, List.append(&2, I.BpfOp, skipped, rest)}) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}
59
60law jeq_not_taken_skips:
61  for jt: U32
62  for jf: U32
63  for +skipped: List<&2, I.BpfOp>
64  for +rest: List<&2, I.BpfOp>
65  for +inp: R.BpfInput
66  for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(jf) : Nat}
67  {R.bpf_run(inp, Con{I.BpfJmp{I.BpfJeq{}, I.BpfK{1}, jt, jf}, List.append(&2, I.BpfOp, skipped, rest)}) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}
68
69law insn_round_trip:
70  for op: I.BpfOp
71  {I.BpfRaw.decode(I.BpfOp.encode(op)) == Some{op} : Maybe<&2, I.BpfOp>}
72
73law program_round_trip:
74  for +prog: List<&2, I.BpfOp>
75  {I.bpf_decode(I.bpf_encode(prog)) == Done{prog} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
76
77# a stored program with a byte at offset max (so more than max bytes) is
78# refused, whatever its bytes
79law octets_over_limit:
80  for +max: Nat
81  for +order: I.BpfOrder
82  for +o: B.Octets
83  for b: U32
84  for e: {B.Octets.at(o, max) == Some{b} : Maybe<&2, U32>}
85  {I.bpf_of_octets_with(max, order, o) == Fail{I.BpfErrStoredTooLong{max}} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}
86
87law most_restrictive:
88  for a: S.SeccompAction
89  for b: S.SeccompAction
90  {S.SeccompAction.rank(S.seccomp_combine(a, b)) == Nat.min(S.SeccompAction.rank(a), S.SeccompAction.rank(b)) : Nat}
91
92law combine_newer:
93  for +a: S.SeccompAction
94  for +b: S.SeccompAction
95  for e: {Nat.is_le(S.SeccompAction.rank(a), S.SeccompAction.rank(b)) == True{} : Bool}
96  {S.seccomp_combine(a, b) == a : S.SeccompAction}
97
98law combine_older:
99  for +a: S.SeccompAction
100  for +b: S.SeccompAction
101  for e: {Nat.is_lt(S.SeccompAction.rank(b), S.SeccompAction.rank(a)) == True{} : Bool}
102  {S.seccomp_combine(a, b) == b : S.SeccompAction}
103
104law combine_assoc:
105  for a: S.SeccompAction
106  for b: S.SeccompAction
107  for c: S.SeccompAction
108  {S.seccomp_combine(a, S.seccomp_combine(b, c)) == S.seccomp_combine(S.seccomp_combine(a, b), c) : S.SeccompAction}
109
110law action_round_trip:
111  for a: S.SeccompAction
112  {S.SeccompAction.of_u32(S.SeccompAction.to_u32(a)) == S.SeccompAction.clip(a) : S.SeccompAction}
113
114law seccomp_validated_acts:
115  for +opts: V.BpfValidateOptions
116  for +order: I.BpfOrder
117  for +prog: List<&2, I.BpfOp>
118  for +d: S.SeccompData
119  for +ok: {S.seccomp_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
120  {Result.is_done(&2, &2, I.BpfError, S.SeccompAction, S.seccomp_run(order, prog, d)) == True{} : Bool}
121
122# Vectors: the documentation's examples, and one case of each rule
123
124# bpf(4), EXAMPLES: accept only Reverse ARP requests, as the manual writes it
125# with BPF_STMT and BPF_JUMP (0x8035, ETHERTYPE_REVARP; 3, REVARP_REQUEST)
126def rarp() -> List<&2, I.BpfRaw>:
127  [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)]
128
129def rarp_ops() -> List<&2, I.BpfOp>:
130  [I.BpfLdAbs{I.BpfH{}, 12}, I.BpfJmp{I.BpfJeq{}, I.BpfK{32821}, 0, 3}, I.BpfLdAbs{I.BpfH{}, 20}, I.BpfJmp{I.BpfJeq{}, I.BpfK{3}, 0, 1}, I.BpfRet{I.BpfRetK{42}}, I.BpfRet{I.BpfRetK{0}}]
131
132# bpf(4): accept IP packets between 128.3.112.15 and 128.3.112.35
133def hosts() -> List<&2, I.BpfOp>:
134  [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}}]
135
136# bpf(4): accept TCP finger packets (port 79), skipping IP fragments, with
137# the IP header length from BPF_LDX | BPF_MSH
138def finger() -> List<&2, I.BpfOp>:
139  [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}}]
140
141# Ethernet frames: a RARP request, an ARP request, and IPv4 TCP packets
142def pkt_rarp() -> B.Octets:
143  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])
144
145def pkt_arp() -> B.Octets:
146  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])
147
148# from 128.3.112.15 to 128.3.112.35, and from 128.3.112.15 to 10.0.0.1
149def pkt_ab() -> B.Octets:
150  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, 128, 3, 112, 15, 128, 3, 112, 35, 3, 232, 0, 80, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
151
152def pkt_ac() -> B.Octets:
153  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, 128, 3, 112, 15, 10, 0, 0, 1, 3, 232, 0, 80, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])
154
155# to TCP port 79; to port 80; a fragment to port 79; and to port 79 after a
156# 24-byte IP header
157def pkt_finger() -> B.Octets:
158  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])
159
160def pkt_web() -> B.Octets:
161  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])
162
163def pkt_frag() -> B.Octets:
164  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])
165
166def pkt_finger_opts() -> B.Octets:
167  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])
168
169law rarp_prepares:
170  {V.bpf_prepare(V.bpf_maxinsns(), rarp()) == Done{rarp_ops()} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
171
172law rarp_accepts:
173  {R.bpf_run(R.bpf_packet(pkt_rarp()), rarp_ops()) == Done{42} : Result<&2, &2, I.BpfError, U32>}
174
175law rarp_rejects_arp:
176  {R.bpf_run(R.bpf_packet(pkt_arp()), rarp_ops()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
177
178law hosts_accepts:
179  {R.bpf_run(R.bpf_packet(pkt_ab()), hosts()) == Done{4294967295} : Result<&2, &2, I.BpfError, U32>}
180
181law hosts_rejects:
182  {R.bpf_run(R.bpf_packet(pkt_ac()), hosts()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
183
184law finger_accepts:
185  {R.bpf_run(R.bpf_packet(pkt_finger()), finger()) == Done{4294967295} : Result<&2, &2, I.BpfError, U32>}
186
187law finger_accepts_options:
188  {R.bpf_run(R.bpf_packet(pkt_finger_opts()), finger()) == Done{4294967295} : Result<&2, &2, I.BpfError, U32>}
189
190law finger_rejects_port:
191  {R.bpf_run(R.bpf_packet(pkt_web()), finger()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
192
193law finger_rejects_fragment:
194  {R.bpf_run(R.bpf_packet(pkt_frag()), finger()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
195
196# a load past the end of the input answers 0
197law short_packet:
198  {R.bpf_run(R.bpf_packet(B.Octets.of_list([8, 0, 69])), finger()) == Done{0} : Result<&2, &2, I.BpfError, U32>}
199
200# so does a division by X = 0
201law divide_by_zero_x:
202  {R.bpf_run(R.bpf_packet(pkt_arp()), [I.BpfLdImm{7}, I.BpfAlu{I.BpfDiv{}, I.BpfX{}}, I.BpfRet{I.BpfRetK{1}}]) == Done{0} : Result<&2, &2, I.BpfError, U32>}
203
204law length_load:
205  {R.bpf_run(R.bpf_packet(pkt_rarp()), [I.BpfLdLen{}, I.BpfRet{I.BpfRetA{}}]) == Done{42} : Result<&2, &2, I.BpfError, U32>}
206
207# M[15] = 5; X = 3; A = M[15] * X = 15; M[0] = X; X = M[15]; A = -(A - X)
208law scratch_and_alu:
209  {R.bpf_run(R.bpf_packet(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{}}]) == Done{4294967286} : Result<&2, &2, I.BpfError, U32>}
210
211law validate_accepts:
212  {V.bpf_validate(V.bpf_maxinsns(), finger()) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
213
214law validate_empty:
215  {V.bpf_validate(V.bpf_maxinsns(), []) == Fail{I.BpfErrEmpty{}} : Result<&2, &2, I.BpfError, Unit>}
216
217law validate_too_long:
218  {V.bpf_validate(12n, finger()) == Fail{I.BpfErrTooLong{13n}} : Result<&2, &2, I.BpfError, Unit>}
219
220law validate_jump_out:
221  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfJa{1}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrJump{0n}} : Result<&2, &2, I.BpfError, Unit>}
222
223law validate_no_return:
224  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfRet{I.BpfRetA{}}, I.BpfLdImm{1}]) == Fail{I.BpfErrNoReturn{1n}} : Result<&2, &2, I.BpfError, Unit>}
225
226law validate_scratch:
227  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfSt{16}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrScratch{0n}} : Result<&2, &2, I.BpfError, Unit>}
228
229law validate_div_zero:
230  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfAlu{I.BpfMod{}, I.BpfK{0}}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrDivZero{0n}} : Result<&2, &2, I.BpfError, Unit>}
231
232law decode_bad_opcode:
233  {I.bpf_decode([I.bpf_stmt(6, 0), I.bpf_stmt(14, 0)]) == Fail{I.BpfErrBadCode{1n, 14}} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
234
235law program_bytes:
236  {B.Octets.hex(I.bpf_to_octets(I.BpfLittle{}, rarp())) == "280000000c000000150000033580000028000000140000001500000103000000060000002a0000000600000000000000" : String}
237
238law program_bytes_back:
239  {I.bpf_of_octets(I.BpfBig{}, I.bpf_to_octets(I.BpfBig{}, rarp())) == Done{rarp()} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}
240
241# the default limit on stored programs: 8 bytes for each of BPF_MAXINSNS
242# instructions (compared as U32, which holds both)
243law octets_max_default:
244  {U32.from_nat(I.bpf_octets_max()) == U32.mul(8, U32.from_nat(V.bpf_maxinsns())) : U32}
245
246law octets_limit_refuses:
247  {I.bpf_of_octets_with(16n, I.BpfBig{}, B.Octets.zeros(17n)) == Fail{I.BpfErrStoredTooLong{16n}} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}
248
249law octets_limit_accepts:
250  {I.bpf_of_octets_with(16n, I.BpfLittle{}, I.bpf_to_octets(I.BpfLittle{}, [I.bpf_stmt(6, 1), I.bpf_stmt(22, 0)])) == Done{[I.bpf_stmt(6, 1), I.bpf_stmt(22, 0)]} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}
251
252# seccomp(2), EXAMPLES, install_filter(syscall_nr, t_arch, f_errno) with
253# t_arch = AUDIT_ARCH_X86_64, so upper_nr_limit = X32_SYSCALL_BIT - 1: the
254# call syscall_nr fails with f_errno, other calls are allowed, and another
255# architecture or an x32 call (nr above the limit) kills the process
256def seccomp_example(nr: U32, e: U32) -> List<&2, I.BpfOp>:
257  [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{nr}, 0, 1}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompErrno{e})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompAllow{})}}, I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompKillProcess{})}}]
258
259def sc_call(nr: U32, arch: U32) -> S.SeccompData:
260  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()}
261
262# ERRNO(e) for system call nr, ALLOW for the others
263def deny(nr: U32, e: U32) -> List<&2, I.BpfOp>:
264  [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{})}}]
265
266law seccomp_example_valid:
267  {S.seccomp_validate(V.bpf_maxinsns(), seccomp_example(59, 99)) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
268
269law seccomp_example_errno:
270  {S.seccomp_run(S.seccomp_order(), seccomp_example(59, 99), sc_call(59, S.seccomp_arch_x86_64())) == Done{S.SeccompErrno{99}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
271
272law seccomp_example_allow:
273  {S.seccomp_run(S.seccomp_order(), seccomp_example(59, 99), sc_call(1, S.seccomp_arch_x86_64())) == Done{S.SeccompAllow{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
274
275law seccomp_example_other_arch:
276  {S.seccomp_run(S.seccomp_order(), seccomp_example(59, 99), sc_call(59, S.seccomp_arch_i386())) == Done{S.SeccompKillProcess{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
277
278law seccomp_example_x32:
279  {S.seccomp_run(S.seccomp_order(), seccomp_example(59, 99), sc_call(1073741883, S.seccomp_arch_x86_64())) == Done{S.SeccompKillProcess{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
280
281law seccomp_rejects_byte_load:
282  {S.seccomp_validate(V.bpf_maxinsns(), finger()) == Fail{I.BpfErrSeccompLoad{0n}} : Result<&2, &2, I.BpfError, Unit>}
283
284law seccomp_rejects_unaligned:
285  {S.seccomp_validate(V.bpf_maxinsns(), [I.BpfLdAbs{I.BpfW{}, 6}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrSeccompLoad{0n}} : Result<&2, &2, I.BpfError, Unit>}
286
287# two filters with the same action: the newer one wins, with its data
288law stack_newest_on_tie:
289  {S.seccomp_eval([deny(39, 1), deny(39, 2)], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64())) == Done{S.SeccompErrno{1}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
290
291law stack_most_restrictive:
292  {S.seccomp_eval([deny(39, 1), [I.BpfRet{I.BpfRetK{S.SeccompAction.to_u32(S.SeccompTrap{5})}}], deny(110, 3)], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64())) == Done{S.SeccompTrap{5}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
293
294law stack_empty_allows:
295  {S.seccomp_eval([], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64())) == Done{S.SeccompAllow{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
296
297law unknown_action_kills:
298  {S.SeccompAction.of_u32(65536) == S.SeccompKillProcess{} : S.SeccompAction}
299
300law install_path_limit:
301  {S.seccomp_install(S.SeccompLimits{4096n, 19n}, [deny(39, 1), deny(39, 2)], I.bpf_encode(deny(110, 3))) == Fail{I.BpfErrPathTooLong{20n}} : Result<&2, &2, I.BpfError, List<&2, List<&2, I.BpfOp>>>}
302
303law install_pushes:
304  {S.seccomp_install(S.seccomp_limits(), [deny(39, 1)], I.bpf_encode(deny(110, 3))) == Done{[deny(110, 3), deny(39, 1)]} : Result<&2, &2, I.BpfError, List<&2, List<&2, I.BpfOp>>>}
305
306law seccomp_rejects_mod:
307  {S.seccomp_validate(V.bpf_maxinsns(), [I.BpfLdImm{7}, I.BpfAlu{I.BpfMod{}, I.BpfK{3}}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrSeccompInsn{1n}} : Result<&2, &2, I.BpfError, Unit>}
308
309# the page's runs: ./a.out 1 0xC000003E 99 makes write (1) fail, and
310# ./a.out 295 0xC000003E 99 leaves the calls whoami makes alone
311law seccomp_example_write:
312  {S.seccomp_run(S.seccomp_order(), seccomp_example(1, 99), sc_call(1, S.seccomp_arch_x86_64())) == Done{S.SeccompErrno{99}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
313
314law seccomp_example_preadv:
315  {S.seccomp_run(S.seccomp_order(), seccomp_example(295, 99), sc_call(1, S.seccomp_arch_x86_64())) == Done{S.SeccompAllow{}} : Result<&2, &2, I.BpfError, S.SeccompAction>}
316
317# scratch memory read before it is written: refused by default, on every
318# path (here the jump past the store), and allowed by the permissive options
319law validate_mem_init:
320  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrMemInit{0n}} : Result<&2, &2, I.BpfError, Unit>}
321
322law validate_mem_init_path:
323  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{1}, I.BpfJmp{I.BpfJeq{}, I.BpfK{1}, 1, 0}, I.BpfSt{2}, I.BpfLdMem{2}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrMemInit{3n}} : Result<&2, &2, I.BpfError, Unit>}
324
325law validate_mem_init_written:
326  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{1}, I.BpfSt{2}, I.BpfJmp{I.BpfJeq{}, I.BpfK{1}, 1, 0}, I.BpfSt{3}, I.BpfLdMem{2}, I.BpfRet{I.BpfRetA{}}]) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
327
328# code after a jump is reached only by jumps to it; code after a return
329# counts as reached from the return, as Linux counts it
330law validate_mem_after_jump:
331  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{0}, I.BpfSt{0}, I.BpfJa{1}, I.BpfLdMem{1}, I.BpfRet{I.BpfRetA{}}]) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
332
333law validate_mem_after_return:
334  {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{0}, I.BpfRet{I.BpfRetA{}}, I.BpfLdMem{1}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrMemInit{2n}} : Result<&2, &2, I.BpfError, Unit>}
335
336law validate_permissive:
337  {V.bpf_validate_with(V.BpfValidateOptions.permissive(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}]) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
338
339# Witnesses: each hypothesis of a law above holds for some input (the
340# validation hypotheses: validate_accepts, validate_permissive and
341# seccomp_example_valid; octets_over_limit: witness_octets_over)
342
343law witness_skip_length:
344  {List.length(&2, I.BpfOp, [I.BpfTax{}, I.BpfTxa{}, I.BpfNeg{}]) == U32.to_nat(3) : Nat}
345
346law witness_octets_over:
347  {B.Octets.at(B.Octets.zeros(9n), 8n) == Some{0} : Maybe<&2, U32>}
348
349law witness_rank_le:
350  {Nat.is_le(S.SeccompAction.rank(S.SeccompErrno{1}), S.SeccompAction.rank(S.SeccompErrno{2})) == True{} : Bool}
351
352law witness_rank_lt:
353  {Nat.is_lt(S.SeccompAction.rank(S.SeccompKillProcess{}), S.SeccompAction.rank(S.SeccompAllow{})) == True{} : Bool}