From: Xu Kuohai <redacted>
A bpf prog returning a positive number attached to file_alloc_security
hook makes kernel panic.
This happens because file system can not filter out the positive number
returned by the LSM prog using IS_ERR, and misinterprets this positive
number as a file pointer.
Given that hook file_alloc_security never returned positive number
before the introduction of BPF LSM, and other BPF LSM hooks may
encounter similar issues, this patch adds LSM return value check
in verifier, to ensure no unexpected value is returned.
Fixes: 520b7aa00d8c ("bpf: lsm: Initialize the BPF LSM hooks")
Reported-by: Xin Liu <redacted>
Signed-off-by: Xu Kuohai <redacted>
Acked-by: Eduard Zingerman <eddyz87@gmail.com>
---
include/linux/bpf.h | 1 +
include/linux/bpf_lsm.h | 9 +++++++
kernel/bpf/bpf_lsm.c | 30 ++++++++++++++++++++-
kernel/bpf/btf.c | 5 +++-
kernel/bpf/verifier.c | 60 ++++++++++++++++++++++++++++++++++-------
5 files changed, 94 insertions(+), 11 deletions(-)
@@ -927,6 +927,7 @@ struct bpf_insn_access_aux {};};structbpf_verifier_log*log;/* for verbose logs */+boolis_retval;/* is accessing function return value ? */};staticinlinevoid
@@ -420,3 +419,32 @@ bool bpf_lsm_has_retval_param(const struct bpf_prog *prog)returnbtf_id_set_contains(&retval_param_lsm_hooks,prog->aux->attach_btf_id);}++/* hooks return 0 or 1 */+BTF_SET_START(bool_lsm_hooks)+BTF_ID(func,bpf_lsm_xfrm_state_pol_flow_match)+BTF_ID(func,bpf_lsm_audit_rule_known)+BTF_ID(func,bpf_lsm_inode_xattr_skipcap)+BTF_SET_END(bool_lsm_hooks)++intbpf_lsm_get_retval_range(conststructbpf_prog*prog,+structbpf_retval_range*retval_range)+{+/* no return value range for void hooks */+if(!prog->aux->attach_func_proto->type)+return-EINVAL;++if(btf_id_set_contains(&bool_lsm_hooks,prog->aux->attach_btf_id)){+retval_range->minval=0;+retval_range->maxval=1;+}else{+/* All other LSM hooks, except task_prctl, return 0 on success+*andnegativeerrorcodeonfailure.+*Tokeepthingssimple,weonlyallowbpfprogstoreturn0+*ornegativeerrnofortask_prctl.+*/+retval_range->minval=-MAX_ERRNO;+retval_range->maxval=0;+}+return0;+}
@@ -6416,8 +6416,11 @@ bool btf_ctx_access(int off, int size, enum bpf_access_type type,if(arg==nr_args){switch(prog->expected_attach_type){-caseBPF_LSM_CGROUP:caseBPF_LSM_MAC:+/* mark we are accessing the return value */+info->is_retval=true;+fallthrough;+caseBPF_LSM_CGROUP:caseBPF_TRACE_FEXIT:/* When LSM programs are attached to void LSM hooks*theyuseFEXITtrampolinesandwhenattachedto
@@ -5587,11 +5606,12 @@ static int check_packet_access(struct bpf_verifier_env *env, u32 regno, int off,/* check access to 'struct bpf_context' fields. Supports fixed offsets only */staticintcheck_ctx_access(structbpf_verifier_env*env,intinsn_idx,intoff,intsize,enumbpf_access_typet,enumbpf_reg_type*reg_type,-structbtf**btf,u32*btf_id)+structbtf**btf,u32*btf_id,bool*is_retval){structbpf_insn_access_auxinfo={.reg_type=*reg_type,.log=&env->log,+.is_retval=false,};if(env->ops->is_valid_access&&
@@ -5604,6 +5624,7 @@ static int check_ctx_access(struct bpf_verifier_env *env, int insn_idx, int off,*typeofnarroweraccess.*/*reg_type=info.reg_type;+*is_retval=info.is_retval;if(base_type(*reg_type)==PTR_TO_BTF_ID){*btf=info.btf;
@@ -6803,6 +6824,17 @@ static int check_stack_access_within_bounds(returngrow_stack_state(env,state,-min_off/* size */);}+staticboolget_func_retval_range(structbpf_prog*prog,+structbpf_retval_range*range)+{+if(prog->type==BPF_PROG_TYPE_LSM&&+prog->expected_attach_type==BPF_LSM_MAC&&+!bpf_lsm_get_retval_range(prog,range)){+returntrue;+}+returnfalse;+}+/* check whether memory at (regno + off) is accessible for t = (read | write)*ift==write,value_regnoisaregisterwhichvalueisstoredintomemory*ift==read,value_regnoisaregisterwhichwillreceivethevaluefrommemory
@@ -6907,6 +6939,8 @@ static int check_mem_access(struct bpf_verifier_env *env, int insn_idx, u32 regnif(!err&&value_regno>=0&&(t==BPF_READ||rdonly_mem))mark_reg_unknown(env,regs,value_regno);}elseif(reg->type==PTR_TO_CTX){+boolis_retval=false;+structbpf_retval_rangerange;enumbpf_reg_typereg_type=SCALAR_VALUE;structbtf*btf=NULL;u32btf_id=0;
@@ -6922,7 +6956,7 @@ static int check_mem_access(struct bpf_verifier_env *env, int insn_idx, u32 regnreturnerr;err=check_ctx_access(env,insn_idx,off,size,t,®_type,&btf,-&btf_id);+&btf_id,&is_retval);if(err)verbose_linfo(env,insn_idx,"; ");if(!err&&t==BPF_READ&&value_regno>=0){
@@ -6931,7 +6965,14 @@ static int check_mem_access(struct bpf_verifier_env *env, int insn_idx, u32 regn*case,weknowtheoffsetiszero.*/if(reg_type==SCALAR_VALUE){-mark_reg_unknown(env,regs,value_regno);+if(is_retval&&get_func_retval_range(env->prog,&range)){+err=__mark_reg_s32_range(env,regs,value_regno,+range.minval,range.maxval);+if(err)+returnerr;+}else{+mark_reg_unknown(env,regs,value_regno);+}}else{mark_reg_known_zero(env,regs,value_regno);
@@ -15782,12 +15823,13 @@ static int check_return_code(struct bpf_verifier_env *env, int regno, const charcaseBPF_PROG_TYPE_LSM:if(env->prog->expected_attach_type!=BPF_LSM_CGROUP){-/* Regular BPF_PROG_TYPE_LSM programs can return-*anyvalue.-*/-return0;-}-if(!env->prog->aux->attach_func_proto->type){+/* no range found, any return value is allowed */+if(!get_func_retval_range(env->prog,&range))+return0;+/* no restricted range, any return value is allowed */+if(range.minval==S32_MIN&&range.maxval==S32_MAX)+return0;+}elseif(!env->prog->aux->attach_func_proto->type){/* Make sure programs that attach to void*hooksdon'ttrytomodifyreturnvalue.*/
From: Xu Kuohai <redacted>
After checking lsm hook return range in verifier, the test case
"test_progs -t test_lsm" failed, and the failure log says:
libbpf: prog 'test_int_hook': BPF program load failed: Invalid argument
libbpf: prog 'test_int_hook': -- BEGIN PROG LOAD LOG --
0: R1=ctx() R10=fp0
; int BPF_PROG(test_int_hook, struct vm_area_struct *vma, @ lsm.c:89
0: (79) r0 = *(u64 *)(r1 +24) ; R0_w=scalar(smin=smin32=-4095,smax=smax32=0) R1=ctx()
[...]
24: (b4) w0 = -1 ; R0_w=0xffffffff
; int BPF_PROG(test_int_hook, struct vm_area_struct *vma, @ lsm.c:89
25: (95) exit
At program exit the register R0 has smin=4294967295 smax=4294967295 should have been in [-4095, 0]
It can be seen that instruction "w0 = -1" zero extended -1 to 64-bit
register r0, setting both smin and smax values of r0 to 4294967295.
This resulted in a false reject when r0 was checked with range [-4095, 0].
Given bpf lsm does not return 64-bit values, this patch fixes it by changing
the compare between r0 and return range from 64-bit operation to 32-bit
operation for bpf lsm.
Fixes: 8fa4ecd49b81 ("bpf: enforce exact retval range on subprog/callback exit")
Signed-off-by: Xu Kuohai <redacted>
Acked-by: Shung-Hsi Yu <redacted>
---
kernel/bpf/verifier.c | 16 +++++++++++-----
1 file changed, 11 insertions(+), 5 deletions(-)
@@ -10034,8 +10038,8 @@ static int prepare_func_exit(struct bpf_verifier_env *env, int *insn_idx)if(err)returnerr;-/* enforce R0 return value range */-if(!retval_range_within(callee->callback_ret_range,r0)){+/* enforce R0 return value range, and bpf_callback_t returns 64bit */+if(!retval_range_within(callee->callback_ret_range,r0,false)){verbose_invalid_scalar(env,r0,callee->callback_ret_range,"At callback return","R0");return-EINVAL;
@@ -15718,6 +15722,7 @@ static int check_return_code(struct bpf_verifier_env *env, int regno, const charinterr;structbpf_func_state*frame=env->cur_state->frame[0];constboolis_subprog=frame->subprogno;+boolreturn_32bit=false;/* LSM and struct_ops func-ptr's return type could be "void" */if(!is_subprog||frame->in_exception_callback_fn){
@@ -15829,6 +15834,7 @@ static int check_return_code(struct bpf_verifier_env *env, int regno, const char/* no restricted range, any return value is allowed */if(range.minval==S32_MIN&&range.maxval==S32_MAX)return0;+return_32bit=true;}elseif(!env->prog->aux->attach_func_proto->type){/* Make sure programs that attach to void*hooksdon'ttrytomodifyreturnvalue.
@@ -15859,7 +15865,7 @@ static int check_return_code(struct bpf_verifier_env *env, int regno, const charif(err)returnerr;-if(!retval_range_within(range,reg)){+if(!retval_range_within(range,reg,return_32bit)){verbose_invalid_scalar(env,reg,range,exit_ctx,reg_name);if(!is_subprog&&prog->expected_attach_type==BPF_LSM_CGROUP&&
From: Xu Kuohai <redacted>
bpf progs can be attached to kernel functions, and the attached functions
can take different parameters or return different return values. If
prog attached to one kernel function tail calls prog attached to another
kernel function, the ctx access or return value verification could be
bypassed.
For example, if prog1 is attached to func1 which takes only 1 parameter
and prog2 is attached to func2 which takes two parameters. Since verifier
assumes the bpf ctx passed to prog2 is constructed based on func2's
prototype, verifier allows prog2 to access the second parameter from
the bpf ctx passed to it. The problem is that verifier does not prevent
prog1 from passing its bpf ctx to prog2 via tail call. In this case,
the bpf ctx passed to prog2 is constructed from func1 instead of func2,
that is, the assumption for ctx access verification is bypassed.
Another example, if BPF LSM prog1 is attached to hook file_alloc_security,
and BPF LSM prog2 is attached to hook bpf_lsm_audit_rule_known. Verifier
knows the return value rules for these two hooks, e.g. it is legal for
bpf_lsm_audit_rule_known to return positive number 1, and it is illegal
for file_alloc_security to return positive number. So verifier allows
prog2 to return positive number 1, but does not allow prog1 to return
positive number. The problem is that verifier does not prevent prog1
from calling prog2 via tail call. In this case, prog2's return value 1
will be used as the return value for prog1's hook file_alloc_security.
That is, the return value rule is bypassed.
This patch adds restriction for tail call to prevent such bypasses.
Signed-off-by: Xu Kuohai <redacted>
---
include/linux/bpf.h | 1 +
kernel/bpf/core.c | 21 ++++++++++++++++++---
2 files changed, 19 insertions(+), 3 deletions(-)
From: Xu Kuohai <redacted>
With lsm return value check, the no-alu32 version test_libbpf_get_fd_by_id_opts
is rejected by the verifier, and the log says:
0: R1=ctx() R10=fp0
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
0: (b7) r0 = 0 ; R0_w=0
1: (79) r2 = *(u64 *)(r1 +0)
func 'bpf_lsm_bpf_map' arg0 has btf_id 916 type STRUCT 'bpf_map'
2: R1=ctx() R2_w=trusted_ptr_bpf_map()
; if (map != (struct bpf_map *)&data_input) @ test_libbpf_get_fd_by_id_opts.c:29
2: (18) r3 = 0xffff9742c0951a00 ; R3_w=map_ptr(map=data_input,ks=4,vs=4)
4: (5d) if r2 != r3 goto pc+4 ; R2_w=trusted_ptr_bpf_map() R3_w=map_ptr(map=data_input,ks=4,vs=4)
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
5: (79) r0 = *(u64 *)(r1 +8) ; R0_w=scalar() R1=ctx()
; if (fmode & FMODE_WRITE) @ test_libbpf_get_fd_by_id_opts.c:32
6: (67) r0 <<= 62 ; R0_w=scalar(smax=0x4000000000000000,umax=0xc000000000000000,smin32=0,smax32=umax32=0,var_off=(0x0; 0xc000000000000000))
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
; @ test_libbpf_get_fd_by_id_opts.c:0
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
9: (95) exit
And here is the C code of the prog.
SEC("lsm/bpf_map")
int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode)
{
if (map != (struct bpf_map *)&data_input)
return 0;
if (fmode & FMODE_WRITE)
return -EACCES;
return 0;
}
It is clear that the prog can only return either 0 or -EACCESS, and both
values are legal.
So why is it rejected by the verifier?
The verifier log shows that the second if and return value setting
statements in the prog is optimized to bitwise operations "r0 s>>= 63"
and "r0 &= -13". The verifier correctly deduces that the value of
r0 is in the range [-1, 0] after verifing instruction "r0 s>>= 63".
But when the verifier proceeds to verify instruction "r0 &= -13", it
fails to deduce the correct value range of r0.
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
So why the verifier fails to deduce the result of 'r0 &= -13'?
The verifier uses tnum to track values, and the two ranges "[-1, 0]" and
"[0, -1ULL]" are encoded to the same tnum. When verifing instruction
"r0 &= -13", the verifier erroneously deduces the result from
"[0, -1ULL] AND -13", which is out of the expected return range
[-4095, 0].
As explained by Eduard in [0], the clang transformation that generates this
pattern is located in DAGCombiner::SimplifySelectCC() method (see [1]).
The transformation happens as a part of DAG to DAG rewrites
(LLVM uses several internal representations:
- generic optimizer uses LLVM IR, most of the work is done
using this representation;
- before instruction selection IR is converted to Selection DAG,
some optimizations are applied at this stage,
all such optimizations are a set of pattern replacements;
- Selection DAG is converted to machine code, some optimizations
are applied at the machine code level).
Full pattern is described as follows:
// fold (select_cc seteq (and x, y), 0, 0, A) -> (and (sra (shl x)) A)
// where y is has a single bit set.
// A plaintext description would be, we can turn the SELECT_CC into an AND
// when the condition can be materialized as an all-ones register. Any
// single bit-test can be materialized as an all-ones register with
// shift-left and shift-right-arith.
For this particular test case the DAG is converted as follows:
.---------------- lhs The meaning of this select_cc is:
| .------- rhs `lhs == rhs ? true value : false value`
| | .----- true value
| | | .-- false value
v v v v
(select_cc seteq (and X 2) 0 0 -13)
^
-> '---------------.
(and (sra (sll X 62) 63) |
-13) |
|
Before pattern is applied, it checks that second 'and' operand has
only one bit set, (which is true for '2').
The pattern itself generates logical shift left / arithmetic shift
right pair, that ensures that result is either all ones (-1) or all
zeros (0). Hence, applying 'and' to shifts result and false value
generates a correct result.
As suggested by Eduard and Andrii, this patch makes a special case
for source or destination register of '&=' operation being in
range [-1, 0].
Meaning that one of the '&=' operands is either:
- all ones, in which case the counterpart is the result of the operation;
- all zeros, in which case zero is the result of the operation.
That is, the result is equivalent to adding 0 to the counterpart. And MIN
and MAX values could be deduced based on these observations.
[0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/
[1] https://github.com/llvm/llvm-project/blob/4523a267829c807f3fc8fab8e5e9613985a51565/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp
Suggested-by: Eduard Zingerman <eddyz87@gmail.com>
Suggested-by: Andrii Nakryiko <andrii@kernel.org>
Signed-off-by: Xu Kuohai <redacted>
---
include/linux/tnum.h | 3 ++
kernel/bpf/tnum.c | 25 +++++++++++++++++
kernel/bpf/verifier.c | 64 +++++++++++++++++++++++++++++++++++++++++++
3 files changed, 92 insertions(+)
@@ -52,6 +52,9 @@ struct tnum tnum_mul(struct tnum a, struct tnum b);/* Return a tnum representing numbers satisfying both @a and @b */structtnumtnum_intersect(structtnuma,structtnumb);+/* Return a tnum representing numbers satisfying either @a or @b */+structtnumtnum_union(structtnuma,structtnumb);+/* Return @a with all but the lowest @size bytes cleared */structtnumtnum_cast(structtnuma,u8size);
@@ -150,6 +150,31 @@ struct tnum tnum_intersect(struct tnum a, struct tnum b)returnTNUM(v&~mu,mu);}+/* Each bit has 3 states: unknown, known 0, known 1. Using x to represent+*unknownstate,theresultoftheunionoftwobitsisasfollows:+*+*|x01+*-----+------------+*x|xxx+*0|x0x+*1|xx1+*+*Fortnumaandb,onlythebitsthatarebothknown0orknown1ina+*andbareknownintheresultofunionaandb.+*/+structtnumtnum_union(structtnuma,structtnumb)+{+u64v0,v1,mu;++/* unknown bits either in a or b */+mu=a.mask|b.mask;+/* "known 1" bits in both a and b */+v1=(a.value&b.value)&~mu;+/* "known 0" bits in both a and b */+v0=(~a.value&~b.value)&~mu;+returnTNUM(v1,~(v0|v1));+}+structtnumtnum_cast(structtnuma,u8size){a.value&=(1ULL<<(size*8))-1;
@@ -13632,6 +13632,39 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,return;}+/* special case: dst_reg is in range [-1, 0] */+if(dst_reg->s32_min_value==-1&&dst_reg->s32_max_value==0){+/* the result is equivalent to adding 0 to src_reg */+var32_off=tnum_union(src_reg->var_off,tnum_const(0));+dst_reg->var_off=tnum_with_subreg(dst_reg->var_off,var32_off);+/* update signed min/max to include 0 */+dst_reg->s32_min_value=min_t(s32,src_reg->s32_min_value,0);+dst_reg->s32_max_value=max_t(s32,src_reg->s32_max_value,0);+/* since we're adding 0 to src_reg and 0 is the smallest+*unsignedinteger,dst_reg->u32_min_valueshouldbe0,+*anddst->u32_max_valueshouldbesrc_reg->u32_max_value.+*/+dst_reg->u32_min_value=0;+dst_reg->u32_max_value=src_reg->u32_max_value;+return;+}++/* special case: src_reg is in range [-1, 0] */+if(src_reg->s32_min_value==-1&&src_reg->s32_max_value==0){+/* the result is equivalent to adding 0 to dst_reg */+var32_off=tnum_union(dst_reg->var_off,tnum_const(0));+dst_reg->var_off=tnum_with_subreg(dst_reg->var_off,var32_off);+/* update signed min/max to include 0 */+dst_reg->s32_min_value=min_t(s32,dst_reg->s32_min_value,0);+dst_reg->s32_max_value=max_t(s32,dst_reg->s32_max_value,0);+/* since we're adding 0 to dst_reg and 0 is the smallest+*unsignedinteger,dst_reg->u32_min_valueshouldbe0,+*anddst->u32_max_valueshouldremainunchanged.+*/+dst_reg->u32_min_value=0;+return;+}+/* We get our minimum from the var_off, since that's inherently*bitwise.Ourmaximumistheminimumoftheoperands'maxima.*/
@@ -13662,6 +13695,37 @@ static void scalar_min_max_and(struct bpf_reg_state *dst_reg,return;}+/* special case: dst_reg is in range [-1, 0] */+if(dst_reg->smin_value==-1&&dst_reg->smax_value==0){+/* the result is equivalent to adding 0 to src_reg */+dst_reg->var_off=tnum_union(src_reg->var_off,tnum_const(0));+/* update signed min/max to include 0 */+dst_reg->smin_value=min_t(s64,src_reg->smin_value,0);+dst_reg->smax_value=max_t(s64,src_reg->smax_value,0);+/* since we're adding 0 to src_reg and 0 is the smallest+*unsignedinteger,dst_reg->umin_valueshouldbe0,+*anddst->umax_valueshouldbesrc_reg->umax_value.+*/+dst_reg->umin_value=0;+dst_reg->umax_value=src_reg->umax_value;+return;+}++/* special case: src_reg is in range [-1, 0] */+if(src_reg->smin_value==-1&&src_reg->smax_value==0){+/* the result is equivalent to adding 0 to dst_reg */+dst_reg->var_off=tnum_union(dst_reg->var_off,tnum_const(0));+/* update signed min/max to include 0 */+dst_reg->smin_value=min_t(s64,dst_reg->smin_value,0);+dst_reg->smax_value=max_t(s64,dst_reg->smax_value,0);+/* since we're adding 0 to dst_reg and 0 is the smallest+*unsignedinteger,dst_reg->min_valueshouldbe0,+*anddst->umax_valueshouldremainunchanged.+*/+dst_reg->umin_value=0;+return;+}+/* We get our minimum from the var_off, since that's inherently*bitwise.Ourmaximumistheminimumoftheoperands'maxima.*/
From: Xu Kuohai <redacted>
The return ranges of some bpf lsm test progs can not be deduced by
the verifier accurately. To avoid erroneous rejections, add explicit
return value checks for these progs.
Signed-off-by: Xu Kuohai <redacted>
---
tools/testing/selftests/bpf/progs/err.h | 10 ++++++++++
tools/testing/selftests/bpf/progs/test_sig_in_xattr.c | 4 ++++
.../selftests/bpf/progs/test_verify_pkcs7_sig.c | 8 ++++++--
.../selftests/bpf/progs/verifier_global_subprogs.c | 7 ++++++-
4 files changed, 26 insertions(+), 3 deletions(-)
@@ -55,12 +56,12 @@ int BPF_PROG(bpf, int cmd, union bpf_attr *attr, unsigned int size)ret=bpf_probe_read_kernel(&value,sizeof(value),&attr->value);if(ret)-returnret;+gotoout;ret=bpf_copy_from_user(data_val,sizeof(structdata),(void*)(unsignedlong)value);if(ret)-returnret;+gotoout;if(data_val->data_len>sizeof(data_val->data))return-EINVAL;
@@ -84,5 +85,8 @@ int BPF_PROG(bpf, int cmd, union bpf_attr *attr, unsigned int size)bpf_key_put(trusted_keyring);+out:+set_if_not_errno_or_zero(ret,-EFAULT);+returnret;}
@@ -7,6 +7,7 @@#include"bpf_misc.h"#include"xdp_metadata.h"#include"bpf_kfuncs.h"+#include"err.h"/* The compiler may be able to detect the access to uninitializedmemoryintheroutinesperformingoutofboundmemoryaccessesand
From: Xu Kuohai <redacted>
Add test for lsm tail call to ensure tail call can only be used between
bpf lsm progs attached to the same hook.
Signed-off-by: Xu Kuohai <redacted>
---
.../selftests/bpf/prog_tests/test_lsm.c | 46 ++++++++++++++++++-
.../selftests/bpf/progs/lsm_tailcall.c | 34 ++++++++++++++
2 files changed, 79 insertions(+), 1 deletion(-)
create mode 100644 tools/testing/selftests/bpf/progs/lsm_tailcall.c
Cc Harishankar Vishwanathan, Prof. Srinivas Narayana and Prof. Santosh
Nagarakatte, and Matan Shachnai, whom have recently work on
scalar*_min_max_and(); also dropping LSM/FS related mails from Cc since
it's a bit long and I'm not sure whether the mailing list will reject
due to too many email in Cc.
On Thu, Jul 11, 2024 at 07:38:24PM GMT, Xu Kuohai wrote:
With lsm return value check, the no-alu32 version test_libbpf_get_fd_by_id_opts
is rejected by the verifier, and the log says:
0: R1=ctx() R10=fp0
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
0: (b7) r0 = 0 ; R0_w=0
1: (79) r2 = *(u64 *)(r1 +0)
func 'bpf_lsm_bpf_map' arg0 has btf_id 916 type STRUCT 'bpf_map'
2: R1=ctx() R2_w=trusted_ptr_bpf_map()
; if (map != (struct bpf_map *)&data_input) @ test_libbpf_get_fd_by_id_opts.c:29
2: (18) r3 = 0xffff9742c0951a00 ; R3_w=map_ptr(map=data_input,ks=4,vs=4)
4: (5d) if r2 != r3 goto pc+4 ; R2_w=trusted_ptr_bpf_map() R3_w=map_ptr(map=data_input,ks=4,vs=4)
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
5: (79) r0 = *(u64 *)(r1 +8) ; R0_w=scalar() R1=ctx()
; if (fmode & FMODE_WRITE) @ test_libbpf_get_fd_by_id_opts.c:32
6: (67) r0 <<= 62 ; R0_w=scalar(smax=0x4000000000000000,umax=0xc000000000000000,smin32=0,smax32=umax32=0,var_off=(0x0; 0xc000000000000000))
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
; @ test_libbpf_get_fd_by_id_opts.c:0
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
9: (95) exit
And here is the C code of the prog.
SEC("lsm/bpf_map")
int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode)
{
if (map != (struct bpf_map *)&data_input)
return 0;
if (fmode & FMODE_WRITE)
return -EACCES;
return 0;
}
It is clear that the prog can only return either 0 or -EACCESS, and both
values are legal.
So why is it rejected by the verifier?
The verifier log shows that the second if and return value setting
statements in the prog is optimized to bitwise operations "r0 s>>= 63"
and "r0 &= -13". The verifier correctly deduces that the value of
r0 is in the range [-1, 0] after verifing instruction "r0 s>>= 63".
But when the verifier proceeds to verify instruction "r0 &= -13", it
fails to deduce the correct value range of r0.
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
So why the verifier fails to deduce the result of 'r0 &= -13'?
The verifier uses tnum to track values, and the two ranges "[-1, 0]" and
"[0, -1ULL]" are encoded to the same tnum. When verifing instruction
"r0 &= -13", the verifier erroneously deduces the result from
"[0, -1ULL] AND -13", which is out of the expected return range
[-4095, 0].
As explained by Eduard in [0], the clang transformation that generates this
pattern is located in DAGCombiner::SimplifySelectCC() method (see [1]).
...
As suggested by Eduard and Andrii, this patch makes a special case
for source or destination register of '&=' operation being in
range [-1, 0].
...
Been wonder whether it possible for a more general approach ever since I
saw the discussion back in April. I think I've finally got something.
The problem we face here is that the tightest bound for the [-1, 0] case
was tracked with signed ranges, yet the BPF verifier looses knowledge of
them all too quickly in scalar*_min_max_and(); knowledge of previous
signed ranges were not used at all to derive the outcome of signed
ranges after BPF_AND.
static void scalar_min_max_and(...) {
...
if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
dst_reg->smin_value = dst_reg->umin_value;
dst_reg->smax_value = dst_reg->umax_value;
} else {
dst_reg->smin_value = S64_MIN;
dst_reg->smax_value = S64_MAX;
}
...
}
So looks like its time to be nobody[1] and try to teach BPF verifier how
track signed ranges when ANDing two (possibly) negative numbers. Luckily
bitwise AND is comparatively easier to do than other bitwise operations:
non-negative range & non-negative range is always non-negative,
non-negative range & negative range is still always non-negative, and
negative range & negative range is always negative.
smax_value is straight forwards, we can just do
max(dst_reg->smax_value, src_reg->smax_value)
which works across all sign combinations. Technically for non-negative &
non-negative we can use min() instead of max(), but the non-negative &
non-negative case should be handled pretty well by the unsigned ranges
already; it seems simpler to let such knowledge flows from unsigned
ranges to signed ranges during reg_bounds_sync(). Plus we are not wrong
for non-negative & non-negative by using max(), just imprecise, so no
correctness/soundness issue here.
smin_value is the tricker one, but doable with
masked_negative(min(dst_reg->smin_value, src_reg->smin_value))
where masked_negative(v) basically just clear all bits after the most
significant unset bit, effectively rounding a negative value down to a
negative power-of-2 value, and returning 0 for non-negative values. E.g.
for some 8-bit, negative value
masked_negative(0b11101001) == 0b11100000
This can be done with a tweaked version of "Round up to the next highest
power of 2"[2],
/* Invert the bits so the first unset bit can be propagated with |= */
v = ~v;
/* Now propagate the first (previously unset, now set) bit to the
* trailing positions */
v |= v >> 1;
v |= v >> 2;
v |= v >> 4;
...
v |= v >> 32; /* Assuming 64-bit */
/* Propagation done, now invert again */
v = ~v;
Again, we technically can do better if we take sign bit into account,
but deriving smin_value this way should still be correct/sound across
different sign combinations, and overall should help us derived [-16, 0]
from "[-1, 0] AND -13", thus preventing BPF verifier from rejecting the
program.
---
Alternatively we can employ a range-splitting trick (think I saw this in
[3]) that allow us to take advantage of existing tnum_and() by splitting
the signed ranges into two if the range crosses the sign boundary (i.e.
contains both non-negative and negative values), one range will be
[smin, U64_MAX], the other will be [0, smax]. This way we get around
tnum's weakness of representing [-1, 0] as [0, U64_MAX].
if (src_reg->smin_value < 0 && src_reg->smax_value >= 0) {
src_lower = tnum_range(src_reg->smin_value, U64_MAX);
src_higher = tnum_range(0, src_reg->smax_value);
} else {
src_lower = tnum_range(src_reg->smin_value, src_reg->smax_value);
src_higher = tnum_range(src_reg->smin_value, src_reg->smax_value);
}
if (dst_reg->smin_value < 0 && dst_reg->smax_value >= 0) {
dst_lower = tnum_range(dst_reg->smin_value, U64_MAX);
dst_higher = tnum_range(0, dst_reg->smax_value);
} else {
dst_lower = tnum_range(dst_reg->smin_value, dst_reg->smax_value);
dst_higher = tnum_range(dst_reg->smin_value, dst_reg->smax_value);
}
lower = tnum_and(src_lower, dst_lower);
higher = tnum_and(src_higher, dst_higher);
dst->smin_value = lower.value;
dst->smax_value = higher.value | higher.mask;
---
Personally I like the first method better as it is simpler yet still
does the job well enough. I'll work on that in the next few days and see
if it actually works.
1: https://github.com/torvalds/linux/blob/dac045fc9fa6/kernel/bpf/verifier.c#L13338
2: https://graphics.stanford.edu/~seander/bithacks.html#RoundUpPowerOf2
3: https://dl.acm.org/doi/10.1145/2651360
...
Cc Harishankar Vishwanathan, Prof. Srinivas Narayana and Prof. Santosh
Nagarakatte, and Matan Shachnai, whom have recently work on
scalar*_min_max_and(); also dropping LSM/FS related mails from Cc since
it's a bit long and I'm not sure whether the mailing list will reject
due to too many email in Cc.
On Thu, Jul 11, 2024 at 07:38:24PM GMT, Xu Kuohai wrote:
quoted
With lsm return value check, the no-alu32 version test_libbpf_get_fd_by_id_opts
is rejected by the verifier, and the log says:
0: R1=ctx() R10=fp0
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
0: (b7) r0 = 0 ; R0_w=0
1: (79) r2 = *(u64 *)(r1 +0)
func 'bpf_lsm_bpf_map' arg0 has btf_id 916 type STRUCT 'bpf_map'
2: R1=ctx() R2_w=trusted_ptr_bpf_map()
; if (map != (struct bpf_map *)&data_input) @ test_libbpf_get_fd_by_id_opts.c:29
2: (18) r3 = 0xffff9742c0951a00 ; R3_w=map_ptr(map=data_input,ks=4,vs=4)
4: (5d) if r2 != r3 goto pc+4 ; R2_w=trusted_ptr_bpf_map() R3_w=map_ptr(map=data_input,ks=4,vs=4)
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
5: (79) r0 = *(u64 *)(r1 +8) ; R0_w=scalar() R1=ctx()
; if (fmode & FMODE_WRITE) @ test_libbpf_get_fd_by_id_opts.c:32
6: (67) r0 <<= 62 ; R0_w=scalar(smax=0x4000000000000000,umax=0xc000000000000000,smin32=0,smax32=umax32=0,var_off=(0x0; 0xc000000000000000))
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
; @ test_libbpf_get_fd_by_id_opts.c:0
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
9: (95) exit
And here is the C code of the prog.
SEC("lsm/bpf_map")
int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode)
{
if (map != (struct bpf_map *)&data_input)
return 0;
if (fmode & FMODE_WRITE)
return -EACCES;
return 0;
}
It is clear that the prog can only return either 0 or -EACCESS, and both
values are legal.
So why is it rejected by the verifier?
The verifier log shows that the second if and return value setting
statements in the prog is optimized to bitwise operations "r0 s>>= 63"
and "r0 &= -13". The verifier correctly deduces that the value of
r0 is in the range [-1, 0] after verifing instruction "r0 s>>= 63".
But when the verifier proceeds to verify instruction "r0 &= -13", it
fails to deduce the correct value range of r0.
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
So why the verifier fails to deduce the result of 'r0 &= -13'?
The verifier uses tnum to track values, and the two ranges "[-1, 0]" and
"[0, -1ULL]" are encoded to the same tnum. When verifing instruction
"r0 &= -13", the verifier erroneously deduces the result from
"[0, -1ULL] AND -13", which is out of the expected return range
[-4095, 0].
As explained by Eduard in [0], the clang transformation that generates this
pattern is located in DAGCombiner::SimplifySelectCC() method (see [1]).
...
quoted
As suggested by Eduard and Andrii, this patch makes a special case
for source or destination register of '&=' operation being in
range [-1, 0].
...
Been wonder whether it possible for a more general approach ever since I
saw the discussion back in April. I think I've finally got something.
The problem we face here is that the tightest bound for the [-1, 0] case
was tracked with signed ranges, yet the BPF verifier looses knowledge of
them all too quickly in scalar*_min_max_and(); knowledge of previous
signed ranges were not used at all to derive the outcome of signed
ranges after BPF_AND.
static void scalar_min_max_and(...) {
...
if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
dst_reg->smin_value = dst_reg->umin_value;
dst_reg->smax_value = dst_reg->umax_value;
} else {
dst_reg->smin_value = S64_MIN;
dst_reg->smax_value = S64_MAX;
}
...
}
This is indeed the root cause.
So looks like its time to be nobody[1] and try to teach BPF verifier how
track signed ranges when ANDing two (possibly) negative numbers. Luckily
bitwise AND is comparatively easier to do than other bitwise operations:
non-negative range & non-negative range is always non-negative,
non-negative range & negative range is still always non-negative, and
negative range & negative range is always negative.
Right, only bitwise ANDing two negatives yields to a negative result.
smax_value is straight forwards, we can just do
max(dst_reg->smax_value, src_reg->smax_value)
which works across all sign combinations. Technically for non-negative &
non-negative we can use min() instead of max(), but the non-negative &
non-negative case should be handled pretty well by the unsigned ranges
already; it seems simpler to let such knowledge flows from unsigned
ranges to signed ranges during reg_bounds_sync(). Plus we are not wrong
for non-negative & non-negative by using max(), just imprecise, so no
correctness/soundness issue here.
I think this is correct, since in two's complement, more '1' bits means
more large, regardless of sign, and bitwise AND never generates more '1'
bits.
smin_value is the tricker one, but doable with
masked_negative(min(dst_reg->smin_value, src_reg->smin_value))
where masked_negative(v) basically just clear all bits after the most
significant unset bit, effectively rounding a negative value down to a
negative power-of-2 value, and returning 0 for non-negative values. E.g.
for some 8-bit, negative value
masked_negative(0b11101001) == 0b11100000
Ah, it's really tricky. Seems it's the longest high '1' bits sequence
in both operands. This '1' bits should remain unchanged by the bitwise
AND operation. So this sequence must be in the result, making it the
minimum possible value.
This can be done with a tweaked version of "Round up to the next highest
power of 2"[2],
/* Invert the bits so the first unset bit can be propagated with |= */
v = ~v;
/* Now propagate the first (previously unset, now set) bit to the
* trailing positions */
v |= v >> 1;
v |= v >> 2;
v |= v >> 4;
...
v |= v >> 32; /* Assuming 64-bit */
/* Propagation done, now invert again */
v = ~v;
Again, we technically can do better if we take sign bit into account,
but deriving smin_value this way should still be correct/sound across
different sign combinations, and overall should help us derived [-16, 0]
from "[-1, 0] AND -13", thus preventing BPF verifier from rejecting the
program.
---
Alternatively we can employ a range-splitting trick (think I saw this in
[3]) that allow us to take advantage of existing tnum_and() by splitting
the signed ranges into two if the range crosses the sign boundary (i.e.
contains both non-negative and negative values), one range will be
[smin, U64_MAX], the other will be [0, smax]. This way we get around
tnum's weakness of representing [-1, 0] as [0, U64_MAX].
if (src_reg->smin_value < 0 && src_reg->smax_value >= 0) {
src_lower = tnum_range(src_reg->smin_value, U64_MAX);
src_higher = tnum_range(0, src_reg->smax_value);
} else {
src_lower = tnum_range(src_reg->smin_value, src_reg->smax_value);
src_higher = tnum_range(src_reg->smin_value, src_reg->smax_value);
}
if (dst_reg->smin_value < 0 && dst_reg->smax_value >= 0) {
dst_lower = tnum_range(dst_reg->smin_value, U64_MAX);
dst_higher = tnum_range(0, dst_reg->smax_value);
} else {
dst_lower = tnum_range(dst_reg->smin_value, dst_reg->smax_value);
dst_higher = tnum_range(dst_reg->smin_value, dst_reg->smax_value);
}
lower = tnum_and(src_lower, dst_lower);
higher = tnum_and(src_higher, dst_higher);
dst->smin_value = lower.value;
dst->smax_value = higher.value | higher.mask;
This looks even more tricky...
---
Personally I like the first method better as it is simpler yet still
does the job well enough. I'll work on that in the next few days and see
if it actually works.
This really sounds great. Thank you for the excellent work!
This commit teach the BPF verifier how to infer signed ranges directly
from signed ranges of the operands to prevent verifier rejection, which
is needed for the following BPF program's no-alu32 version, as shown by
Xu Kuohai:
SEC("lsm/bpf_map")
int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode)
{
if (map != (struct bpf_map *)&data_input)
return 0;
if (fmode & FMODE_WRITE)
return -EACCES;
return 0;
}
Where the relevant verifer log upon rejection are:
...
5: (79) r0 = *(u64 *)(r1 +8) ; R0_w=scalar() R1=ctx()
; if (fmode & FMODE_WRITE) @ test_libbpf_get_fd_by_id_opts.c:32
6: (67) r0 <<= 62 ; R0_w=scalar(smax=0x4000000000000000,umax=0xc000000000000000,smin32=0,smax32=umax32=0,var_off=(0x0; 0xc000000000000000))
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
; @ test_libbpf_get_fd_by_id_opts.c:0
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
9: (95) exit
This sequence of instructions comes from Clang's transformation located
in DAGCombiner::SimplifySelectCC() method, which combined the "fmode &
FMODE_WRITE" check with the return statement without needing BPF_JMP at
all. See Eduard's comment for more detail of this transformation[0].
While the verifier can correctly infer that the value of r0 is in a
tight [-1, 0] range after instruction "r0 s>>= 63", is was not able to
come up with a tight range for "r0 &= -13" (which would be [-13, 0]),
and instead inferred a very loose range:
r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
The reason is that scalar*_min_max_add() mainly relies on tnum for
interring value in register after BPF_AND, however [-1, 0] cannot be
tracked precisely with tnum, and effectively turns into [0, -1] (i.e.
tnum_unknown). So upon BPF_AND the resulting tnum is equivalent to
dst_reg->var_off = tnum_and(tnum_unknown, tnum_const(-13))
And from there the BPF verifier was only able to infer smin=S64_MIN,
smax=0x7ffffffffffffff3, which is outside of the expected [-4095, 0]
range for return values, and thus the program was rejected.
To allow verification of such instruction pattern, update
scalar*_min_max_and() to infer signed ranges directly from signed ranges
of the operands. With BPF_AND, the resulting value always gains more
unset '0' bit, thus it only move towards 0x0000000000000000. The
difficulty lies with how to deal with signs. While non-negative
(positive and zero) value simply grows smaller, a negative number can
grows smaller, but may also underflow and become a larger value.
To better address this situation we split the signed ranges into
negative range and non-negative range cases, ignoring the mixed sign
cases for now; and only consider how to calculate smax_value.
Since negative range & negative range preserve the sign bit, so we know
the result is still a negative value, thus it only move towards S64_MIN,
but never underflow, thus a save bet is to use a value in ranges that is
closet to 0, thus "max(dst_reg->smax_value, src->smax_value)". For
negative range & positive range the sign bit is always cleared, thus we
know the resulting is a non-negative, and only moves towards 0, so a
safe bet is to use smax_value of the non-negative range. Last but not
least, non-negative range & non-negative range is still a non-negative
value, and only moves towards 0; however same as the unsigned range
case, the maximum is actually capped by the lesser of the two, and thus
min(dst_reg->smax_value, src_reg->smax_value);
Listing out the above reasoning as a table (dst_reg abbreviated as dst,
src_reg abbreviated as src, smax_value abbrivated as smax) we get:
| src_reg
smax = ? +---------------------------+---------------------------
| negative | non-negative
---------+--------------+---------------------------+---------------------------
| negative | max(dst->smax, src->smax) | src->smax
dst_reg +--------------+---------------------------+---------------------------
| non-negative | dst->smax | min(dst->smax, src->smax)
However this is quite complicated, luckily it can be simplified given
the following observations
max(dst_reg->smax_value, src_reg->smax_value) >= src_reg->smax_value
max(dst_reg->smax_value, src_reg->smax_value) >= dst_reg->smax_value
max(dst_reg->smax_value, src_reg->smax_value) >= min(dst_reg->smax_value, src_reg->smax_value)
So we could substitute the cells in the table above all with max(...),
and arrive at:
| src_reg
smax' = ? +---------------------------+---------------------------
| negative | non-negative
---------+--------------+---------------------------+---------------------------
| negative | max(dst->smax, src->smax) | max(dst->smax, src->smax)
dst_reg +--------------+---------------------------+---------------------------
| non-negative | max(dst->smax, src->smax) | max(dst->smax, src->smax)
Meaning that simply using
max(dst_reg->smax_value, src_reg->smax_value)
to calculate the resulting smax_value would work across all sign combinations.
For smin_value, we know that both non-negative range & non-negative
range and negative range & non-negative range both result in a
non-negative value, so an easy guess is to use the minimum non-negative
value, thus 0.
| src_reg
smin = ? +----------------------------+---------------------------
| negative | non-negative
---------+--------------+----------------------------+---------------------------
| negative | ? | 0
dst_reg +--------------+----------------------------+---------------------------
| non-negative | 0 | 0
This leave the negative range & negative range case to be considered. We
know that negative range & negative range always yield a negative value,
so a preliminary guess would be S64_MIN. However, that guess is too
imprecise to help with the r0 <<= 62, r0 s>>= 63, r0 &= -13 pattern
we're trying to deal with here.
This can be further improve with the observation that for negative range
& negative range, the smallest possible value must be one that has
longest _common_ most-significant set '1' bits sequence, thus we can use
min(dst_reg->smin_value, src->smin_value) as the starting point, as the
smaller value will be the one with the shorter most-significant set '1'
bits sequence. But that alone is not enough, as we do not know whether
rest of the bits would be set, so the safest guess would be one that
clear alls bits after the most-significant set '1' bits sequence,
something akin to bit_floor(), but for rounding to a negative power-of-2
instead.
negative_bit_floor(0xffff000000000003) == 0xffff000000000000
negative_bit_floor(0xf0ff0000ffff0000) == 0xf000000000000000
negative_bit_floor(0xfffffb0000000000) == 0xfffff80000000000
With negative range & negative range solve, we now have:
| src_reg
smin = ? +----------------------------+---------------------------
| negative | non-negative
---------+--------------+----------------------------+---------------------------
| negative |negative_bit_floor( | 0
| | min(dst->smin, src->smin))|
dst_reg +--------------+----------------------------+---------------------------
| non-negative | 0 | 0
This can be further simplied since min(dst->smin, src->smin) < 0 when both
dst_reg and src_reg have a negative range. Which means using
negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value)
to calculate the resulting smin_value would work across all sign combinations.
Together these allows us to infer the signed range of the result of BPF_AND
operation using the signed range from its operands.
[0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/
Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/
Cc: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Shung-Hsi Yu <redacted>
---
kernel/bpf/verifier.c | 62 +++++++++++++++++++++++++++++--------------
1 file changed, 42 insertions(+), 20 deletions(-)
@@ -13466,6 +13466,39 @@ static void scalar_min_max_mul(struct bpf_reg_state *dst_reg,}}+/* Clears all trailing bits after the most significant unset bit.+*+*UsedforestimatingtheminimumpossiblevalueafterBPF_AND.This+*effectivelyroundsanegativevaluedowntoanegativepower-of-2value+*(exceptfor-1,whichjustreturn-1)andreturning0fornon-negative+*values.E.g.masked32_negative(0xff0ff0ff)==0xff000000.+*/+staticinlines32negative32_bit_floor(s32v)+{+/* XXX: per C standard section 6.5.7 right shift of signed negative+*valueisimplementation-defined.Shouldunsignedtypebeusedhere+*instead?+*/+v&=v>>1;+v&=v>>2;+v&=v>>4;+v&=v>>8;+v&=v>>16;+returnv;+}++/* Same as negative32_bit_floor() above, but for 64-bit signed value */+staticinlines64negative_bit_floor(s64v)+{+v&=v>>1;+v&=v>>2;+v&=v>>4;+v&=v>>8;+v&=v>>16;+v&=v>>32;+returnv;+}+staticvoidscalar32_min_max_and(structbpf_reg_state*dst_reg,structbpf_reg_state*src_reg){
@@ -13485,16 +13518,10 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,dst_reg->u32_min_value=var32_off.value;dst_reg->u32_max_value=min(dst_reg->u32_max_value,umax_val);-/* Safe to set s32 bounds by casting u32 result into s32 when u32-*doesn'tcrosssignboundary.Otherwisesets32boundstounbounded.-*/-if((s32)dst_reg->u32_min_value<=(s32)dst_reg->u32_max_value){-dst_reg->s32_min_value=dst_reg->u32_min_value;-dst_reg->s32_max_value=dst_reg->u32_max_value;-}else{-dst_reg->s32_min_value=S32_MIN;-dst_reg->s32_max_value=S32_MAX;-}+/* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */+dst_reg->s32_min_value=negative32_bit_floor(min(dst_reg->s32_min_value,+src_reg->s32_min_value));+dst_reg->s32_max_value=max(dst_reg->s32_max_value,src_reg->s32_max_value);}staticvoidscalar_min_max_and(structbpf_reg_state*dst_reg,
@@ -13515,16 +13542,11 @@ static void scalar_min_max_and(struct bpf_reg_state *dst_reg,dst_reg->umin_value=dst_reg->var_off.value;dst_reg->umax_value=min(dst_reg->umax_value,umax_val);-/* Safe to set s64 bounds by casting u64 result into s64 when u64-*doesn'tcrosssignboundary.Otherwisesets64boundstounbounded.-*/-if((s64)dst_reg->umin_value<=(s64)dst_reg->umax_value){-dst_reg->smin_value=dst_reg->umin_value;-dst_reg->smax_value=dst_reg->umax_value;-}else{-dst_reg->smin_value=S64_MIN;-dst_reg->smax_value=S64_MAX;-}+/* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */+dst_reg->smin_value=negative_bit_floor(min(dst_reg->smin_value,+src_reg->smin_value));+dst_reg->smax_value=max(dst_reg->smax_value,src_reg->smax_value);+/* We may learn something more from the var_off */__update_reg_bounds(dst_reg);}
@@ -13466,6 +13466,39 @@ static void scalar_min_max_mul(struct bpf_reg_state *dst_reg,}}+/* Clears all trailing bits after the most significant unset bit.+*+*UsedforestimatingtheminimumpossiblevalueafterBPF_AND.This+*effectivelyroundsanegativevaluedowntoanegativepower-of-2value+*(exceptfor-1,whichjustreturn-1)andreturning0fornon-negative+*values.E.g.masked32_negative(0xff0ff0ff)==0xff000000.
s/masked32_negative/negative32_bit_floor/
quoted hunk
+ */
+static inline s32 negative32_bit_floor(s32 v)
+{
+ /* XXX: per C standard section 6.5.7 right shift of signed negative
+ * value is implementation-defined. Should unsigned type be used here
+ * instead?
+ */
+ v &= v >> 1;
+ v &= v >> 2;
+ v &= v >> 4;
+ v &= v >> 8;
+ v &= v >> 16;
+ return v;
+}
+
+/* Same as negative32_bit_floor() above, but for 64-bit signed value */
+static inline s64 negative_bit_floor(s64 v)
+{
+ v &= v >> 1;
+ v &= v >> 2;
+ v &= v >> 4;
+ v &= v >> 8;
+ v &= v >> 16;
+ v &= v >> 32;
+ return v;
+}
+
static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
struct bpf_reg_state *src_reg)
{
@@ -13485,16 +13518,10 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg, dst_reg->u32_min_value = var32_off.value; dst_reg->u32_max_value = min(dst_reg->u32_max_value, umax_val);- /* Safe to set s32 bounds by casting u32 result into s32 when u32- * doesn't cross sign boundary. Otherwise set s32 bounds to unbounded.- */- if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {- dst_reg->s32_min_value = dst_reg->u32_min_value;- dst_reg->s32_max_value = dst_reg->u32_max_value;- } else {- dst_reg->s32_min_value = S32_MIN;- dst_reg->s32_max_value = S32_MAX;- }+ /* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */+ dst_reg->s32_min_value = negative32_bit_floor(min(dst_reg->s32_min_value,+ src_reg->s32_min_value));+ dst_reg->s32_max_value = max(dst_reg->s32_max_value, src_reg->s32_max_value); } static void scalar_min_max_and(struct bpf_reg_state *dst_reg,
@@ -13515,16 +13542,11 @@ static void scalar_min_max_and(struct bpf_reg_state *dst_reg, dst_reg->umin_value = dst_reg->var_off.value; dst_reg->umax_value = min(dst_reg->umax_value, umax_val);- /* Safe to set s64 bounds by casting u64 result into s64 when u64- * doesn't cross sign boundary. Otherwise set s64 bounds to unbounded.- */- if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {- dst_reg->smin_value = dst_reg->umin_value;- dst_reg->smax_value = dst_reg->umax_value;- } else {- dst_reg->smin_value = S64_MIN;- dst_reg->smax_value = S64_MAX;- }+ /* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */+ dst_reg->smin_value = negative_bit_floor(min(dst_reg->smin_value,+ src_reg->smin_value));+ dst_reg->smax_value = max(dst_reg->smax_value, src_reg->smax_value);+ /* We may learn something more from the var_off */ __update_reg_bounds(dst_reg); }
On Tue, Jul 16, 2024 at 03:05:11PM GMT, Xu Kuohai wrote:
On 7/15/2024 11:29 PM, Shung-Hsi Yu wrote:
quoted
Cc Harishankar Vishwanathan, Prof. Srinivas Narayana and Prof. Santosh
Nagarakatte, and Matan Shachnai, whom have recently work on
scalar*_min_max_and(); also dropping LSM/FS related mails from Cc since
it's a bit long and I'm not sure whether the mailing list will reject
due to too many email in Cc.
On Thu, Jul 11, 2024 at 07:38:24PM GMT, Xu Kuohai wrote:
quoted
With lsm return value check, the no-alu32 version test_libbpf_get_fd_by_id_opts
is rejected by the verifier, and the log says:
0: R1=ctx() R10=fp0
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
0: (b7) r0 = 0 ; R0_w=0
1: (79) r2 = *(u64 *)(r1 +0)
func 'bpf_lsm_bpf_map' arg0 has btf_id 916 type STRUCT 'bpf_map'
2: R1=ctx() R2_w=trusted_ptr_bpf_map()
; if (map != (struct bpf_map *)&data_input) @ test_libbpf_get_fd_by_id_opts.c:29
2: (18) r3 = 0xffff9742c0951a00 ; R3_w=map_ptr(map=data_input,ks=4,vs=4)
4: (5d) if r2 != r3 goto pc+4 ; R2_w=trusted_ptr_bpf_map() R3_w=map_ptr(map=data_input,ks=4,vs=4)
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
5: (79) r0 = *(u64 *)(r1 +8) ; R0_w=scalar() R1=ctx()
; if (fmode & FMODE_WRITE) @ test_libbpf_get_fd_by_id_opts.c:32
6: (67) r0 <<= 62 ; R0_w=scalar(smax=0x4000000000000000,umax=0xc000000000000000,smin32=0,smax32=umax32=0,var_off=(0x0; 0xc000000000000000))
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
; @ test_libbpf_get_fd_by_id_opts.c:0
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
; int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) @ test_libbpf_get_fd_by_id_opts.c:27
9: (95) exit
And here is the C code of the prog.
SEC("lsm/bpf_map")
int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode)
{
if (map != (struct bpf_map *)&data_input)
return 0;
if (fmode & FMODE_WRITE)
return -EACCES;
return 0;
}
It is clear that the prog can only return either 0 or -EACCESS, and both
values are legal.
So why is it rejected by the verifier?
The verifier log shows that the second if and return value setting
statements in the prog is optimized to bitwise operations "r0 s>>= 63"
and "r0 &= -13". The verifier correctly deduces that the value of
r0 is in the range [-1, 0] after verifing instruction "r0 s>>= 63".
But when the verifier proceeds to verify instruction "r0 &= -13", it
fails to deduce the correct value range of r0.
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
So why the verifier fails to deduce the result of 'r0 &= -13'?
The verifier uses tnum to track values, and the two ranges "[-1, 0]" and
"[0, -1ULL]" are encoded to the same tnum. When verifing instruction
"r0 &= -13", the verifier erroneously deduces the result from
"[0, -1ULL] AND -13", which is out of the expected return range
[-4095, 0].
As explained by Eduard in [0], the clang transformation that generates this
pattern is located in DAGCombiner::SimplifySelectCC() method (see [1]).
...
quoted
As suggested by Eduard and Andrii, this patch makes a special case
for source or destination register of '&=' operation being in
range [-1, 0].
...
Been wonder whether it possible for a more general approach ever since I
saw the discussion back in April. I think I've finally got something.
The problem we face here is that the tightest bound for the [-1, 0] case
was tracked with signed ranges, yet the BPF verifier looses knowledge of
them all too quickly in scalar*_min_max_and(); knowledge of previous
signed ranges were not used at all to derive the outcome of signed
ranges after BPF_AND.
static void scalar_min_max_and(...) {
...
if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
dst_reg->smin_value = dst_reg->umin_value;
dst_reg->smax_value = dst_reg->umax_value;
} else {
dst_reg->smin_value = S64_MIN;
dst_reg->smax_value = S64_MAX;
}
...
}
This is indeed the root cause.
quoted
So looks like its time to be nobody[1] and try to teach BPF verifier how
track signed ranges when ANDing two (possibly) negative numbers. Luckily
bitwise AND is comparatively easier to do than other bitwise operations:
non-negative range & non-negative range is always non-negative,
non-negative range & negative range is still always non-negative, and
negative range & negative range is always negative.
Right, only bitwise ANDing two negatives yields to a negative result.
quoted
smax_value is straight forwards, we can just do
max(dst_reg->smax_value, src_reg->smax_value)
which works across all sign combinations. Technically for non-negative &
non-negative we can use min() instead of max(), but the non-negative &
non-negative case should be handled pretty well by the unsigned ranges
already; it seems simpler to let such knowledge flows from unsigned
ranges to signed ranges during reg_bounds_sync(). Plus we are not wrong
for non-negative & non-negative by using max(), just imprecise, so no
correctness/soundness issue here.
I think this is correct, since in two's complement, more '1' bits means
more large, regardless of sign, and bitwise AND never generates more '1'
bits.
quoted
smin_value is the tricker one, but doable with
masked_negative(min(dst_reg->smin_value, src_reg->smin_value))
where masked_negative(v) basically just clear all bits after the most
significant unset bit, effectively rounding a negative value down to a
negative power-of-2 value, and returning 0 for non-negative values. E.g.
for some 8-bit, negative value
masked_negative(0b11101001) == 0b11100000
Ah, it's really tricky. Seems it's the longest high '1' bits sequence
in both operands. This '1' bits should remain unchanged by the bitwise
AND operation. So this sequence must be in the result, making it the
minimum possible value.
quoted
This can be done with a tweaked version of "Round up to the next highest
power of 2"[2],
/* Invert the bits so the first unset bit can be propagated with |= */
v = ~v;
/* Now propagate the first (previously unset, now set) bit to the
* trailing positions */
v |= v >> 1;
v |= v >> 2;
v |= v >> 4;
...
v |= v >> 32; /* Assuming 64-bit */
/* Propagation done, now invert again */
v = ~v;
Again, we technically can do better if we take sign bit into account,
but deriving smin_value this way should still be correct/sound across
different sign combinations, and overall should help us derived [-16, 0]
from "[-1, 0] AND -13", thus preventing BPF verifier from rejecting the
program.
---
Alternatively we can employ a range-splitting trick (think I saw this in
[3]) that allow us to take advantage of existing tnum_and() by splitting
the signed ranges into two if the range crosses the sign boundary (i.e.
contains both non-negative and negative values), one range will be
[smin, U64_MAX], the other will be [0, smax]. This way we get around
tnum's weakness of representing [-1, 0] as [0, U64_MAX].
if (src_reg->smin_value < 0 && src_reg->smax_value >= 0) {
src_lower = tnum_range(src_reg->smin_value, U64_MAX);
src_higher = tnum_range(0, src_reg->smax_value);
} else {
src_lower = tnum_range(src_reg->smin_value, src_reg->smax_value);
src_higher = tnum_range(src_reg->smin_value, src_reg->smax_value);
}
if (dst_reg->smin_value < 0 && dst_reg->smax_value >= 0) {
dst_lower = tnum_range(dst_reg->smin_value, U64_MAX);
dst_higher = tnum_range(0, dst_reg->smax_value);
} else {
dst_lower = tnum_range(dst_reg->smin_value, dst_reg->smax_value);
dst_higher = tnum_range(dst_reg->smin_value, dst_reg->smax_value);
}
lower = tnum_and(src_lower, dst_lower);
higher = tnum_and(src_higher, dst_higher);
dst->smin_value = lower.value;
dst->smax_value = higher.value | higher.mask;
This looks even more tricky...
Indeed, and I think the above is still wrong because it did not proper
set smin_value to S64_MIN when needed.
quoted
Personally I like the first method better as it is simpler yet still
does the job well enough. I'll work on that in the next few days and see
if it actually works.
This really sounds great. Thank you for the excellent work!
Sent RFC in sibling thread. I think it would be better if the patch was
included as part of your series. But let's see what the other think of
it first.
From: Eduard Zingerman <eddyz87@gmail.com> Date: 2024-07-17 21:10:42
On Tue, 2024-07-16 at 22:52 +0800, Shung-Hsi Yu wrote:
[...]
To allow verification of such instruction pattern, update
scalar*_min_max_and() to infer signed ranges directly from signed ranges
of the operands. With BPF_AND, the resulting value always gains more
unset '0' bit, thus it only move towards 0x0000000000000000. The
difficulty lies with how to deal with signs. While non-negative
(positive and zero) value simply grows smaller, a negative number can
grows smaller, but may also underflow and become a larger value.
To better address this situation we split the signed ranges into
negative range and non-negative range cases, ignoring the mixed sign
cases for now; and only consider how to calculate smax_value.
Since negative range & negative range preserve the sign bit, so we know
the result is still a negative value, thus it only move towards S64_MIN,
but never underflow, thus a save bet is to use a value in ranges that is
closet to 0, thus "max(dst_reg->smax_value, src->smax_value)". For
negative range & positive range the sign bit is always cleared, thus we
know the resulting is a non-negative, and only moves towards 0, so a
safe bet is to use smax_value of the non-negative range. Last but not
least, non-negative range & non-negative range is still a non-negative
value, and only moves towards 0; however same as the unsigned range
case, the maximum is actually capped by the lesser of the two, and thus
min(dst_reg->smax_value, src_reg->smax_value);
Listing out the above reasoning as a table (dst_reg abbreviated as dst,
src_reg abbreviated as src, smax_value abbrivated as smax) we get:
| src_reg
smax = ? +---------------------------+---------------------------
| negative | non-negative
---------+--------------+---------------------------+---------------------------
| negative | max(dst->smax, src->smax) | src->smax
dst_reg +--------------+---------------------------+---------------------------
| non-negative | dst->smax | min(dst->smax, src->smax)
However this is quite complicated, luckily it can be simplified given
the following observations
max(dst_reg->smax_value, src_reg->smax_value) >= src_reg->smax_value
max(dst_reg->smax_value, src_reg->smax_value) >= dst_reg->smax_value
max(dst_reg->smax_value, src_reg->smax_value) >= min(dst_reg->smax_value, src_reg->smax_value)
So we could substitute the cells in the table above all with max(...),
and arrive at:
| src_reg
smax' = ? +---------------------------+---------------------------
| negative | non-negative
---------+--------------+---------------------------+---------------------------
| negative | max(dst->smax, src->smax) | max(dst->smax, src->smax)
dst_reg +--------------+---------------------------+---------------------------
| non-negative | max(dst->smax, src->smax) | max(dst->smax, src->smax)
Meaning that simply using
max(dst_reg->smax_value, src_reg->smax_value)
to calculate the resulting smax_value would work across all sign combinations.
For smin_value, we know that both non-negative range & non-negative
range and negative range & non-negative range both result in a
non-negative value, so an easy guess is to use the minimum non-negative
value, thus 0.
| src_reg
smin = ? +----------------------------+---------------------------
| negative | non-negative
---------+--------------+----------------------------+---------------------------
| negative | ? | 0
dst_reg +--------------+----------------------------+---------------------------
| non-negative | 0 | 0
This leave the negative range & negative range case to be considered. We
know that negative range & negative range always yield a negative value,
so a preliminary guess would be S64_MIN. However, that guess is too
imprecise to help with the r0 <<= 62, r0 s>>= 63, r0 &= -13 pattern
we're trying to deal with here.
This can be further improve with the observation that for negative range
& negative range, the smallest possible value must be one that has
longest _common_ most-significant set '1' bits sequence, thus we can use
min(dst_reg->smin_value, src->smin_value) as the starting point, as the
smaller value will be the one with the shorter most-significant set '1'
bits sequence. But that alone is not enough, as we do not know whether
rest of the bits would be set, so the safest guess would be one that
clear alls bits after the most-significant set '1' bits sequence,
something akin to bit_floor(), but for rounding to a negative power-of-2
instead.
negative_bit_floor(0xffff000000000003) == 0xffff000000000000
negative_bit_floor(0xf0ff0000ffff0000) == 0xf000000000000000
negative_bit_floor(0xfffffb0000000000) == 0xfffff80000000000
With negative range & negative range solve, we now have:
| src_reg
smin = ? +----------------------------+---------------------------
| negative | non-negative
---------+--------------+----------------------------+---------------------------
| negative |negative_bit_floor( | 0
| | min(dst->smin, src->smin))|
dst_reg +--------------+----------------------------+---------------------------
| non-negative | 0 | 0
This can be further simplied since min(dst->smin, src->smin) < 0 when both
dst_reg and src_reg have a negative range. Which means using
negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value)
to calculate the resulting smin_value would work across all sign combinations.
Together these allows us to infer the signed range of the result of BPF_AND
operation using the signed range from its operands.
Hi Shung-Hsi,
This seems quite elegant.
As an additional check, I did a simple brute-force for all possible
ranges of 6-bit integers and bounds are computed safely.
[...]
On Wed, Jul 17, 2024 at 02:10:35PM GMT, Eduard Zingerman wrote:
On Tue, 2024-07-16 at 22:52 +0800, Shung-Hsi Yu wrote:
[...]
quoted
To allow verification of such instruction pattern, update
scalar*_min_max_and() to infer signed ranges directly from signed ranges
of the operands. With BPF_AND, the resulting value always gains more
unset '0' bit, thus it only move towards 0x0000000000000000. The
difficulty lies with how to deal with signs. While non-negative
(positive and zero) value simply grows smaller, a negative number can
grows smaller, but may also underflow and become a larger value.
To better address this situation we split the signed ranges into
negative range and non-negative range cases, ignoring the mixed sign
cases for now; and only consider how to calculate smax_value.
Since negative range & negative range preserve the sign bit, so we know
the result is still a negative value, thus it only move towards S64_MIN,
but never underflow, thus a save bet is to use a value in ranges that is
closet to 0, thus "max(dst_reg->smax_value, src->smax_value)". For
negative range & positive range the sign bit is always cleared, thus we
know the resulting is a non-negative, and only moves towards 0, so a
safe bet is to use smax_value of the non-negative range. Last but not
least, non-negative range & non-negative range is still a non-negative
value, and only moves towards 0; however same as the unsigned range
case, the maximum is actually capped by the lesser of the two, and thus
min(dst_reg->smax_value, src_reg->smax_value);
Listing out the above reasoning as a table (dst_reg abbreviated as dst,
src_reg abbreviated as src, smax_value abbrivated as smax) we get:
| src_reg
smax = ? +---------------------------+---------------------------
| negative | non-negative
---------+--------------+---------------------------+---------------------------
| negative | max(dst->smax, src->smax) | src->smax
dst_reg +--------------+---------------------------+---------------------------
| non-negative | dst->smax | min(dst->smax, src->smax)
However this is quite complicated, luckily it can be simplified given
the following observations
max(dst_reg->smax_value, src_reg->smax_value) >= src_reg->smax_value
max(dst_reg->smax_value, src_reg->smax_value) >= dst_reg->smax_value
max(dst_reg->smax_value, src_reg->smax_value) >= min(dst_reg->smax_value, src_reg->smax_value)
So we could substitute the cells in the table above all with max(...),
and arrive at:
| src_reg
smax' = ? +---------------------------+---------------------------
| negative | non-negative
---------+--------------+---------------------------+---------------------------
| negative | max(dst->smax, src->smax) | max(dst->smax, src->smax)
dst_reg +--------------+---------------------------+---------------------------
| non-negative | max(dst->smax, src->smax) | max(dst->smax, src->smax)
Meaning that simply using
max(dst_reg->smax_value, src_reg->smax_value)
to calculate the resulting smax_value would work across all sign combinations.
For smin_value, we know that both non-negative range & non-negative
range and negative range & non-negative range both result in a
non-negative value, so an easy guess is to use the minimum non-negative
value, thus 0.
| src_reg
smin = ? +----------------------------+---------------------------
| negative | non-negative
---------+--------------+----------------------------+---------------------------
| negative | ? | 0
dst_reg +--------------+----------------------------+---------------------------
| non-negative | 0 | 0
This leave the negative range & negative range case to be considered. We
know that negative range & negative range always yield a negative value,
so a preliminary guess would be S64_MIN. However, that guess is too
imprecise to help with the r0 <<= 62, r0 s>>= 63, r0 &= -13 pattern
we're trying to deal with here.
This can be further improve with the observation that for negative range
& negative range, the smallest possible value must be one that has
longest _common_ most-significant set '1' bits sequence, thus we can use
min(dst_reg->smin_value, src->smin_value) as the starting point, as the
smaller value will be the one with the shorter most-significant set '1'
bits sequence. But that alone is not enough, as we do not know whether
rest of the bits would be set, so the safest guess would be one that
clear alls bits after the most-significant set '1' bits sequence,
something akin to bit_floor(), but for rounding to a negative power-of-2
instead.
negative_bit_floor(0xffff000000000003) == 0xffff000000000000
negative_bit_floor(0xf0ff0000ffff0000) == 0xf000000000000000
negative_bit_floor(0xfffffb0000000000) == 0xfffff80000000000
With negative range & negative range solve, we now have:
| src_reg
smin = ? +----------------------------+---------------------------
| negative | non-negative
---------+--------------+----------------------------+---------------------------
| negative |negative_bit_floor( | 0
| | min(dst->smin, src->smin))|
dst_reg +--------------+----------------------------+---------------------------
| non-negative | 0 | 0
This can be further simplied since min(dst->smin, src->smin) < 0 when both
dst_reg and src_reg have a negative range. Which means using
negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value)
to calculate the resulting smin_value would work across all sign combinations.
Together these allows us to infer the signed range of the result of BPF_AND
operation using the signed range from its operands.
Hi Shung-Hsi,
This seems quite elegant.
As an additional check, I did a simple brute-force for all possible
ranges of 6-bit integers and bounds are computed safely.
Thanks for looking into this, as well as the complement.
Did took me quite awhile to try come up with a simple solution that
works just well enough without further complication, felt quite proud :)
On Tue, Jul 16, 2024 at 10:52 AM Shung-Hsi Yu [off-list ref] wrote:
quoted hunk
This commit teach the BPF verifier how to infer signed ranges directly
from signed ranges of the operands to prevent verifier rejection, which
is needed for the following BPF program's no-alu32 version, as shown by
Xu Kuohai:
SEC("lsm/bpf_map")
int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode)
{
if (map != (struct bpf_map *)&data_input)
return 0;
if (fmode & FMODE_WRITE)
return -EACCES;
return 0;
}
Where the relevant verifer log upon rejection are:
...
5: (79) r0 = *(u64 *)(r1 +8) ; R0_w=scalar() R1=ctx()
; if (fmode & FMODE_WRITE) @ test_libbpf_get_fd_by_id_opts.c:32
6: (67) r0 <<= 62 ; R0_w=scalar(smax=0x4000000000000000,umax=0xc000000000000000,smin32=0,smax32=umax32=0,var_off=(0x0; 0xc000000000000000))
7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
; @ test_libbpf_get_fd_by_id_opts.c:0
8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
9: (95) exit
This sequence of instructions comes from Clang's transformation located
in DAGCombiner::SimplifySelectCC() method, which combined the "fmode &
FMODE_WRITE" check with the return statement without needing BPF_JMP at
all. See Eduard's comment for more detail of this transformation[0].
While the verifier can correctly infer that the value of r0 is in a
tight [-1, 0] range after instruction "r0 s>>= 63", is was not able to
come up with a tight range for "r0 &= -13" (which would be [-13, 0]),
and instead inferred a very loose range:
r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
The reason is that scalar*_min_max_add() mainly relies on tnum for
interring value in register after BPF_AND, however [-1, 0] cannot be
tracked precisely with tnum, and effectively turns into [0, -1] (i.e.
tnum_unknown). So upon BPF_AND the resulting tnum is equivalent to
dst_reg->var_off = tnum_and(tnum_unknown, tnum_const(-13))
And from there the BPF verifier was only able to infer smin=S64_MIN,
smax=0x7ffffffffffffff3, which is outside of the expected [-4095, 0]
range for return values, and thus the program was rejected.
To allow verification of such instruction pattern, update
scalar*_min_max_and() to infer signed ranges directly from signed ranges
of the operands. With BPF_AND, the resulting value always gains more
unset '0' bit, thus it only move towards 0x0000000000000000. The
difficulty lies with how to deal with signs. While non-negative
(positive and zero) value simply grows smaller, a negative number can
grows smaller, but may also underflow and become a larger value.
To better address this situation we split the signed ranges into
negative range and non-negative range cases, ignoring the mixed sign
cases for now; and only consider how to calculate smax_value.
Since negative range & negative range preserve the sign bit, so we know
the result is still a negative value, thus it only move towards S64_MIN,
but never underflow, thus a save bet is to use a value in ranges that is
closet to 0, thus "max(dst_reg->smax_value, src->smax_value)". For
negative range & positive range the sign bit is always cleared, thus we
know the resulting is a non-negative, and only moves towards 0, so a
safe bet is to use smax_value of the non-negative range. Last but not
least, non-negative range & non-negative range is still a non-negative
value, and only moves towards 0; however same as the unsigned range
case, the maximum is actually capped by the lesser of the two, and thus
min(dst_reg->smax_value, src_reg->smax_value);
Listing out the above reasoning as a table (dst_reg abbreviated as dst,
src_reg abbreviated as src, smax_value abbrivated as smax) we get:
| src_reg
smax = ? +---------------------------+---------------------------
| negative | non-negative
---------+--------------+---------------------------+---------------------------
| negative | max(dst->smax, src->smax) | src->smax
dst_reg +--------------+---------------------------+---------------------------
| non-negative | dst->smax | min(dst->smax, src->smax)
However this is quite complicated, luckily it can be simplified given
the following observations
max(dst_reg->smax_value, src_reg->smax_value) >= src_reg->smax_value
max(dst_reg->smax_value, src_reg->smax_value) >= dst_reg->smax_value
max(dst_reg->smax_value, src_reg->smax_value) >= min(dst_reg->smax_value, src_reg->smax_value)
So we could substitute the cells in the table above all with max(...),
and arrive at:
| src_reg
smax' = ? +---------------------------+---------------------------
| negative | non-negative
---------+--------------+---------------------------+---------------------------
| negative | max(dst->smax, src->smax) | max(dst->smax, src->smax)
dst_reg +--------------+---------------------------+---------------------------
| non-negative | max(dst->smax, src->smax) | max(dst->smax, src->smax)
Meaning that simply using
max(dst_reg->smax_value, src_reg->smax_value)
to calculate the resulting smax_value would work across all sign combinations.
For smin_value, we know that both non-negative range & non-negative
range and negative range & non-negative range both result in a
non-negative value, so an easy guess is to use the minimum non-negative
value, thus 0.
| src_reg
smin = ? +----------------------------+---------------------------
| negative | non-negative
---------+--------------+----------------------------+---------------------------
| negative | ? | 0
dst_reg +--------------+----------------------------+---------------------------
| non-negative | 0 | 0
This leave the negative range & negative range case to be considered. We
know that negative range & negative range always yield a negative value,
so a preliminary guess would be S64_MIN. However, that guess is too
imprecise to help with the r0 <<= 62, r0 s>>= 63, r0 &= -13 pattern
we're trying to deal with here.
This can be further improve with the observation that for negative range
& negative range, the smallest possible value must be one that has
longest _common_ most-significant set '1' bits sequence, thus we can use
min(dst_reg->smin_value, src->smin_value) as the starting point, as the
smaller value will be the one with the shorter most-significant set '1'
bits sequence. But that alone is not enough, as we do not know whether
rest of the bits would be set, so the safest guess would be one that
clear alls bits after the most-significant set '1' bits sequence,
something akin to bit_floor(), but for rounding to a negative power-of-2
instead.
negative_bit_floor(0xffff000000000003) == 0xffff000000000000
negative_bit_floor(0xf0ff0000ffff0000) == 0xf000000000000000
negative_bit_floor(0xfffffb0000000000) == 0xfffff80000000000
With negative range & negative range solve, we now have:
| src_reg
smin = ? +----------------------------+---------------------------
| negative | non-negative
---------+--------------+----------------------------+---------------------------
| negative |negative_bit_floor( | 0
| | min(dst->smin, src->smin))|
dst_reg +--------------+----------------------------+---------------------------
| non-negative | 0 | 0
This can be further simplied since min(dst->smin, src->smin) < 0 when both
dst_reg and src_reg have a negative range. Which means using
negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value)
to calculate the resulting smin_value would work across all sign combinations.
Together these allows us to infer the signed range of the result of BPF_AND
operation using the signed range from its operands.
[0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/
Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/
Cc: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Shung-Hsi Yu <redacted>
---
kernel/bpf/verifier.c | 62 +++++++++++++++++++++++++++++--------------
1 file changed, 42 insertions(+), 20 deletions(-)
@@ -13466,6 +13466,39 @@ static void scalar_min_max_mul(struct bpf_reg_state *dst_reg,}}+/* Clears all trailing bits after the most significant unset bit.+*+*UsedforestimatingtheminimumpossiblevalueafterBPF_AND.This+*effectivelyroundsanegativevaluedowntoanegativepower-of-2value+*(exceptfor-1,whichjustreturn-1)andreturning0fornon-negative+*values.E.g.masked32_negative(0xff0ff0ff)==0xff000000.+*/+staticinlines32negative32_bit_floor(s32v)+{+/* XXX: per C standard section 6.5.7 right shift of signed negative+*valueisimplementation-defined.Shouldunsignedtypebeusedhere+*instead?+*/+v&=v>>1;+v&=v>>2;+v&=v>>4;+v&=v>>8;+v&=v>>16;+returnv;+}++/* Same as negative32_bit_floor() above, but for 64-bit signed value */+staticinlines64negative_bit_floor(s64v)+{+v&=v>>1;+v&=v>>2;+v&=v>>4;+v&=v>>8;+v&=v>>16;+v&=v>>32;+returnv;+}+staticvoidscalar32_min_max_and(structbpf_reg_state*dst_reg,structbpf_reg_state*src_reg){
@@ -13485,16 +13518,10 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,dst_reg->u32_min_value=var32_off.value;dst_reg->u32_max_value=min(dst_reg->u32_max_value,umax_val);-/* Safe to set s32 bounds by casting u32 result into s32 when u32-*doesn'tcrosssignboundary.Otherwisesets32boundstounbounded.-*/-if((s32)dst_reg->u32_min_value<=(s32)dst_reg->u32_max_value){-dst_reg->s32_min_value=dst_reg->u32_min_value;-dst_reg->s32_max_value=dst_reg->u32_max_value;-}else{-dst_reg->s32_min_value=S32_MIN;-dst_reg->s32_max_value=S32_MAX;-}+/* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */+dst_reg->s32_min_value=negative32_bit_floor(min(dst_reg->s32_min_value,+src_reg->s32_min_value));+dst_reg->s32_max_value=max(dst_reg->s32_max_value,src_reg->s32_max_value);}staticvoidscalar_min_max_and(structbpf_reg_state*dst_reg,
@@ -13515,16 +13542,11 @@ static void scalar_min_max_and(struct bpf_reg_state *dst_reg,dst_reg->umin_value=dst_reg->var_off.value;dst_reg->umax_value=min(dst_reg->umax_value,umax_val);-/* Safe to set s64 bounds by casting u64 result into s64 when u64-*doesn'tcrosssignboundary.Otherwisesets64boundstounbounded.-*/-if((s64)dst_reg->umin_value<=(s64)dst_reg->umax_value){-dst_reg->smin_value=dst_reg->umin_value;-dst_reg->smax_value=dst_reg->umax_value;-}else{-dst_reg->smin_value=S64_MIN;-dst_reg->smax_value=S64_MAX;-}+/* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */+dst_reg->smin_value=negative_bit_floor(min(dst_reg->smin_value,+src_reg->smin_value));+dst_reg->smax_value=max(dst_reg->smax_value,src_reg->smax_value);+/* We may learn something more from the var_off */__update_reg_bounds(dst_reg);}--
2.45.2
Apologies for the late response and thank you for CCing us Shung-Hsi.
The patch itself seems well thought out and looks correct. Great work!
We quickly checked your patch using Agni [1], and were not able to find any
violations. That is, given well-formed register state inputs to
adjust_scalar_min_max_vals, the new algorithm always produces sound outputs
for the BPF_AND (both 32/64) instruction.
It looks like you already performed tests with Z3, and Eduard performed a
brute force testing using 6-bit integers. Agni's result stands as an
additional stronger guarantee because Agni generates SMT formulas directly
from the C source code of the verifier and checks the correctness in Z3
without any external library functions, it uses full 64-bit size bitvectors
in the formulas generated and considers the correctness for 64-bit integer
inputs, and finally it considers the correctness of the *final* output
abstract values generated after running update_reg_bounds() and
reg_bounds_sync().
Using Agni's encodings we were also quickly able to check the precision of
the new algorithm. An algorithm is more precise if it produces tighter
range bounds, while being correct. We are happy to note that the new
algorithm produces outputs that are at least as precise or more precise
than the old algorithm, for all well-formed register state inputs.
Best,
Hari
[1] https://github.com/bpfverif/agni
Hi Harishankar,
On Sun, Jul 28, 2024 at 06:38:40PM GMT, Harishankar Vishwanathan wrote:
On Tue, Jul 16, 2024 at 10:52 AM Shung-Hsi Yu [off-list ref] wrote:
quoted
This commit teach the BPF verifier how to infer signed ranges directly
from signed ranges of the operands to prevent verifier rejection, which
is needed for the following BPF program's no-alu32 version, as shown by
Xu Kuohai:
[...]
Apologies for the late response and thank you for CCing us Shung-Hsi.
The patch itself seems well thought out and looks correct. Great work!
Thanks! :)
We quickly checked your patch using Agni [1], and were not able to find any
violations. That is, given well-formed register state inputs to
adjust_scalar_min_max_vals, the new algorithm always produces sound outputs
for the BPF_AND (both 32/64) instruction.
That is great to hear and really boost the level of confidence. Though I
did made an update[1] to the patch such that implementation of
negative_bit_floor() is change from
v &= v >> 1;
v &= v >> 2;
v &= v >> 4;
v &= v >> 8;
v &= v >> 16;
v &= v >> 32;
return v;
to one that closer resembles tnum_range()
u8 bits = fls64(~v); /* find most-significant unset bit */
u64 delta;
/* special case, needed because 1ULL << 64 is undefined */
if (bits > 63)
return 0;
delta = (1ULL << bits) - 1;
return ~delta;
My understanding is that the two implementations should return the same
output for the same input, so overall the deduction remains the same.
And my simpler test with Z3 does not find violation in the new
implementation. But it would be much better if we can have Agni check
the new implementation for violation as well.
Speak of which, would you and others involved in checking this patch be
comfortable with adding a formal acknowledgment[2] for the patch so this
work can be credited in the git repo as well? (i.e. usually replying
with an Acked-by, other alternatives are Reviewed-by and Tested-by)
IMHO the work done here is in the realm of Reviewed-by, but that itself
comes with other implications[3], which may or may not be wanted
depending on individual's circumstances.
I'll probably post the updated patch out next week, changing only the
comments in [1].
It looks like you already performed tests with Z3, and Eduard performed a
brute force testing using 6-bit integers. Agni's result stands as an
additional stronger guarantee because Agni generates SMT formulas directly
from the C source code of the verifier and checks the correctness in Z3
without any external library functions, it uses full 64-bit size bitvectors
in the formulas generated and considers the correctness for 64-bit integer
inputs, and finally it considers the correctness of the *final* output
abstract values generated after running update_reg_bounds() and
reg_bounds_sync().
I had some vague ideas that Agni provides better guarantee, but did not
know exactly what they are. Thanks for the clear explanation on the
additional guarantee Agni provides; its especially assuring to know that
update_reg_bounds() and reg_bounds_sync() have been taken into account.
Using Agni's encodings we were also quickly able to check the precision of
the new algorithm. An algorithm is more precise if it produces tighter
range bounds, while being correct. We are happy to note that the new
algorithm produces outputs that are at least as precise or more precise
than the old algorithm, for all well-formed register state inputs.
On Tue, Jul 30, 2024 at 12:26 AM Shung-Hsi Yu [off-list ref] wrote:
[...]
That is great to hear and really boost the level of confidence. Though I
did made an update[1] to the patch such that implementation of
negative_bit_floor() is change from
v &= v >> 1;
v &= v >> 2;
v &= v >> 4;
v &= v >> 8;
v &= v >> 16;
v &= v >> 32;
return v;
to one that closer resembles tnum_range()
u8 bits = fls64(~v); /* find most-significant unset bit */
u64 delta;
/* special case, needed because 1ULL << 64 is undefined */
if (bits > 63)
return 0;
delta = (1ULL << bits) - 1;
return ~delta;