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

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

[Shung-Hsi Yu]

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/

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

[John Fastabend]

Shung-Hsi Yu wrote:
> 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

Sounds interesting to me. Just creating a summarized list of the examples
that have forced the signed/unsigned separation would be valuable and the
reasons why we have both var_off and min,max would be a nice document.
The examples would show why the bit tracking and min/max has resisted
easily being unified.

> 
> 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/
>