Alan Jowett
Alan Jowett
BPF programs with local calls (calls to BPF sub-programs) should separate the main program and the sub-program into different sections in the ELF file. Entry point BPF programs each go...
https://github.com/dthaler/ebpf-docs-1/blob/elf/rst/elf.rst#142btf-map-definitions defines the format for the new ".maps" BTF map definition section. bpf_writer should have an option to write out the new map format.
This pull request introduces support for atomic operations in the disassembler and improves the handling of atomic compare-exchange instructions in the JIT compiler. The most important changes include handling atomic...
Resolves: #741 This pull request includes changes to the `ebpf_domain.cpp` file to handle 32-bit operations more robustly and adds new test cases for 32-bit pointer truncation operations in the `test-data/pointer.yaml`...
This pull request includes changes to improve the handling of unreachable code detection and adds new test cases for various infinite loop scenarios. The most important changes include adding a...
Resolves: #728 This pull request exposes a new API "ebpf_check_constraints_at_label" which permits the caller to compare a set of constraints against the model at a specific label. If the model...
All these tests should fail, but currently pass: ```yaml --- test-case: simple infinite loop, less than options: ["termination"] pre: [] code: : | r0 = 0 if r0 < 1...
Verifier should reject this sequence as it has reserved bits being set to non-zero. (Note offset field in mod operation is set, which should be rejected). ``` 00000000: b7000000003000fd b50001007aff0008...
Repro (from fuzzer) ```asm add32 %r1, 0x0 stw [%r1+22], 0x2000000 exit ``` add32 truncates the upper bits of the pointer, making it completely invalid.
Missing the multiplication case here: https://github.com/vbpf/ebpf-verifier/blob/80ada1c8b96263a924990a95576633223d355fbe/src/assertions.cpp#L211 Repro sequence as generated by fuzzer: ```asm mov32 %r0, 0x830800 mul %r0, %r3 jne %r1, %r0, +0 exit ```