[LSF/MM/BPF TOPIC] Value Tracking in Verifier

[Shung-Hsi Yu <shung-hsi.yu@suse.com>]

Hello,

I'd like propose a discussion about BPF verifier itself. To avoid being too
vague, this proposition limits to value tracking (i.e. var_off and
*{min,max}_value in bpf_reg_state); taking a very brief look at the
challenges of current implementation, and maybe alternative implementation
like PREVAIL[1]. Before heading on to the actual discussion:
- Unify signed and unsigned min/max tracking[2]
- Refactor value tracking routines (as set-operations)
- Tracking relation between values

Admittedly the current topic is a rather narrowly scoped. The discussion
could be further expanded to be about the verifier in general as needed,
some (less concrete) ideas to discuss:
- Further reducing loop/branch states
- Lazier precision tracking
- Simplification/refactoring of codebase
- Documentation improvement


Thanks,
Shung-Hsi Yu

1: https://vbpf.github.io/
2: https://lore.kernel.org/bpf/20231108054611.19531-1-shung-hsi.yu@suse.com/