The main object of this patch series is to support verification of eBPF
programs with bounded loops. Only bounds derived from JLT (unsigned <)
with the taken branch in the loop are supported, but it should be clear
how others could be added.
Testing of these changes has consisted only of test_verifier (including
a small number of loop tests added in patch #8). Much more testing
(including more test_verifier test cases) would be needed before these
patches could be considered ready to apply.
That said, some component parts of the series are useful outside of the
context of bounded loop handling, and may be worth applying separately.
Patches #1 and #2 (tests) are a nice cleanup/simplification of subprog
marking. I posted them a couple of weeks ago as RFC "bpf/verifier:
simplify subprog tracking"; I have not yet integrated the comments and
suggestions from replies on that posting (so no need to repeat them!)
Patch #3 is a cleanup we've wanted to do since func_calls went in,
putting parent pointers in the registers instead of the state so that
we don't need skip_callee() machinery. Again, worth doing on its own
even if the bounded loops stuff is rejected.
Patch #4 moves the saved return-addresses in bpf_func_state down one
frame, so that we don't store a meaningless callsite of -1 in the
outermost frame and we do store a state's current insn_idx in the
innermost frame. This is necessary for my approach to loop handling,
which needs to identify the location of jump insns when a loop is
Patch #5 adds a new parent state pointer into bpf_func_state (it should
really be in bpf_verifier_state, and I later (Patch #10) figured out
how to make that work) and walks back along these pointers to detect
loops each time a state list mark is visited. This then replaces the
static loop detection in check_cfg.
The verifier already did not walk impossible JEQ/JNE branches; patch #6
extends this to greater-than/less-than type branches. As well as
allowing us to reduce the number of paths walked and prevent
inconsistent min/max state (potentially making this another one useful
outside of the series), this means that when we walk around a bounded
loop we can eventually determine that we're done and stop walking it.
Patch #7 implements the key 'boundedness detection', looking at the
register state last time through the loop and ensuring that the loop
is on course to terminate in a reasonable number of iterations. The
behaviour could be improved by having it store some state about what
the boundedness check concluded (e.g. the delta last time through the
loop) in the new explored_state.
Patch #8 adds some tests for bounded loops, mainly either probing for
bugs that existed in early versions of the code, or testing constructs
which are (or were) beyond the verifier's ability to understand. As
noted above, there are not nearly enough tests here yet.
Patch #9 is a better way to distinguish between states which have been
shown to safely reach an exit, and states whose continuations are
still being explored (since the latter cannot be used for pruning),
rather than just distrusting all states which appear in a loop body.
Patches #10 and #11 improve upon some suboptimal code from earlier in
the series, mostly from patch #5. I haven't yet had time to fold them
into the earlier patches. Patch #12 updates a test to match.
bpf/verifier: validate func_calls by marking at do_check() time
bpf/verifier: update selftests
bpf/verifier: per-register parent pointers
bpf/verifier: store insn_idx instead of callsite in bpf_func_state
bpf/verifier: detect loops dynamically rather than statically
bpf/verifier: do not walk impossible branches
bpf/verifier: allow bounded loops with JLT/true back-edge
bpf/verifier: selftests for bounded loops
bpf/verifier: count still-live children of explored_states
bpf/verifier: parent state pointer is not per-frame
bpf/verifier: better detection of statically unreachable code
bpf/verifier: update selftests
include/linux/bpf_verifier.h | 46 +-
kernel/bpf/verifier.c | 1267 +++++++++++++++------------
tools/testing/selftests/bpf/test_verifier.c | 248 +++++-
3 files changed, 949 insertions(+), 612 deletions(-)