On Wed, Mar 6, 2024 at 10:33 AM Andrii Nakryiko
<andrii.nakryiko@xxxxxxxxx> wrote:
>
> On Tue, Mar 5, 2024 at 7:19 PM Alexei Starovoitov
> <alexei.starovoitov@xxxxxxxxx> wrote:
> >
> > From: Alexei Starovoitov <ast@xxxxxxxxxx>
> >
> > Introduce may_goto instruction that from the verifier pov is similar to
> > open coded iterators bpf_for()/bpf_repeat() and bpf_loop() helper, but it
> > doesn't iterate any objects.
> > In assembly 'may_goto' is a nop most of the time until bpf runtime has to
> > terminate the program for whatever reason. In the current implementation
> > may_goto has a hidden counter, but other mechanisms can be used.
> > For programs written in C the later patch introduces 'cond_break' macro
> > that combines 'may_goto' with 'break' statement and has similar semantics:
> > cond_break is a nop until bpf runtime has to break out of this loop.
> > It can be used in any normal "for" or "while" loop, like
> >
> > for (i = zero; i < cnt; cond_break, i++) {
> >
> > The verifier recognizes that may_goto is used in the program, reserves
> > additional 8 bytes of stack, initializes them in subprog prologue, and
> > replaces may_goto instruction with:
> > aux_reg = *(u64 *)(fp - 40)
> > if aux_reg == 0 goto pc+off
> > aux_reg -= 1
> > *(u64 *)(fp - 40) = aux_reg
> >
> > may_goto instruction can be used by LLVM to implement __builtin_memcpy,
> > __builtin_strcmp.
> >
> > may_goto is not a full substitute for bpf_for() macro.
> > bpf_for() doesn't have induction variable that verifiers sees,
> > so 'i' in bpf_for(i, 0, 100) is seen as imprecise and bounded.
> >
> > But when the code is written as:
> > for (i = 0; i < 100; cond_break, i++)
> > the verifier see 'i' as precise constant zero,
> > hence cond_break (aka may_goto) doesn't help to converge the loop.
> > A static or global variable can be used as a workaround:
> > static int zero = 0;
> > for (i = zero; i < 100; cond_break, i++) // works!
> >
> > may_goto works well with arena pointers that don't need to be bounds
> > checked on access. Load/store from arena returns imprecise unbounded
> > scalar and loops with may_goto pass the verifier.
> >
> > Reserve new opcode BPF_JMP | BPF_JCOND for may_goto insn.
> > JCOND stands for conditional pseudo jump.
> > Since goto_or_nop insn was proposed, it may use the same opcode.
> > may_goto vs goto_or_nop can be distinguished by src_reg:
> > code = BPF_JMP | BPF_JCOND
> > src_reg = 0 - may_goto
> > src_reg = 1 - goto_or_nop
> >
> > Acked-by: Andrii Nakryiko <andrii@xxxxxxxxxx>
> > Signed-off-by: Alexei Starovoitov <ast@xxxxxxxxxx>
> > ---
> > include/linux/bpf_verifier.h | 2 +
> > include/uapi/linux/bpf.h | 5 +
> > kernel/bpf/core.c | 1 +
> > kernel/bpf/disasm.c | 4 +
> > kernel/bpf/verifier.c | 163 +++++++++++++++++++++++++++------
> > tools/include/uapi/linux/bpf.h | 5 +
> > 6 files changed, 150 insertions(+), 30 deletions(-)
> >
>
> [...]
>
> > @@ -14871,11 +14882,36 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
> > int err;
> >
> > /* Only conditional jumps are expected to reach here. */
> > - if (opcode == BPF_JA || opcode > BPF_JSLE) {
> > + if (opcode == BPF_JA || opcode > BPF_JCOND) {
> > verbose(env, "invalid BPF_JMP/JMP32 opcode %x\n", opcode);
> > return -EINVAL;
> > }
> >
> > + if (opcode == BPF_JCOND) {
> > + struct bpf_verifier_state *cur_st = env->cur_state, *queued_st, *prev_st;
> > + int idx = *insn_idx;
> > +
> > + if (insn->code != (BPF_JMP | BPF_JCOND) ||
> > + insn->src_reg != BPF_MAY_GOTO ||
> > + insn->dst_reg || insn->imm || insn->off == 0) {
>
> Why rejecting insn->off == 0? It's still a legal instruction, even if
> not super useful in practice. insn->off == -1 is also weird, but legal
> (and not rejected in this case).
Legal, but nonsensical.
s390 hits it due to macro endian issue, so it's better to
reject early instead of wasting 1m verifier steps.
