diff mbox series

[bpf-next,v2,1/4] bpf: Improve verifier JEQ/JNE insn branch taken checking

Message ID 20230406164455.1045294-1-yhs@fb.com (mailing list archive)
State Accepted
Commit 13fbcee55706db45ce047a7cea14811d68f94ee3
Delegated to: BPF
Headers show
Series bpf: Improve verifier for cond_op and spilled loop index variables | expand

Checks

Context Check Description
bpf/vmtest-bpf-next-VM_Test-1 success Logs for ShellCheck
bpf/vmtest-bpf-next-VM_Test-7 success Logs for set-matrix
bpf/vmtest-bpf-next-VM_Test-2 success Logs for build for aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-3 success Logs for build for aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-5 success Logs for build for x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-6 success Logs for build for x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-4 success Logs for build for s390x with gcc
bpf/vmtest-bpf-next-VM_Test-25 success Logs for test_progs_no_alu32_parallel on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-26 success Logs for test_progs_no_alu32_parallel on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-31 success Logs for test_verifier on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-34 success Logs for test_verifier on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-35 success Logs for test_verifier on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-8 success Logs for test_maps on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-9 success Logs for test_maps on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-11 success Logs for test_maps on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-12 success Logs for test_maps on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-13 success Logs for test_progs on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-14 success Logs for test_progs on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-16 success Logs for test_progs on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-17 success Logs for test_progs on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-18 success Logs for test_progs_no_alu32 on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-19 success Logs for test_progs_no_alu32 on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-21 success Logs for test_progs_no_alu32 on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-22 success Logs for test_progs_no_alu32 on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-23 success Logs for test_progs_no_alu32_parallel on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-24 success Logs for test_progs_no_alu32_parallel on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-27 success Logs for test_progs_parallel on aarch64 with gcc
bpf/vmtest-bpf-next-VM_Test-28 success Logs for test_progs_parallel on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-29 success Logs for test_progs_parallel on x86_64 with gcc
bpf/vmtest-bpf-next-VM_Test-30 success Logs for test_progs_parallel on x86_64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-32 success Logs for test_verifier on aarch64 with llvm-16
bpf/vmtest-bpf-next-VM_Test-20 success Logs for test_progs_no_alu32 on s390x with gcc
bpf/vmtest-bpf-next-VM_Test-33 success Logs for test_verifier on s390x with gcc
netdev/series_format success Posting correctly formatted
netdev/tree_selection success Clearly marked for bpf-next, async
netdev/fixes_present success Fixes tag not required for -next series
netdev/header_inline success No static functions without inline keyword in header files
netdev/build_32bit success Errors and warnings before: 28 this patch: 28
netdev/cc_maintainers warning 11 maintainers not CCed: song@kernel.org sdf@google.com haoluo@google.com kuba@kernel.org john.fastabend@gmail.com kpsingh@kernel.org jolsa@kernel.org hawk@kernel.org netdev@vger.kernel.org martin.lau@linux.dev davem@davemloft.net
netdev/build_clang success Errors and warnings before: 18 this patch: 18
netdev/verify_signedoff success Signed-off-by tag matches author and committer
netdev/deprecated_api success None detected
netdev/check_selftest success No net selftest shell script
netdev/verify_fixes success No Fixes tag
netdev/build_allmodconfig_warn success Errors and warnings before: 28 this patch: 28
netdev/checkpatch success total: 0 errors, 0 warnings, 0 checks, 28 lines checked
netdev/kdoc success Errors and warnings before: 0 this patch: 0
netdev/source_inline success Was 0 now: 0
bpf/vmtest-bpf-next-VM_Test-15 fail Logs for test_progs on s390x with gcc
bpf/vmtest-bpf-next-PR fail PR summary
bpf/vmtest-bpf-next-VM_Test-10 success Logs for test_maps on s390x with gcc

Commit Message

Yonghong Song April 6, 2023, 4:44 p.m. UTC 
Currently, for BPF_JEQ/BPF_JNE insn, verifier determines
whether the branch is taken or not only if both operands
are constants. Therefore, for the following code snippet,
  0: (85) call bpf_ktime_get_ns#5       ; R0_w=scalar()
  1: (a5) if r0 < 0x3 goto pc+2         ; R0_w=scalar(umin=3)
  2: (b7) r2 = 2                        ; R2_w=2
  3: (1d) if r0 == r2 goto pc+2 6

At insn 3, since r0 is not a constant, verifier assumes both branch
can be taken which may lead inproper verification failure.

Add comparing umin/umax value and the constant. If the umin value
is greater than the constant, or umax value is smaller than the constant,
for JEQ the branch must be not-taken, and for JNE the branch must be taken.
The jmp32 mode JEQ/JNE branch taken checking is also handled similarly.

The following lists the veristat result w.r.t. changed number
of processes insns during verification:

File                                                   Program                                               Insns (A)  Insns (B)  Insns    (DIFF)
-----------------------------------------------------  ----------------------------------------------------  ---------  ---------  ---------------
test_cls_redirect.bpf.linked3.o                        cls_redirect                                              64980      73472  +8492 (+13.07%)
test_seg6_loop.bpf.linked3.o                           __add_egr_x                                               12425      12423      -2 (-0.02%)
test_tcp_hdr_options.bpf.linked3.o                     estab                                                      2634       2558     -76 (-2.89%)
test_parse_tcp_hdr_opt.bpf.linked3.o                   xdp_ingress_v6                                             1421       1420      -1 (-0.07%)
test_parse_tcp_hdr_opt_dynptr.bpf.linked3.o            xdp_ingress_v6                                             1238       1237      -1 (-0.08%)
test_tc_dtime.bpf.linked3.o                            egress_fwdns_prio100                                        414        411      -3 (-0.72%)

Mostly a small improvement but test_cls_redirect.bpf.linked3.o has a 13% regression.
I checked with verifier log and found it this is due to pruning.
For some JEQ/JNE branches impacted by this patch,
one branch is explored and the other has state equivalence and
pruned.

Signed-off-by: Yonghong Song <yhs@fb.com>
---
 kernel/bpf/verifier.c | 8 ++++++++
 1 file changed, 8 insertions(+)

Comments

Dave Marchevsky April 6, 2023, 5:49 p.m. UTC | #1 
On 4/6/23 12:44 PM, Yonghong Song wrote:
> Currently, for BPF_JEQ/BPF_JNE insn, verifier determines
> whether the branch is taken or not only if both operands
> are constants. Therefore, for the following code snippet,
>   0: (85) call bpf_ktime_get_ns#5       ; R0_w=scalar()
>   1: (a5) if r0 < 0x3 goto pc+2         ; R0_w=scalar(umin=3)
>   2: (b7) r2 = 2                        ; R2_w=2
>   3: (1d) if r0 == r2 goto pc+2 6
> 
> At insn 3, since r0 is not a constant, verifier assumes both branch
> can be taken which may lead inproper verification failure.
> 
> Add comparing umin/umax value and the constant. If the umin value
> is greater than the constant, or umax value is smaller than the constant,
> for JEQ the branch must be not-taken, and for JNE the branch must be taken.
> The jmp32 mode JEQ/JNE branch taken checking is also handled similarly.
> 
> The following lists the veristat result w.r.t. changed number
> of processes insns during verification:
> 
> File                                                   Program                                               Insns (A)  Insns (B)  Insns    (DIFF)
> -----------------------------------------------------  ----------------------------------------------------  ---------  ---------  ---------------
> test_cls_redirect.bpf.linked3.o                        cls_redirect                                              64980      73472  +8492 (+13.07%)
> test_seg6_loop.bpf.linked3.o                           __add_egr_x                                               12425      12423      -2 (-0.02%)
> test_tcp_hdr_options.bpf.linked3.o                     estab                                                      2634       2558     -76 (-2.89%)
> test_parse_tcp_hdr_opt.bpf.linked3.o                   xdp_ingress_v6                                             1421       1420      -1 (-0.07%)
> test_parse_tcp_hdr_opt_dynptr.bpf.linked3.o            xdp_ingress_v6                                             1238       1237      -1 (-0.08%)
> test_tc_dtime.bpf.linked3.o                            egress_fwdns_prio100                                        414        411      -3 (-0.72%)
> 
> Mostly a small improvement but test_cls_redirect.bpf.linked3.o has a 13% regression.
> I checked with verifier log and found it this is due to pruning.
> For some JEQ/JNE branches impacted by this patch,
> one branch is explored and the other has state equivalence and
> pruned.

Can you elaborate a bit on this insn increase caused by pruning?

My naive reading of this: there was some state exploration that was
previously pruned due to is_branch_taken returning indeterminate
value (-1), and now that it can concretely say branch is/isn't taken,
states which would've been considered equivalent no longer are.
Is that accurate?

> 
> Signed-off-by: Yonghong Song <yhs@fb.com>
> ---

Regardless,

Acked-by: Dave Marchevsky <davemarchevsky@fb.com>
Alexei Starovoitov April 6, 2023, 8:03 p.m. UTC | #2 
On Thu, Apr 6, 2023 at 10:49 AM Dave Marchevsky <davemarchevsky@meta.com> wrote:
>
>
>
> On 4/6/23 12:44 PM, Yonghong Song wrote:
> > Currently, for BPF_JEQ/BPF_JNE insn, verifier determines
> > whether the branch is taken or not only if both operands
> > are constants. Therefore, for the following code snippet,
> >   0: (85) call bpf_ktime_get_ns#5       ; R0_w=scalar()
> >   1: (a5) if r0 < 0x3 goto pc+2         ; R0_w=scalar(umin=3)
> >   2: (b7) r2 = 2                        ; R2_w=2
> >   3: (1d) if r0 == r2 goto pc+2 6
> >
> > At insn 3, since r0 is not a constant, verifier assumes both branch
> > can be taken which may lead inproper verification failure.
> >
> > Add comparing umin/umax value and the constant. If the umin value
> > is greater than the constant, or umax value is smaller than the constant,
> > for JEQ the branch must be not-taken, and for JNE the branch must be taken.
> > The jmp32 mode JEQ/JNE branch taken checking is also handled similarly.
> >
> > The following lists the veristat result w.r.t. changed number
> > of processes insns during verification:
> >
> > File                                                   Program                                               Insns (A)  Insns (B)  Insns    (DIFF)
> > -----------------------------------------------------  ----------------------------------------------------  ---------  ---------  ---------------
> > test_cls_redirect.bpf.linked3.o                        cls_redirect                                              64980      73472  +8492 (+13.07%)
> > test_seg6_loop.bpf.linked3.o                           __add_egr_x                                               12425      12423      -2 (-0.02%)
> > test_tcp_hdr_options.bpf.linked3.o                     estab                                                      2634       2558     -76 (-2.89%)
> > test_parse_tcp_hdr_opt.bpf.linked3.o                   xdp_ingress_v6                                             1421       1420      -1 (-0.07%)
> > test_parse_tcp_hdr_opt_dynptr.bpf.linked3.o            xdp_ingress_v6                                             1238       1237      -1 (-0.08%)
> > test_tc_dtime.bpf.linked3.o                            egress_fwdns_prio100                                        414        411      -3 (-0.72%)
> >
> > Mostly a small improvement but test_cls_redirect.bpf.linked3.o has a 13% regression.
> > I checked with verifier log and found it this is due to pruning.
> > For some JEQ/JNE branches impacted by this patch,
> > one branch is explored and the other has state equivalence and
> > pruned.
>
> Can you elaborate a bit on this insn increase caused by pruning?
>
> My naive reading of this: there was some state exploration that was
> previously pruned due to is_branch_taken returning indeterminate
> value (-1), and now that it can concretely say branch is/isn't taken,
> states which would've been considered equivalent no longer are.
> Is that accurate?

Pretty much. It's because when is_branch_taken() is certain on the direction
of the branch it marks register as precise and it hurts state equivalence
later.

>
> >
> > Signed-off-by: Yonghong Song <yhs@fb.com>
> > ---
>
> Regardless,
>
> Acked-by: Dave Marchevsky <davemarchevsky@fb.com>
Andrii Nakryiko April 6, 2023, 8:35 p.m. UTC | #3 
On Thu, Apr 6, 2023 at 9:45 AM Yonghong Song <yhs@fb.com> wrote:
>
> Currently, for BPF_JEQ/BPF_JNE insn, verifier determines
> whether the branch is taken or not only if both operands
> are constants. Therefore, for the following code snippet,
>   0: (85) call bpf_ktime_get_ns#5       ; R0_w=scalar()
>   1: (a5) if r0 < 0x3 goto pc+2         ; R0_w=scalar(umin=3)
>   2: (b7) r2 = 2                        ; R2_w=2
>   3: (1d) if r0 == r2 goto pc+2 6
>
> At insn 3, since r0 is not a constant, verifier assumes both branch
> can be taken which may lead inproper verification failure.
>
> Add comparing umin/umax value and the constant. If the umin value
> is greater than the constant, or umax value is smaller than the constant,
> for JEQ the branch must be not-taken, and for JNE the branch must be taken.
> The jmp32 mode JEQ/JNE branch taken checking is also handled similarly.
>
> The following lists the veristat result w.r.t. changed number
> of processes insns during verification:
>
> File                                                   Program                                               Insns (A)  Insns (B)  Insns    (DIFF)
> -----------------------------------------------------  ----------------------------------------------------  ---------  ---------  ---------------
> test_cls_redirect.bpf.linked3.o                        cls_redirect                                              64980      73472  +8492 (+13.07%)
> test_seg6_loop.bpf.linked3.o                           __add_egr_x                                               12425      12423      -2 (-0.02%)
> test_tcp_hdr_options.bpf.linked3.o                     estab                                                      2634       2558     -76 (-2.89%)
> test_parse_tcp_hdr_opt.bpf.linked3.o                   xdp_ingress_v6                                             1421       1420      -1 (-0.07%)
> test_parse_tcp_hdr_opt_dynptr.bpf.linked3.o            xdp_ingress_v6                                             1238       1237      -1 (-0.08%)
> test_tc_dtime.bpf.linked3.o                            egress_fwdns_prio100                                        414        411      -3 (-0.72%)
>
> Mostly a small improvement but test_cls_redirect.bpf.linked3.o has a 13% regression.
> I checked with verifier log and found it this is due to pruning.
> For some JEQ/JNE branches impacted by this patch,
> one branch is explored and the other has state equivalence and
> pruned.
>
> Signed-off-by: Yonghong Song <yhs@fb.com>
> ---

LGTM.

Acked-by: Andrii Nakryiko <andrii@kernel.org>

>  kernel/bpf/verifier.c | 8 ++++++++
>  1 file changed, 8 insertions(+)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 56f569811f70..5c6b90e384a5 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -12651,10 +12651,14 @@ static int is_branch32_taken(struct bpf_reg_state *reg, u32 val, u8 opcode)
>         case BPF_JEQ:
>                 if (tnum_is_const(subreg))
>                         return !!tnum_equals_const(subreg, val);
> +               else if (val < reg->u32_min_value || val > reg->u32_max_value)
> +                       return 0;
>                 break;
>         case BPF_JNE:
>                 if (tnum_is_const(subreg))
>                         return !tnum_equals_const(subreg, val);
> +               else if (val < reg->u32_min_value || val > reg->u32_max_value)
> +                       return 1;
>                 break;
>         case BPF_JSET:
>                 if ((~subreg.mask & subreg.value) & val)
> @@ -12724,10 +12728,14 @@ static int is_branch64_taken(struct bpf_reg_state *reg, u64 val, u8 opcode)
>         case BPF_JEQ:
>                 if (tnum_is_const(reg->var_off))
>                         return !!tnum_equals_const(reg->var_off, val);
> +               else if (val < reg->umin_value || val > reg->umax_value)
> +                       return 0;
>                 break;
>         case BPF_JNE:
>                 if (tnum_is_const(reg->var_off))
>                         return !tnum_equals_const(reg->var_off, val);
> +               else if (val < reg->umin_value || val > reg->umax_value)
> +                       return 1;
>                 break;
>         case BPF_JSET:
>                 if ((~reg->var_off.mask & reg->var_off.value) & val)
> --
> 2.34.1
>
diff mbox series

Patch

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 56f569811f70..5c6b90e384a5 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -12651,10 +12651,14 @@  static int is_branch32_taken(struct bpf_reg_state *reg, u32 val, u8 opcode)
 	case BPF_JEQ:
 		if (tnum_is_const(subreg))
 			return !!tnum_equals_const(subreg, val);
+		else if (val < reg->u32_min_value || val > reg->u32_max_value)
+			return 0;
 		break;
 	case BPF_JNE:
 		if (tnum_is_const(subreg))
 			return !tnum_equals_const(subreg, val);
+		else if (val < reg->u32_min_value || val > reg->u32_max_value)
+			return 1;
 		break;
 	case BPF_JSET:
 		if ((~subreg.mask & subreg.value) & val)
@@ -12724,10 +12728,14 @@  static int is_branch64_taken(struct bpf_reg_state *reg, u64 val, u8 opcode)
 	case BPF_JEQ:
 		if (tnum_is_const(reg->var_off))
 			return !!tnum_equals_const(reg->var_off, val);
+		else if (val < reg->umin_value || val > reg->umax_value)
+			return 0;
 		break;
 	case BPF_JNE:
 		if (tnum_is_const(reg->var_off))
 			return !tnum_equals_const(reg->var_off, val);
+		else if (val < reg->umin_value || val > reg->umax_value)
+			return 1;
 		break;
 	case BPF_JSET:
 		if ((~reg->var_off.mask & reg->var_off.value) & val)