bend-osdev-bpf Releases (1): 0.1.0.0 0x9fae2d11be141cc220d6a37e498b4020 indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-bpf@0.1.0.0 Definitions (317, 1 to 100 shown): LAWS.validated_returns (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validated_returns) law validated_returns: for +opts: V.BpfValidateOptions for +prog: List<&2, I.BpfOp> for +inp: R.BpfInput for +ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>} {Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run(inp, prog)) == True{} : Bool} LAWS.validated_ignores_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validated_ignores_tail) law validated_ignores_tail: for +opts: V.BpfValidateOptions for +prog: List<&2, I.BpfOp> for +rest: List<&2, I.BpfOp> for +inp: R.BpfInput for +ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>} {R.bpf_run(inp, List.append(&2, I.BpfOp, prog, rest)) == R.bpf_run(inp, prog) : Result<&2, &2, I.BpfError, U32>} LAWS.ret_k (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=ret_k) law ret_k: for k: U32 for +inp: R.BpfInput {R.bpf_run(inp, [I.BpfRet{I.BpfRetK{k}}]) == Done{k} : Result<&2, &2, I.BpfError, U32>} LAWS.ja_skips (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=ja_skips) law ja_skips: for k: U32 for +skipped: List<&2, I.BpfOp> for +rest: List<&2, I.BpfOp> for +inp: R.BpfInput for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(k) : Nat} {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>} LAWS.jeq_taken_skips (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=jeq_taken_skips) law jeq_taken_skips: for jt: U32 for jf: U32 for +skipped: List<&2, I.BpfOp> for +rest: List<&2, I.BpfOp> for +inp: R.BpfInput for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(jt) : Nat} {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>} LAWS.jeq_not_taken_skips (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=jeq_not_taken_skips) law jeq_not_taken_skips: for jt: U32 for jf: U32 for +skipped: List<&2, I.BpfOp> for +rest: List<&2, I.BpfOp> for +inp: R.BpfInput for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(jf) : Nat} {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>} LAWS.insn_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=insn_round_trip) law insn_round_trip: for op: I.BpfOp {I.BpfRaw.decode(I.BpfOp.encode(op)) == Some{op} : Maybe<&2, I.BpfOp>} LAWS.program_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=program_round_trip) law program_round_trip: for +prog: List<&2, I.BpfOp> {I.bpf_decode(I.bpf_encode(prog)) == Done{prog} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>} LAWS.octets_over_limit (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=octets_over_limit) # a stored program with a byte at offset max (so more than max bytes) is # refused, whatever its bytes law octets_over_limit: for +max: Nat for +order: I.BpfOrder for +o: B.Octets for b: U32 for e: {B.Octets.at(o, max) == Some{b} : Maybe<&2, U32>} {I.bpf_of_octets_with(max, order, o) == Fail{I.BpfErrStoredTooLong{max}} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>} LAWS.most_restrictive (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=most_restrictive) law most_restrictive: for a: S.SeccompAction for b: S.SeccompAction {S.SeccompAction.rank(S.seccomp_combine(a, b)) == Nat.min(S.SeccompAction.rank(a), S.SeccompAction.rank(b)) : Nat} LAWS.combine_newer (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=combine_newer) law combine_newer: for +a: S.SeccompAction for +b: S.SeccompAction for e: {Nat.is_le(S.SeccompAction.rank(a), S.SeccompAction.rank(b)) == True{} : Bool} {S.seccomp_combine(a, b) == a : S.SeccompAction} LAWS.combine_older (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=combine_older) law combine_older: for +a: S.SeccompAction for +b: S.SeccompAction for e: {Nat.is_lt(S.SeccompAction.rank(b), S.SeccompAction.rank(a)) == True{} : Bool} {S.seccomp_combine(a, b) == b : S.SeccompAction} LAWS.combine_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=combine_assoc) law combine_assoc: for a: S.SeccompAction for b: S.SeccompAction for c: S.SeccompAction {S.seccomp_combine(a, S.seccomp_combine(b, c)) == S.seccomp_combine(S.seccomp_combine(a, b), c) : S.SeccompAction} LAWS.action_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=action_round_trip) law action_round_trip: for a: S.SeccompAction {S.SeccompAction.of_u32(S.SeccompAction.to_u32(a)) == S.SeccompAction.clip(a) : S.SeccompAction} LAWS.seccomp_validated_acts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_validated_acts) law seccomp_validated_acts: for +opts: V.BpfValidateOptions for +order: I.BpfOrder for +prog: List<&2, I.BpfOp> for +d: S.SeccompData for +ok: {S.seccomp_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>} {Result.is_done(&2, &2, I.BpfError, S.SeccompAction, S.seccomp_run(order, prog, d)) == True{} : Bool} LAWS.rarp (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=rarp) # bpf(4), EXAMPLES: accept only Reverse ARP requests, as the manual writes it # with BPF_STMT and BPF_JUMP (0x8035, ETHERTYPE_REVARP; 3, REVARP_REQUEST) def rarp() -> List<&2, I.BpfRaw>: LAWS.rarp_ops (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=rarp_ops) def rarp_ops() -> List<&2, I.BpfOp>: LAWS.hosts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=hosts) # bpf(4): accept IP packets between 128.3.112.15 and 128.3.112.35 def hosts() -> List<&2, I.BpfOp>: LAWS.finger (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=finger) # bpf(4): accept TCP finger packets (port 79), skipping IP fragments, with # the IP header length from BPF_LDX | BPF_MSH def finger() -> List<&2, I.BpfOp>: LAWS.pkt_rarp (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=pkt_rarp) # Ethernet frames: a RARP request, an ARP request, and IPv4 TCP packets def pkt_rarp() -> B.Octets: LAWS.pkt_arp (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=pkt_arp) def pkt_arp() -> B.Octets: LAWS.pkt_ab (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=pkt_ab) # from 128.3.112.15 to 128.3.112.35, and from 128.3.112.15 to 10.0.0.1 def pkt_ab() -> B.Octets: LAWS.pkt_ac (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=pkt_ac) def pkt_ac() -> B.Octets: LAWS.pkt_finger (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=pkt_finger) # to TCP port 79; to port 80; a fragment to port 79; and to port 79 after a # 24-byte IP header def pkt_finger() -> B.Octets: LAWS.pkt_web (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=pkt_web) def pkt_web() -> B.Octets: LAWS.pkt_frag (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=pkt_frag) def pkt_frag() -> B.Octets: LAWS.pkt_finger_opts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=pkt_finger_opts) def pkt_finger_opts() -> B.Octets: LAWS.rarp_prepares (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=rarp_prepares) law rarp_prepares: {V.bpf_prepare(V.bpf_maxinsns(), rarp()) == Done{rarp_ops()} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>} LAWS.rarp_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=rarp_accepts) law rarp_accepts: {R.bpf_run(R.bpf_packet(pkt_rarp()), rarp_ops()) == Done{42} : Result<&2, &2, I.BpfError, U32>} LAWS.rarp_rejects_arp (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=rarp_rejects_arp) law rarp_rejects_arp: {R.bpf_run(R.bpf_packet(pkt_arp()), rarp_ops()) == Done{0} : Result<&2, &2, I.BpfError, U32>} LAWS.hosts_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=hosts_accepts) law hosts_accepts: {R.bpf_run(R.bpf_packet(pkt_ab()), hosts()) == Done{4294967295} : Result<&2, &2, I.BpfError, U32>} LAWS.hosts_rejects (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=hosts_rejects) law hosts_rejects: {R.bpf_run(R.bpf_packet(pkt_ac()), hosts()) == Done{0} : Result<&2, &2, I.BpfError, U32>} LAWS.finger_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=finger_accepts) law finger_accepts: {R.bpf_run(R.bpf_packet(pkt_finger()), finger()) == Done{4294967295} : Result<&2, &2, I.BpfError, U32>} LAWS.finger_accepts_options (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=finger_accepts_options) law finger_accepts_options: {R.bpf_run(R.bpf_packet(pkt_finger_opts()), finger()) == Done{4294967295} : Result<&2, &2, I.BpfError, U32>} LAWS.finger_rejects_port (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=finger_rejects_port) law finger_rejects_port: {R.bpf_run(R.bpf_packet(pkt_web()), finger()) == Done{0} : Result<&2, &2, I.BpfError, U32>} LAWS.finger_rejects_fragment (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=finger_rejects_fragment) law finger_rejects_fragment: {R.bpf_run(R.bpf_packet(pkt_frag()), finger()) == Done{0} : Result<&2, &2, I.BpfError, U32>} LAWS.short_packet (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=short_packet) # a load past the end of the input answers 0 law short_packet: {R.bpf_run(R.bpf_packet(B.Octets.of_list([8, 0, 69])), finger()) == Done{0} : Result<&2, &2, I.BpfError, U32>} LAWS.divide_by_zero_x (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=divide_by_zero_x) # so does a division by X = 0 law divide_by_zero_x: {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>} LAWS.length_load (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=length_load) law length_load: {R.bpf_run(R.bpf_packet(pkt_rarp()), [I.BpfLdLen{}, I.BpfRet{I.BpfRetA{}}]) == Done{42} : Result<&2, &2, I.BpfError, U32>} LAWS.scratch_and_alu (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=scratch_and_alu) # M[15] = 5; X = 3; A = M[15] * X = 15; M[0] = X; X = M[15]; A = -(A - X) law scratch_and_alu: {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>} LAWS.validate_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_accepts) law validate_accepts: {V.bpf_validate(V.bpf_maxinsns(), finger()) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>} LAWS.validate_empty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_empty) law validate_empty: {V.bpf_validate(V.bpf_maxinsns(), []) == Fail{I.BpfErrEmpty{}} : Result<&2, &2, I.BpfError, Unit>} LAWS.validate_too_long (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_too_long) law validate_too_long: {V.bpf_validate(12n, finger()) == Fail{I.BpfErrTooLong{13n}} : Result<&2, &2, I.BpfError, Unit>} LAWS.validate_jump_out (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_jump_out) law validate_jump_out: {V.bpf_validate(V.bpf_maxinsns(), [I.BpfJa{1}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrJump{0n}} : Result<&2, &2, I.BpfError, Unit>} LAWS.validate_no_return (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_no_return) law validate_no_return: {V.bpf_validate(V.bpf_maxinsns(), [I.BpfRet{I.BpfRetA{}}, I.BpfLdImm{1}]) == Fail{I.BpfErrNoReturn{1n}} : Result<&2, &2, I.BpfError, Unit>} LAWS.validate_scratch (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_scratch) law validate_scratch: {V.bpf_validate(V.bpf_maxinsns(), [I.BpfSt{16}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrScratch{0n}} : Result<&2, &2, I.BpfError, Unit>} LAWS.validate_div_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_div_zero) law validate_div_zero: {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>} LAWS.decode_bad_opcode (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=decode_bad_opcode) law decode_bad_opcode: {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>>} LAWS.program_bytes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=program_bytes) law program_bytes: {B.Octets.hex(I.bpf_to_octets(I.BpfLittle{}, rarp())) == "280000000c000000150000033580000028000000140000001500000103000000060000002a0000000600000000000000" : String} LAWS.program_bytes_back (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=program_bytes_back) law program_bytes_back: {I.bpf_of_octets(I.BpfBig{}, I.bpf_to_octets(I.BpfBig{}, rarp())) == Done{rarp()} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>} LAWS.octets_max_default (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=octets_max_default) # the default limit on stored programs: 8 bytes for each of BPF_MAXINSNS # instructions (compared as U32, which holds both) law octets_max_default: {U32.from_nat(I.bpf_octets_max()) == U32.mul(8, U32.from_nat(V.bpf_maxinsns())) : U32} LAWS.octets_limit_refuses (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=octets_limit_refuses) law octets_limit_refuses: {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>>} LAWS.octets_limit_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=octets_limit_accepts) law octets_limit_accepts: {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>>} LAWS.seccomp_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_example) # seccomp(2), EXAMPLES, install_filter(syscall_nr, t_arch, f_errno) with # t_arch = AUDIT_ARCH_X86_64, so upper_nr_limit = X32_SYSCALL_BIT - 1: the # call syscall_nr fails with f_errno, other calls are allowed, and another # architecture or an x32 call (nr above the limit) kills the process def seccomp_example(nr: U32, e: U32) -> List<&2, I.BpfOp>: LAWS.sc_call (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=sc_call) def sc_call(nr: U32, arch: U32) -> S.SeccompData: LAWS.deny (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=deny) # ERRNO(e) for system call nr, ALLOW for the others def deny(nr: U32, e: U32) -> List<&2, I.BpfOp>: LAWS.seccomp_example_valid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_example_valid) law seccomp_example_valid: {S.seccomp_validate(V.bpf_maxinsns(), seccomp_example(59, 99)) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>} LAWS.seccomp_example_errno (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_example_errno) law seccomp_example_errno: {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>} LAWS.seccomp_example_allow (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_example_allow) law seccomp_example_allow: {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>} LAWS.seccomp_example_other_arch (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_example_other_arch) law seccomp_example_other_arch: {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>} LAWS.seccomp_example_x32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_example_x32) law seccomp_example_x32: {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>} LAWS.seccomp_rejects_byte_load (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_rejects_byte_load) law seccomp_rejects_byte_load: {S.seccomp_validate(V.bpf_maxinsns(), finger()) == Fail{I.BpfErrSeccompLoad{0n}} : Result<&2, &2, I.BpfError, Unit>} LAWS.seccomp_rejects_unaligned (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_rejects_unaligned) law seccomp_rejects_unaligned: {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>} LAWS.stack_newest_on_tie (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=stack_newest_on_tie) # two filters with the same action: the newer one wins, with its data law stack_newest_on_tie: {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>} LAWS.stack_most_restrictive (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=stack_most_restrictive) law stack_most_restrictive: {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>} LAWS.stack_empty_allows (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=stack_empty_allows) law stack_empty_allows: {S.seccomp_eval([], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64())) == Done{S.SeccompAllow{}} : Result<&2, &2, I.BpfError, S.SeccompAction>} LAWS.unknown_action_kills (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=unknown_action_kills) law unknown_action_kills: {S.SeccompAction.of_u32(65536) == S.SeccompKillProcess{} : S.SeccompAction} LAWS.install_path_limit (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=install_path_limit) law install_path_limit: {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>>>} LAWS.install_pushes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=install_pushes) law install_pushes: {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>>>} LAWS.seccomp_rejects_mod (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_rejects_mod) law seccomp_rejects_mod: {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>} LAWS.seccomp_example_write (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_example_write) # the page's runs: ./a.out 1 0xC000003E 99 makes write (1) fail, and # ./a.out 295 0xC000003E 99 leaves the calls whoami makes alone law seccomp_example_write: {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>} LAWS.seccomp_example_preadv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=seccomp_example_preadv) law seccomp_example_preadv: {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>} LAWS.validate_mem_init (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_mem_init) # scratch memory read before it is written: refused by default, on every # path (here the jump past the store), and allowed by the permissive options law validate_mem_init: {V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}]) == Fail{I.BpfErrMemInit{0n}} : Result<&2, &2, I.BpfError, Unit>} LAWS.validate_mem_init_path (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_mem_init_path) law validate_mem_init_path: {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>} LAWS.validate_mem_init_written (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_mem_init_written) law validate_mem_init_written: {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>} LAWS.validate_mem_after_jump (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_mem_after_jump) # code after a jump is reached only by jumps to it; code after a return # counts as reached from the return, as Linux counts it law validate_mem_after_jump: {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>} LAWS.validate_mem_after_return (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_mem_after_return) law validate_mem_after_return: {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>} LAWS.validate_permissive (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validate_permissive) law validate_permissive: {V.bpf_validate_with(V.BpfValidateOptions.permissive(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}]) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>} LAWS.witness_skip_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=witness_skip_length) law witness_skip_length: {List.length(&2, I.BpfOp, [I.BpfTax{}, I.BpfTxa{}, I.BpfNeg{}]) == U32.to_nat(3) : Nat} LAWS.witness_octets_over (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=witness_octets_over) law witness_octets_over: {B.Octets.at(B.Octets.zeros(9n), 8n) == Some{0} : Maybe<&2, U32>} LAWS.witness_rank_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=witness_rank_le) law witness_rank_le: {Nat.is_le(S.SeccompAction.rank(S.SeccompErrno{1}), S.SeccompAction.rank(S.SeccompErrno{2})) == True{} : Bool} LAWS.witness_rank_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=witness_rank_lt) law witness_rank_lt: {Nat.is_lt(S.SeccompAction.rank(S.SeccompKillProcess{}), S.SeccompAction.rank(S.SeccompAllow{})) == True{} : Bool} PROOF.absurd.bool (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=absurd.bool) def absurd.bool(b: Bool) -> Type: PROOF.absurd.ft (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=absurd.ft) def absurd.ft(e: {False{} == True{} : Bool}) -> Empty: PROOF.absurd.res (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=absurd.res) def absurd.res(r: Result<&2, &2, I.BpfError, Unit>) -> Type: PROOF.absurd.fd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=absurd.fd) def absurd.fd(-e: I.BpfError, h: {Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> Empty: PROOF.nat.lt_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=nat.lt_zero) def nat.lt_zero(x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}: PROOF.need_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=need_ok) def need_ok(b: Bool, -e: I.BpfError, h: {V.bpf_chk(b, e) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {b == True{} : Bool}: PROOF.both_l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=both_l) def both_l(r: Result<&2, &2, I.BpfError, Unit>, -s: Result<&2, &2, I.BpfError, Unit>, h: {V.bpf_both(r, s) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {r == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}: PROOF.both_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=both_r) def both_r(r: Result<&2, &2, I.BpfError, Unit>, -s: Result<&2, &2, I.BpfError, Unit>, h: {V.bpf_both(r, s) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {s == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}: PROOF.nxt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=nxt) def nxt(-pc: Nat, r: Nat, h: {V.bpf_check.next(pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {Nat.is_lt(0n, r) == True{} : Bool}: PROOF.step_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=step_ok) def step_ok(cur: R.BpfStep, r: Nat) -> Bool: PROOF.step_of_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=step_of_ok) def step_of_ok(m: Maybe<&2, R.BpfState>, -r: Nat, e: {Nat.is_lt(0n, r) == True{} : Bool}) -> {step_ok(R.bpf_step.of(m), r) == True{} : Bool}: PROOF.scratch_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=scratch_ok) def scratch_ok(ok: Bool, -k: U32, -st: R.BpfState, -r: Nat, e1: {ok == True{} : Bool}, e2: {Nat.is_lt(0n, r) == True{} : Bool}) -> {step_ok(R.bpf_scratch(ok, k, st), r) == True{} : Bool}: PROOF.mem_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=mem_ok) def mem_ok(+k: U32, -st: R.BpfState, +pc: Nat, +r: Nat, +h: {V.bpf_check.mem(k, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {step_ok(R.bpf_scratch(U32.is_lt(k, I.bpf_memwords()), k, st), r) == True{} : Bool}: PROOF.jsel_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=jsel_ok) def jsel_ok(hit: Bool, -jt: U32, -jf: U32, -r: Nat, e1: {Nat.is_lt(U32.to_nat(jt), r) == True{} : Bool}, e2: {Nat.is_lt(U32.to_nat(jf), r) == True{} : Bool}) -> {Nat.is_lt(R.bpf_jsel(hit, jt, jf), r) == True{} : Bool}: PROOF.jmp_ranges (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=jmp_ranges) # the two range checks inside bpf_check.jmp def jmp_ranges(+jt: U32, +jf: U32, +pc: Nat, +r: Nat, +h: {V.bpf_check.jmp(jt, jf, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {V.bpf_both(V.bpf_chk(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}), V.bpf_chk(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc})) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}: PROOF.jmp_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=jmp_ok) def jmp_ok(+jt: U32, +jf: U32, +pc: Nat, +r: Nat, hit: Bool, h: {V.bpf_check.jmp(jt, jf, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {Nat.is_lt(R.bpf_jsel(hit, jt, jf), r) == True{} : Bool}: PROOF.exec_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=exec_ok) # every instruction that passed its checks steps to an instruction that exists def exec_ok(op: I.BpfOp, st: R.BpfState, +inp: R.BpfInput, +pc: Nat, +r: Nat, h: {V.bpf_check.op(op, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {step_ok(R.bpf_exec(op, st, inp), r) == True{} : Bool}: PROOF.go_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=go_ok) # A run from a fine step, over instructions that passed their checks, # answers Done: induction on the instructions def go_ok(xs: List<&2, I.BpfOp>, cur: R.BpfStep, +inp: R.BpfInput, +pc: Nat, +v: {V.bpf_check.all(xs, pc) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, p: {step_ok(cur, List.length(&2, I.BpfOp, xs)) == True{} : Bool}) -> {Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(xs, cur, inp)) == True{} : Bool}: More: https://jend.leeeet.dev/packages/bend-osdev-bpf.txt?definitions_offset=100