test bpf verifier div #10528
Open
test bpf verifier div #10528
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This patch introduces interval analysis (range tracking) and tnum
analysis (bitwise tracking) for both signed and unsigned division
operations in the BPF verifier.
The BPF verifier currently lacks support for value tracking on BPF_DIV
instructions, which can lead to false positives during verification of
BPF programs that utilize division instructions.
According to the BPF instruction set[1], the instruction's offset field
(`insn->off`) is used to distinguish between signed (`off == 1`) and
unsigned division (`off == 0`). Moreover, we also follow the BPF division
semantics to handle special cases, such as division by zero and signed
division overflow.
- UDIV: dst = (src != 0) ? (dst / src) : 0
- SDIV: dst = (src == 0) ? 0 : ((src == -1 && dst == LLONG_MIN) ? LLONG_MIN : (dst / src))
Here is the overview of the changes made in this patch:
1. For interval analysis:
- Added `scalar_min_max_udiv` and `scalar32_min_max_udiv` to update
umin/umax bounds, which is straightforward.
- Added `scalar_min_max_sdiv` and `scalar32_min_max_sdiv` to update
smin/smax bounds. It handles non-monotonic intervals by decomposing
the divisor range into negative, zero, and positive sub-ranges, and
computing the result range for each sub-range separately. Finally,
it combines the results to get the final smin/smax bounds.
2. For tnum analysis, we referred to LLVM's KnownBits implementation[2]
and the recent research on abstract interpretation of division[3]:
- Added `tnum_udiv` to compute the tnum for unsigned division. It
calculates the maximum possible result based on the maximum values
of the dividend tnum and the minimum values of the divisor tnum,
then constructs the resulting tnum accordingly. We have prove its
soundness using Rocq Prover[4].
- Added `tnum_sdiv` to compute the tnum for signed division. It splits
the operands into positive and negative components, then performs
calculation on absolute values using `tnum_udiv`, finally unions
the results to ensure soundness.
3. Also updated existing selftests based on the expected BPF_DIV behavior.
[1] https://www.kernel.org/doc/Documentation/bpf/standardization/instruction-set.rst
[2] https://llvm.org/doxygen/KnownBits_8cpp_source.html
[3] https://dl.acm.org/doi/10.1145/3728905
[4] https://github.com/shenghaoyuan/open-verified-artifacts/tree/main/tnum
Co-developed-by: Shenghao Yuan <shenghaoyuan0928@163.com>
Signed-off-by: Shenghao Yuan <shenghaoyuan0928@163.com>
Co-developed-by: Tianci Cao <ziye@zju.edu.cn>
Signed-off-by: Tianci Cao <ziye@zju.edu.cn>
Signed-off-by: Yazhou Tang <tangyazhou518@outlook.com>
Now BPF_DIV has value tracking support via interval and tnum analysis. This patch adds selftests to cover various cases of signed and unsigned division operations, including edge cases like division by zero and signed division overflow. Specifically, these selftests are based on dead code elimination: If the BPF verifier can precisely analyze the result of a division operation, it can prune the path that leads to an error (here we use illegal pointer dereference as the error case), allowing the program to pass verification. Co-developed-by: Shenghao Yuan <shenghaoyuan0928@163.com> Signed-off-by: Shenghao Yuan <shenghaoyuan0928@163.com> Co-developed-by: Tianci Cao <ziye@zju.edu.cn> Signed-off-by: Tianci Cao <ziye@zju.edu.cn> Signed-off-by: Yazhou Tang <tangyazhou518@outlook.com>
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
2 times, most recently
from
5007636 to
0ac68c9
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
PR before: #10433 #10251