bpf: propagate read/precision marks over state graph backedges #8999
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
Author
|
Upstream branch: 079e5c5 |
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
61c8df2 to
708d4b4
Compare
Author
|
Upstream branch: db22b13 |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
6c1d78e to
71137b4
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
708d4b4 to
6c5a4cd
Compare
Author
|
Upstream branch: 1ae7a84 |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
71137b4 to
1f40cd5
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
6c5a4cd to
1918227
Compare
Author
|
Upstream branch: 86bc9c7 |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
1f40cd5 to
5559a33
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
1918227 to
3777056
Compare
Author
|
Upstream branch: d496557 |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
5559a33 to
df3cebe
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
3777056 to
7f76eaa
Compare
Author
|
Upstream branch: ca56fbd |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
df3cebe to
084a16f
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
7f76eaa to
5ab4b7b
Compare
Author
|
Upstream branch: 5ffb537 |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
084a16f to
aee7dc4
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
5ab4b7b to
21880e2
Compare
Author
|
Upstream branch: c5cebb2 |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
aee7dc4 to
b7b2b19
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
21880e2 to
86d7ac4
Compare
Author
|
Upstream branch: 90b83ef |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
ac84f36 to
72ece34
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
79f300f to
aac333e
Compare
Author
|
Upstream branch: 3b55a9e |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
72ece34 to
b807c99
Compare
This reverts commit 96a30e4. Next patches in the series modify propagate_precision() to allow arbitrary starting state. Precision propagation requires access to jump history, and arbitrary states represent history not belonging to `env->cur_state`. Signed-off-by: Eduard Zingerman <[email protected]>
Compute strongly connected components in the program CFG. Assign an SCC number to each instruction, recorded in env->insn_aux[*].scc. Use Tarjan's algorithm for SCC computation adapted to run non-recursively. For debug purposes print out computed SCCs as a part of full program dump in compute_live_registers() at log level 2, e.g.: func#0 @0 Live regs before insn: 0: .......... (b4) w6 = 10 2 1: ......6... (18) r1 = 0xffff88810bbb5565 2 3: .1....6... (b4) w2 = 2 2 4: .12...6... (85) call bpf_trace_printk#6 2 5: ......6... (04) w6 += -1 2 6: ......6... (56) if w6 != 0x0 goto pc-6 7: .......... (b4) w6 = 5 1 8: ......6... (18) r1 = 0xffff88810bbb5567 1 10: .1....6... (b4) w2 = 2 1 11: .12...6... (85) call bpf_trace_printk#6 1 12: ......6... (04) w6 += -1 1 13: ......6... (56) if w6 != 0x0 goto pc-6 14: .......... (b4) w0 = 0 15: 0......... (95) exit ^^^ SCC number for the instruction Signed-off-by: Eduard Zingerman <[email protected]>
A function to return IP for a given frame in a call stack of a state. Will be used by a next patch. The `state->insn_idx = env->insn_idx;` assignment in the do_check() allows to use frame_insn_idx with env->cur_state. At the moment bpf_verifier_state->insn_idx is set when new cached state is added in is_state_visited() and accessed only in the contexts when the state is already in the cache. Hence this assignment does not change verifier behaviour. Signed-off-by: Eduard Zingerman <[email protected]>
Allow `mark_chain_precision()` to run from an arbitrary starting state by replacing direct references to `env->cur_state` with a parameter. Signed-off-by: Eduard Zingerman <[email protected]>
Add an out parameter to `propagate_precision()` to record whether any new precision bits were set during its execution. Signed-off-by: Eduard Zingerman <[email protected]>
Add an out parameter to `propagate_liveness()` to record whether any new liveness bits were set during its execution. Signed-off-by: Eduard Zingerman <[email protected]>
The next patch would add some relatively heavy-weight operation to clean_live_states(), this operation can be skipped if REG_LIVE_DONE is set. Move the check from clean_verifier_state() to clean_verifier_state() as a small refactoring commit. Signed-off-by: Eduard Zingerman <[email protected]>
Current loop_entry-based exact states comparison logic does not handle
the following case:
.-> A --. Assume the states are visited in the order A, B, C.
| | | Assume that state B reaches a state equivalent to state A.
| v v At this point, state C is not processed yet, so state A
'-- B C has not received any read or precision marks from C.
As a result, these marks won't be propagated to B.
If B has incomplete marks, it is unsafe to use it in states_equal()
checks.
This commit replaces the existing logic with the following:
- Strongly connected components (SCCs) are computed over the program's
control flow graph (intraprocedurally).
- When a verifier state enters an SCC, that state is recorded as the
SCC entry point.
- When a verifier state is found equivalent to another (e.g., B to A
in the example), it is recorded as a states graph backedge.
Backedges are accumulated per SCC.
- When an SCC entry state reaches `branches == 0`, read and precision
marks are propagated through the backedges (e.g., from A to B, from
C to A, and then again from A to B).
To support nested subprogram calls, the entry state and backedge list
are associated not with the SCC itself but with an object called
`bpf_scc_callchain`. A callchain is a tuple `(callsite*, scc_id)`,
where `callsite` is the index of a call instruction for each frame
except the last.
See the comments added in `is_state_visited()` and
`compute_scc_callchain()` for more details.
Fixes: 2a09928 ("bpf: correct loop detection for iterators convergence")
Signed-off-by: Eduard Zingerman <[email protected]>
The previous patch switched read and precision tracking for iterator-based loops from state-graph-based loop tracking to control-flow-graph-based loop tracking. This patch removes the now-unused `update_loop_entry()` and `get_loop_entry()` functions, which were part of the state-graph-based logic. Signed-off-by: Eduard Zingerman <[email protected]>
Author
|
Upstream branch: 3b55a9e |
Count states accumulated in bpf_scc_visit->backedges in env->peak_states. Signed-off-by: Eduard Zingerman <[email protected]>
The test case absent_mark_in_the_middle_state is equivalent of the
following C program:
1: r8 = bpf_get_prandom_u32();
2: r6 = -32;
3: bpf_iter_num_new(&fp[-8], 0, 10);
4: if (unlikely(bpf_get_prandom_u32()))
5: r6 = -31;
6: for (;;) {
7: if (!bpf_iter_num_next(&fp[-8]))
8: break;
9: if (unlikely(bpf_get_prandom_u32()))
10: *(u64 *)(fp + r6) = 7;
11: }
12: bpf_iter_num_destroy(&fp[-8]);
13: return 0;
W/o a fix that instructs verifier to ignore branches count for loop
entries verification proceeds as follows:
- 1-4, state is {r6=-32,fp-8=active};
- 6, checkpoint A is created with {r6=-32,fp-8=active};
- 7, checkpoint B is created with {r6=-32,fp-8=active},
push state {r6=-32,fp-8=active} from 7 to 9;
- 8,12,13, {r6=-32,fp-8=drained}, exit;
- pop state with {r6=-32,fp-8=active} from 7 to 9;
- 9, push state {r6=-32,fp-8=active} from 9 to 10;
- 6, checkpoint C is created with {r6=-32,fp-8=active};
- 7, checkpoint A is hit, no precision propagated for r6 to C;
- pop state {r6=-32,fp-8=active} from 9 to 10;
- 10, state is {r6=-31,fp-8=active}, r6 is marked as read and precise,
these marks are propagated to checkpoints A and B (but not C, as
it is not the parent of current state;
- 6, {r6=-31,fp-8=active} checkpoint C is hit, because r6 is not
marked precise for this checkpoint;
- the program is accepted, despite a possibility of unaligned u64
stack access at offset -31.
The test case absent_mark_in_the_middle_state2 is similar except the
following change:
r8 = bpf_get_prandom_u32();
r6 = -32;
bpf_iter_num_new(&fp[-8], 0, 10);
if (unlikely(bpf_get_prandom_u32())) {
r6 = -31;
+ jump_into_loop:
+ goto +0;
+ goto loop;
+ }
+ if (unlikely(bpf_get_prandom_u32()))
+ goto jump_into_loop;
+ loop:
for (;;) {
if (!bpf_iter_num_next(&fp[-8]))
break;
if (unlikely(bpf_get_prandom_u32()))
*(u64 *)(fp + r6) = 7;
}
bpf_iter_num_destroy(&fp[-8])
return 0
The goal is to check that read/precision marks are propagated to
checkpoint created at 'goto +0' that resides outside of the loop.
The test case absent_mark_in_the_middle_state3 is a bit different and
is equivalent to the C program below:
int absent_mark_in_the_middle_state3(void)
{
bpf_iter_num_new(&fp[-8], 0, 10)
loop1(-32, &fp[-8])
loop1_wrapper(&fp[-8])
bpf_iter_num_destroy(&fp[-8])
}
int loop1(num, iter)
{
while (bpf_iter_num_next(iter)) {
if (unlikely(bpf_get_prandom_u32()))
*(fp + num) = 7;
}
return 0
}
int loop1_wrapper(iter)
{
r6 = -32;
if (unlikely(bpf_get_prandom_u32()))
r6 = -31;
loop1(r6, iter);
return 0;
}
The unsafe state is reached in a similar manner, but the loop is
located inside a subprogram that is called from two locations in the
main subprogram. This detail is important for exercising
bpf_scc_visit->backedges memory management.
Signed-off-by: Eduard Zingerman <[email protected]>
kernel-patches-daemon-bpf
bot
force-pushed
the
series/966154=>bpf-next
branch
from
b807c99 to
0d2f8e3
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
2 times, most recently
from
c88deee to
19765cc
Compare
Author
|
At least one diff in series https://patchwork.kernel.org/project/netdevbpf/list/?series=971030 irrelevant now. Closing PR. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Pull request for series with
subject: bpf: propagate read/precision marks over state graph backedges
version: 1
url: https://patchwork.kernel.org/project/netdevbpf/list/?series=966154