Re: [PATCH bpf-next v2 00/35] bpf: A verifier that joins states

["Alexei Starovoitov" <alexei.starovoitov@gmail.com>]

There will be a v3.

Real bug is in patch 21.
The callee gets wrong bounds, and an access out of bounds
loads. It has to be clear_scalar_id().

patch  from     what
-----  -------  ------------------------------------------------------
1      sashiko  * Messages print the index of an insn after may_goto
                  is added. It has to be orig_idx.
4, 5   both     * join_reg() drops delta under explore_alu_limits.
                  verifier_bug(), -EFAULT. No join in this case.
                  It takes CAP_BPF without CAP_PERFMON.
5, 19  sashiko    join_func() refuses a join when only 'b' has stack
                  arguments. It costs one more state.
9      both     * What bpf_rdonly_cast() and bpf_cast_to_kern_ctx()
                  return counts as a number. A valid prog is rejected.
9      sashiko  * ctx on one path only. The pointer to the packet
                  counts as a number. The pass ends all the same:
                  flow_kinds_meet() only clears bits.
9      sashiko  * A pointer that store-release spills counts as a
                  number after the fill. Load-acquire from a slot
                  gives FLOW_IS_OTHER. That costs states at most.
10     bpf-ci   * BPF_END | BPF_TO_BE counts as 'dst op= r0' in four
                  tables. It costs insns where r0 is live.
13     bpf-ci   * flow_join_makes_up() reads the ids of 'a' only.
                  The join drops a link between two numbers.
19     both     * bail_insn can be an exit that is dead code.
                  r0 is not live there. A valid prog is rejected.
19     bpf-ci   * A loop that only bpf_throw() ends has no exit.
                  For the graph bpf_throw() returns, so what follows
                  it is in the loop.
19     bpf-ci   * The order of nospec and the added may_goto.
                  Only without CAP_PERFMON.
19     bpf-ci   * -ENOSPC at log level 1 for a prog that loads.
                  See below.
19     sashiko  * loop_guard stays when all is verified again.
                  Harmless: 'r0 = 0; exit' that nobody jumps to.
20     bpf-ci   * A register that only the loop sets stays NOT_INIT in
                  the state that covers all iterations. A valid prog
                  is rejected.
21     both     * bpf_flow_return() drops 'speculative' of an exit.
                  Stricter than it has to be. Without CAP_PERFMON.
21     sashiko  * has_rcu_read_lock() is false in a static subprog
                  that a timer callback calls. Stricter, too.
22     bpf-ci   * Marks of recursion that only callx makes reject
                  progs without recursion. No released kernel has
                  callx.
22     both     * A subprog that is not live keeps the mark. Its
                  frame in arena takes room from the live ones.
22     sashiko    The guard of a recursive subprog at a back edge to
                  its first insn. The extra edge can only reject.

Patches 2 and 22, both: the padding of a recursive frame comes after the
check of the stack depth.
Right. The check has to see it.

Patch 2, bpf-ci: what comes after the check of r10.
The lower half of the stack is the reserve for that. For this reason
recursion is refused in tracing progs, in progs that call
bpf_clone_redirect(), and for an extension of a subprog that is called in
a recursion.

Patch 19, bpf-ci: log level 1 and -ENOSPC.
There are no paths, so there is no position to roll the log back to.
Level 1 has the blocks of the pass, in the order of the pass.
log_true_size tells the size. libbpf grows its own buffer on -ENOSPC.
The follow-up: the log that is dropped when a prog is safe does not count.

Not bugs, or not worth more code
================================
Patch 1, sashiko: 'gotol -1' that gets a guard.
No. Its loop has no exit, so flow_place_guards() has no place for may_goto.
loop_stack_push() rejects the prog: "loop at insn %d never exits".
Same as for 'goto -1'.

Patch 5, sashiko: join_func() and a slot that only one state has.
Right. Only without CAP_PERFMON. Not worth it.

Patches 18 and 19, sashiko: update_insn() has no edge to
bpf_head_guard_target().
That's deliberate. See the comment above bpf_head_guard_target(): stack
that is dead at the head stays dead. A read of it at the target is
rejected. guard_at_head_dead_slot in verifier_budget.c tests it.

Patch 19, sashiko: loop_stack[].refs is stale after a release.
Right, the count is stale. Not a leak. check_refs_taken_in_loop() only
reports early. The reference stays in refs[] until it is released, and
BPF_EXIT rejects it. The report comes one iteration later.
Not worth more code.

Patch 19, sashiko: a nospec exit and the states that the insn pushed.
No. Today's do_check() goes to pop_stack() there and verifies them.
The edge of check_loop_guard() has to be delivered: the added may_goto is
in front of the barrier.

Patch 19, sashiko: do_check_all() goes on after -EAGAIN, -ENOMEM, -EFAULT.
Deliberate. A signal is still pending in the next round, and flow_merge()
returns -EAGAIN for its first state.

Patch 19, both: offloaded progs.
Yes. A loop of an offloaded prog has to have a count. Not worth more code.

Patch 21, bpf-ci: insns_total counts some insns twice.
Yes. insns_total of a static subprog is an estimate. The main prog and
global subprogs have exact numbers. Not worth more code.

Patch 22, sashiko: compute_call_depth() is one frame short.
Nobody knows how many frames a recursion has. The check of r10 limits them
at run time. The arrays of MAX_CALL_FRAMES have their own checks.

Patch 22, sashiko: the edge of an async callback in build_call_graph().
Not from this series. bpf-next has the same is_async_cb test and the same
"recursive call from" message.

Patch 34, sashiko: 2^46 iterations in the interpreter.
No. All may_goto of a subprog use one slot. BPF_MAX_LOOPS is stored there
once, at the entry of the subprog.

Patch 35, sashiko: __load_if_JITed() for callx_one_of_two_not_written.
The test is built for x86-64, arm64 and riscv64. The selftests config has
CONFIG_BPF_JIT_ALWAYS_ON=y there. Without JIT this file fails today.
CAN_USE_CALLX is the same three archs plus indirect calls in C. This callx
is in asm.

Only in the middle of the series. Not worth it
==============================================

  patch  what
  -----  ---------------------------------------------------------------
  3      The prototypes of join.c and env->join are one patch early.
  5      iter in bpf_reg_state is 8 bytes larger until patch 23.
  9      addr_taken is set by patch 28. Its log says so.
  17     per_trip is read first by patch 20. Only W=1 warns.
  19     id_gen has no bound in patches 19 and 20. Patch 21 adds it.
  29     The log does not say that for_u32_spills_u64_fill() has a new
         prog.


Nits. That bots should stop repoting
====================================

  patch  what
  -----  ---------------------------------------------------------------
  14     flow_merge() takes a double pointer. A plain one is enough.
  15     The comment of bpf_flow_exit(): @st stays on the covered path.
  30     __not_msg() in correlated_regs() has one line in its window.
  31     Leftovers in SHAPE_MANY(), three redundant externs.
  32     Dead 'r7 = r0' in TWO_INNER_MAPS, an unused __imm().
  34     The comment of counts(). RUN_JITED(). loop_in_main() and
         loop_in_main_rcu() leave the loop in the first trip.