Scc for callbacks #10555
Closed
Scc for callbacks #10555
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 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 4247 9985 +5738 (+135.11%) setget_sockopt.bpf.o skops_sockopt 5719 7446 +1727 (+30.20%) setget_sockopt.bpf.o socket_post_create 1253 1603 +350 (+27.93%) strobemeta_bpf_loop.bpf.o on_event 3424 7224 +3800 (+110.98%) test_tcp_custom_syncookie.bpf.o tcp_custom_syncookie 11929 38307 +26378 (+221.12%) xdp_synproxy_kern.bpf.o syncookie_tc 13986 23035 +9049 (+64.70%) xdp_synproxy_kern.bpf.o syncookie_xdp 13881 21022 +7141 (+51.44%) Total progs: 4172 Old success: 2520 New success: 2520 total_insns diff min: 0.00% total_insns diff max: 221.12% 0 -> value: 0 value -> 0: 0 total_insns abs max old: 837,487 total_insns abs max new: 837,487 0 .. 5 %: 4163 5 .. 15 %: 2 25 .. 35 %: 2 50 .. 60 %: 1 60 .. 70 %: 1 110 .. 120 %: 1 135 .. 145 %: 1 220 .. 225 %: 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
0428fea to
a1ccce2
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
15 times, most recently
from
22bf7db to
d1dcae1
Compare
|
Automatically cleaning up stale PR; feel free to reopen if needed |
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.