Scc for callbacks #10514
Open
Scc for callbacks #10514
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
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
0de3956 to
2d78e4d
Compare
This is a correctness fix for the verification of BPF programs that work with callback-calling functions. The problem is the same as the issue fixed by series [1] for iterator-based loops: some of the states created while processing the callback function body might have incomplete read or precision marks. An example of an unsafe program that is accepted without this fix can be found in patch #2. There is some impact on verification performance: File Program Insns (A) Insns (B) Insns (DIFF) ------------------------------- -------------------- --------- --------- ----------------- pyperf600_bpf_loop.bpf.o on_event 3429 8259 +4830 (+140.86%) setget_sockopt.bpf.o skops_sockopt 4478 6043 +1565 (+34.95%) setget_sockopt.bpf.o socket_post_create 958 1271 +313 (+32.67%) strobemeta_bpf_loop.bpf.o on_event 2689 6312 +3623 (+134.73%) test_tcp_custom_syncookie.bpf.o tcp_custom_syncookie 9217 27385 +18168 (+197.11%) xdp_synproxy_kern.bpf.o syncookie_tc 6809 13773 +6964 (+102.28%) xdp_synproxy_kern.bpf.o syncookie_xdp 6819 13783 +6964 (+102.13%) Total progs: 4161 Old success: 2508 New success: 2507 total_insns diff min : 0.00 % total_insns diff max : 197.11 % total_insns abs max old : 806,540 total_insns abs max new : 806,540 0 .. 5 %: 4148 5 .. 15 %: 5 30 .. 40 %: 2 40 .. 50 %: 1 100 .. 110 %: 2 130 .. 140 %: 1 140 .. 150 %: 1 195 .. 200 %: 1 [1] https://lore.kernel.org/bpf/174968344350.3524559.14906547029551737094.git-patchwork-notify@kernel.org/ --- b4-submit-tracking --- { "series": { "revision": 1, "change-id": "20251219-scc-for-callbacks-d6d94faa2e43", "prefixes": [] } }
Calls like bpf_loop() or bpf_for_each_map_elem() introduce loops that are not explicitly present in the control-flow graph. The verifier processes such calls by repeatedly interpreting the callback function body within the same verification path (until the current state converges with a previous state). Such loops require a bpf_scc_visit instance in order to allow the accumulation of the state graph backedges. Otherwise, certain checkpoint states created within the bodies of such loops will have incomplete precision marks. See the next patch for an example of a program that leads to the verifier accepting an unsafe program. Fixes: 96c6aa4 ("bpf: compute SCCs in program control flow graph") Fixes: c9e3190 ("bpf: propagate read/precision marks over state graph backedges") Reported-by: Breno Leitao <leitao@debian.org> Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Test for state graph backedges accumulation for SCCs formed by
bpf_loop(). Equivalent to the following C program:
int main(void) {
1: fp[-8] = bpf_get_prandom_u32();
2: fp[-16] = -32; // used in a memory access below
3: bpf_loop(7, loop_cb4, fp, 0);
4: return 0;
}
int loop_cb4(int i, void *ctx) {
5: if (unlikely(ctx[-8] > bpf_get_prandom_u32()))
6: *(u64 *)(fp + ctx[-16]) = 42; // aligned access expected
7: if (unlikely(fp[-8] > bpf_get_prandom_u32()))
8: ctx[-16] = -31; // makes said access unaligned
9: return 0;
}
If state graph backedges are not accumulated properly at the SCC
formed by loop_cb4() call from bpf_loop(), the state {ctx[-16]=-32}
injected at instruction 9 on verification path 1,2,3,5,7,9,4 would be
considered fully verified and would lack precision mark for ctx[-16].
This would lead to early pruning of verification path 1,2,3,5,7,8,9 in
state {ctx[-16]=-31}, which in turn leads to the incorrect assumption
that the above program is safe.
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
eddyz87
force-pushed
the
scc-for-callbacks
branch
from
f7fc7fb to
1b0046c
Compare
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.
No description provided.