Message ID | 20240719110059.797546-6-xukuohai@huaweicloud.com (mailing list archive) |
---|---|
State | Handled Elsewhere |
Delegated to: | Paul Moore |
Headers | show |
Series | Add BPF LSM return value range check, BPF part | expand |
On Fri, 2024-07-19 at 19:00 +0800, Xu Kuohai wrote: > From: Shung-Hsi Yu <shung-hsi.yu@suse.com> [...] > > | src_reg > smin' = ? +----------------------------+--------------------------- > smin'(r) <= smin(r) | negative | non-negative > ---------+--------------+----------------------------+--------------------------- > | negative |negative_bit_floor( |negative_bit_floor( > | | min(dst->smin, src->smin))| min(dst->smin, src->smin)) > dst_reg +--------------+----------------------------+--------------------------- > | non-negative |negative_bit_floor( |negative_bit_floor( > | | min(dst->smin, src->smin))| min(dst->smin, src->smin)) > > Meaning that simply 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 the BPF verifier to infer the signed range of the > result of BPF_AND operation using the signed range from its operands, > and use that information > > r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0) > r0 &= -13 ; R0_w=scalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) > > [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 <shung-hsi.yu@suse.com> > Acked-by: Xu Kuohai <xukuohai@huawei.com> > --- I find derivation of these new rules logical. Also tried a simple brute force testing of this algorithm for 6-bit signed integers, and have not found any constraint violations: https://github.com/eddyz87/bpf-and-brute-force-check As a nitpick, I think that it would be good to have some shortened version of the derivation in the comments alongside the code. (Maybe with a link to the mailing list). Acked-by: Eduard Zingerman <eddyz87@gmail.com> [...]
On Mon, Jul 22, 2024 at 12:13:20AM GMT, Eduard Zingerman wrote: > On Fri, 2024-07-19 at 19:00 +0800, Xu Kuohai wrote: > > From: Shung-Hsi Yu <shung-hsi.yu@suse.com> > > [...] > > > > > | src_reg > > smin' = ? +----------------------------+--------------------------- > > smin'(r) <= smin(r) | negative | non-negative > > ---------+--------------+----------------------------+--------------------------- > > | negative |negative_bit_floor( |negative_bit_floor( > > | | min(dst->smin, src->smin))| min(dst->smin, src->smin)) > > dst_reg +--------------+----------------------------+--------------------------- > > | non-negative |negative_bit_floor( |negative_bit_floor( > > | | min(dst->smin, src->smin))| min(dst->smin, src->smin)) > > > > Meaning that simply 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 the BPF verifier to infer the signed range of the > > result of BPF_AND operation using the signed range from its operands, > > and use that information I accidentally left the above paragraph unfinished, it should end with ... and using that information, it can be sure that that the result of [-1, 0] & -13 will be within that expected range of [-4095, 0]. > > r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0) > > r0 &= -13 ; R0_w=scalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) > > > > [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 <shung-hsi.yu@suse.com> > > Acked-by: Xu Kuohai <xukuohai@huawei.com> > > --- > > I find derivation of these new rules logical. > Also tried a simple brute force testing of this algorithm for 6-bit > signed integers, and have not found any constraint violations: > https://github.com/eddyz87/bpf-and-brute-force-check Thanks! > As a nitpick, I think that it would be good to have some shortened > version of the derivation in the comments alongside the code. Agree it would. Will try to add a 2-4 sentence explanation. > (Maybe with a link to the mailing list). Adding a link to the mailing list seems out of the usual for comment in verifier.c though, and it would be quite long. That said, it would be nice to hint that there exists a more verbose version of the explanation. Maybe an explicit "see commit for the full detail" at the end of the added comment? > Acked-by: Eduard Zingerman <eddyz87@gmail.com> > > [...] Will send an update for this tomorrow.
On Mon, 2024-07-22 at 20:57 +0800, Shung-Hsi Yu wrote: [...] > > As a nitpick, I think that it would be good to have some shortened > > version of the derivation in the comments alongside the code. > > Agree it would. Will try to add a 2-4 sentence explanation. > > > (Maybe with a link to the mailing list). > > Adding a link to the mailing list seems out of the usual for comment in > verifier.c though, and it would be quite long. That said, it would be > nice to hint that there exists a more verbose version of the > explanation. > > Maybe an explicit "see commit for the full detail" at the end of > the added comment? Tbh, I find bounds deduction code extremely confusing. Imho, having lengthy comments there is a good thing.
On Mon, Jul 22, 2024 at 11:48 AM Eduard Zingerman <eddyz87@gmail.com> wrote: > > On Mon, 2024-07-22 at 20:57 +0800, Shung-Hsi Yu wrote: > > [...] > > > > As a nitpick, I think that it would be good to have some shortened > > > version of the derivation in the comments alongside the code. > > > > Agree it would. Will try to add a 2-4 sentence explanation. > > > > > (Maybe with a link to the mailing list). > > > > Adding a link to the mailing list seems out of the usual for comment in > > verifier.c though, and it would be quite long. That said, it would be > > nice to hint that there exists a more verbose version of the > > explanation. > > > > Maybe an explicit "see commit for the full detail" at the end of > > the added comment? > > Tbh, I find bounds deduction code extremely confusing. > Imho, having lengthy comments there is a good thing. +1 Pls document the logic in the code. commit log is good, but good chunk of it probably should be copied as a comment. I've applied the rest of the patches and removed 'test 3' selftest. Pls respin this patch and a test. More than one test would be nice too.
On Mon, Jul 22, 2024 at 05:48:22PM GMT, Alexei Starovoitov wrote: > On Mon, Jul 22, 2024 at 11:48 AM Eduard Zingerman <eddyz87@gmail.com> wrote: > > On Mon, 2024-07-22 at 20:57 +0800, Shung-Hsi Yu wrote: > > > > [...] > > > > > > As a nitpick, I think that it would be good to have some shortened > > > > version of the derivation in the comments alongside the code. > > > > > > Agree it would. Will try to add a 2-4 sentence explanation. > > > > > > > (Maybe with a link to the mailing list). > > > > > > Adding a link to the mailing list seems out of the usual for comment in > > > verifier.c though, and it would be quite long. That said, it would be > > > nice to hint that there exists a more verbose version of the > > > explanation. > > > > > > Maybe an explicit "see commit for the full detail" at the end of > > > the added comment? > > > > Tbh, I find bounds deduction code extremely confusing. > > Imho, having lengthy comments there is a good thing. > > +1 > Pls document the logic in the code. > commit log is good, but good chunk of it probably should be copied > as a comment. > > I've applied the rest of the patches and removed 'test 3' selftest. > Pls respin this patch and a test. > More than one test would be nice too. Ack. Will send send another series that: 1. update current patch - add code comment explanation how signed ranges are deduced in scalar*_min_max_and() - revert 229d6db14942 "selftests/bpf: Workaround strict bpf_lsm return value check." 2. reintroduce Xu Kuohai's "test 3" into verifier_lsm.c 3. add a few tests for BPF_AND's signed range deduction - should it be added to verifier_bounds*.c or verifier_and.c? I think former, because if we later add signed range deduction for BPF_OR as well, then test for signed range deducation of both BPF_AND and BPF_OR can live in the same file, which would be nice as signed range deduction of the two are somewhat symmetric
On Tue, Jul 23, 2024 at 02:36:18PM GMT, Shung-Hsi Yu wrote: [...] > > +1 > > Pls document the logic in the code. > > commit log is good, but good chunk of it probably should be copied > > as a comment. > > > > I've applied the rest of the patches and removed 'test 3' selftest. > > Pls respin this patch and a test. > > More than one test would be nice too. > > Ack. Will send send another series that: > > 1. update current patch > - add code comment explanation how signed ranges are deduced in > scalar*_min_max_and() > - revert 229d6db14942 "selftests/bpf: Workaround strict bpf_lsm return > value check." > 2. reintroduce Xu Kuohai's "test 3" into verifier_lsm.c > 3. add a few tests for BPF_AND's signed range deduction > - should it be added to verifier_bounds*.c or verifier_and.c? > > I think former, because if we later add signed range deduction for > BPF_OR as well... I was curious whether there would be imminent need for signed range deduction for BPF_OR, though looks like there is _not_. Looking at DAGCombiner::SimplifySelectCC() it does not do the bitwise-OR variant of what we've encountered[1,2], that is fold (select_cc seteq (and x, y), 0, A, -1) -> (or (sra (shl x)) A) In other words, transforming the following theoretial C code that returns -EACCES when certain bit is unset, and -1 when certain bit is set if (fmode & FMODE_WRITE) return -1; return -EACCESS; into the following instructions r0 <<= 62 r0 s>>= 63 /* set => r0 = -1, unset => r0 = 0 */ r0 |= -13 /* set => r0 = (-1 | -13) = -1, unset => r0 = (0 | -13) = -13 = -EACCESS */ exit /* returns either -1 or -EACCESS */ So signed ranged deduction with BPF_OR is probably just a nice-to-have for now. 1: https://github.com/llvm/llvm-project/blob/2b78303/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L27657-L27684 2: neither was the setne version transformed, i.e. fold (select_cc setne (and x, y), 0, A, 0) -> (and (sra (shl x)) A) > then test for signed range deducation of both > BPF_AND and BPF_OR can live in the same file, which would be nice > as signed range deduction of the two are somewhat symmetric
On Tue, Jul 23, 2024 at 12:07 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote: > > On Tue, Jul 23, 2024 at 02:36:18PM GMT, Shung-Hsi Yu wrote: > [...] > > > +1 > > > Pls document the logic in the code. > > > commit log is good, but good chunk of it probably should be copied > > > as a comment. > > > > > > I've applied the rest of the patches and removed 'test 3' selftest. > > > Pls respin this patch and a test. > > > More than one test would be nice too. > > > > Ack. Will send send another series that: > > > > 1. update current patch > > - add code comment explanation how signed ranges are deduced in > > scalar*_min_max_and() > > - revert 229d6db14942 "selftests/bpf: Workaround strict bpf_lsm return > > value check." > > 2. reintroduce Xu Kuohai's "test 3" into verifier_lsm.c > > 3. add a few tests for BPF_AND's signed range deduction > > - should it be added to verifier_bounds*.c or verifier_and.c? > > > > I think former, because if we later add signed range deduction for > > BPF_OR as well... > > I was curious whether there would be imminent need for signed range > deduction for BPF_OR, though looks like there is _not_. > > Looking at DAGCombiner::SimplifySelectCC() it does not do the > bitwise-OR variant of what we've encountered[1,2], that is > > fold (select_cc seteq (and x, y), 0, A, -1) -> (or (sra (shl x)) A) > > In other words, transforming the following theoretial C code that > returns -EACCES when certain bit is unset, and -1 when certain bit is > set > > if (fmode & FMODE_WRITE) > return -1; > > return -EACCESS; > > into the following instructions > > r0 <<= 62 > r0 s>>= 63 /* set => r0 = -1, unset => r0 = 0 */ > r0 |= -13 /* set => r0 = (-1 | -13) = -1, unset => r0 = (0 | -13) = -13 = -EACCESS */ > exit /* returns either -1 or -EACCESS */ > > So signed ranged deduction with BPF_OR is probably just a nice-to-have > for now. Yeah. Let's not complicate the verifier until really necessary. But I wonder whether we should override shouldFoldSelectWithSingleBitTest() in the backend to suppress this optimization. I guess not, since removal of a branch is a good thing.
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c index 78104bd85274..d3f3a464a871 100644 --- a/kernel/bpf/verifier.c +++ b/kernel/bpf/verifier.c @@ -13511,6 +13511,40 @@ static void scalar_min_max_mul(struct bpf_reg_state *dst_reg, } } +/* Clears all trailing bits after the most significant unset bit. + * + * Used for estimating the minimum possible value after BPF_AND. This + * effectively rounds a negative value down to a negative power-of-2 value + * (except for -1, which just return -1) and returning 0 for non-negative + * values. E.g. negative32_bit_floor(0xff0ff0ff) == 0xff000000. + */ +static inline s32 negative32_bit_floor(s32 v) +{ + u8 bits = fls(~v); /* find most-significant unset bit */ + u32 delta; + + /* special case, needed because 1UL << 32 is undefined */ + if (bits > 31) + return 0; + + delta = (1UL << bits) - 1; + return ~delta; +} + +/* Same as negative32_bit_floor() above, but for 64-bit signed value */ +static inline s64 negative_bit_floor(s64 v) +{ + 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; +} + static void scalar32_min_max_and(struct bpf_reg_state *dst_reg, struct bpf_reg_state *src_reg) { @@ -13530,16 +13564,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; - } + /* Handle the [-1, 0] & -CONSTANT case that's difficult for tnum */ + 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, @@ -13560,16 +13588,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; - } + /* Handle the [-1, 0] & -CONSTANT case that's difficult for tnum */ + 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); }