[RFC,bpf-next,v2,3/3] selftests/bpf: add more verifier tests for signed range deduction of BPF_AND

Commit Message

Shung-Hsi Yu Nov. 19, 2024, 11:40 a.m. UTC

Add more specific test cases into verifier_and.c to test against signed
range deduction.

WIP, Test failing.
---
The GitHub action is at https://github.com/kernel-patches/bpf/actions/runs/11909088689/

For and_mixed_range_vs_neg_const()

  Error: #432/8 verifier_and/[-1,0] range vs negative constant @unpriv
  ...
  VERIFIER LOG:
  =============
  0: R1=ctx() R10=fp0
  0: (85) call bpf_get_prandom_u32#7    ; R0_w=Pscalar()
  1: (67) r0 <<= 63                     ; R0_w=Pscalar(smax=smax32=umax32=0,umax=0x8000000000000000,smin32=0,var_off=(0x0; 0x8000000000000000))
  2: (c7) r0 s>>= 63                    ; R0_w=Pscalar(smin=smin32=-1,smax=smax32=0)
  3: (b7) r1 = -13                      ; R1_w=P-13
  4: (5f) r0 &= r1                      ; R0_w=Pscalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) R1_w=P-13
  5: (b7) r2 = 0                        ; R2_w=P0
  6: (6d) if r0 s> r2 goto pc+4         ; R0_w=Pscalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) R2_w=P0
  7: (b7) r2 = -16                      ; R2=P-16
  8: (cd) if r0 s< r2 goto pc+2 11: R0=Pscalar() R1=P-13 R2=Pscalar() R10=fp0

	Somehow despite the verifier knows that r0's smin=-16 and smax=0,
	and r2's smin=-16 and smax=-16, it does determine that
	[-16, 0] s< -16 is always false.

  11: (61) r1 = *(u32 *)(r1 +0)
  R1 invalid mem access 'scalar'

Felt like this is something obvious, but I just couldn't see where the
problem lies.

---
 .../selftests/bpf/progs/verifier_and.c        | 56 +++++++++++++++++++
 1 file changed, 56 insertions(+)

Comments

Shung-Hsi Yu Nov. 19, 2024, 11:44 a.m. UTC | #1

On Tue, Nov 19, 2024 at 07:40:21PM GMT, Shung-Hsi Yu wrote:
> Add more specific test cases into verifier_and.c to test against signed
> range deduction.
> 
> WIP, Test failing.
> ---
> The GitHub action is at https://github.com/kernel-patches/bpf/actions/runs/11909088689/
> 
> For and_mixed_range_vs_neg_const()
> 
>   Error: #432/8 verifier_and/[-1,0] range vs negative constant @unpriv
>   ...
>   VERIFIER LOG:
>   =============
>   0: R1=ctx() R10=fp0
>   0: (85) call bpf_get_prandom_u32#7    ; R0_w=Pscalar()
>   1: (67) r0 <<= 63                     ; R0_w=Pscalar(smax=smax32=umax32=0,umax=0x8000000000000000,smin32=0,var_off=(0x0; 0x8000000000000000))
>   2: (c7) r0 s>>= 63                    ; R0_w=Pscalar(smin=smin32=-1,smax=smax32=0)
>   3: (b7) r1 = -13                      ; R1_w=P-13
>   4: (5f) r0 &= r1                      ; R0_w=Pscalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) R1_w=P-13
>   5: (b7) r2 = 0                        ; R2_w=P0
>   6: (6d) if r0 s> r2 goto pc+4         ; R0_w=Pscalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) R2_w=P0
>   7: (b7) r2 = -16                      ; R2=P-16
>   8: (cd) if r0 s< r2 goto pc+2 11: R0=Pscalar() R1=P-13 R2=Pscalar() R10=fp0
> 
> 	Somehow despite the verifier knows that r0's smin=-16 and smax=0,
> 	and r2's smin=-16 and smax=-16, it does determine that
                                typo here  ^ 
                                          not
> 	[-16, 0] s< -16 is always false.
> 
>   11: (61) r1 = *(u32 *)(r1 +0)
>   R1 invalid mem access 'scalar'
> 
> Felt like this is something obvious, but I just couldn't see where the
> problem lies.
...

Patch

diff --git a/tools/testing/selftests/bpf/progs/verifier_and.c b/tools/testing/selftests/bpf/progs/verifier_and.c
index e97e518516b6..56c362f99a21 100644
--- a/tools/testing/selftests/bpf/progs/verifier_and.c
+++ b/tools/testing/selftests/bpf/progs/verifier_and.c
@@ -104,4 +104,60 @@  l0_%=:	r0 = 0;						\
 	: __clobber_all);
 }
 
+SEC("socket")
+__description("[-1,0] range vs negative constant")
+__success __success_unpriv __retval(0)
+__naked void and_mixed_range_vs_neg_const(void)
+{
+	/* Use ARSH with AND like compiler would */
+	asm volatile ("					\
+	call %[bpf_get_prandom_u32];			\
+	r0 <<= 63;					\
+	r0 s>>= 63; /* r0 = [-1, 0] */			\
+	r1 = -13;					\
+	r0 &= r1;					\
+	/* [-1, 0] & -13 give either -13 or 0. So	\
+	 * ideally this should be a tight range of	\
+	 * [-13, 0], but verifier is not advanced enough\
+	 * to deduce that. just knowing result is in	\
+	 * [-16, 0] is good enough.			\
+	 */                                             \
+	r2 = 0;						\
+	if r0 s> r2 goto l0_%=;				\
+	r2 = -16;					\
+	if r0 s< r2 goto l0_%=;				\
+	r0 = 0;						\
+	exit;						\
+l0_%=:  r1 = *(u32*)(r1 + 0);				\
+	exit;						\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("32-bit [-1,0] range vs negative constant")
+__success __success_unpriv __retval(0)
+__naked void and32_mixed_range_vs_neg_const(void)
+{
+	/* See and_mixed_range_vs_neg_const() */
+	asm volatile ("					\
+	call %[bpf_get_prandom_u32];			\
+	w0 <<= 31;					\
+	w0 s>>= 31;					\
+	w1 = -13;					\
+	w0 &= w1;					\
+	w2 = 0;						\
+	if w0 s> w2 goto l0_%=;				\
+	w2 = -16;					\
+	if w0 s< w2 goto l0_%=;				\
+	r0 = 0;						\
+	exit;						\
+l0_%=:  r1 = *(u32*)(r1 + 0);				\
+	exit;						\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
 char _license[] SEC("license") = "GPL";