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.

That is great to hear as well. I really should try Agni myself, hope I
could find time in the near future.

Cheers,
Shung-Hsi

1: https://lore.kernel.org/bpf/20240719081702.137173-1-shung-hsi.yu@suse.com/ (local)
2: https://www.kernel.org/doc/html/v6.9/process/submitting-patches.html#when-to-use-acked-by-cc-and-co-developed-by
3: https://www.kernel.org/doc/html/v6.9/process/submitting-patches.html#reviewer-s-statement-of-oversight