Re: [RFC PATCH 18/20] verification/rvgen: Add support for BPF monitors

[sashiko-bot@kernel.org]

Thank you for your contribution! Sashiko AI review found 1 potential issue(s) to consider:
- [Medium] Generated BPF monitor arrays for state and event names lack null termination if names are 32 characters or longer, leading to out-of-bounds reads.
--

commit 53fecfe68f54b9383a7c0b099f9a1311ed5ff3ef
Author: Gabriele Monaco <gmonaco@redhat.com>

verification/rvgen: Add support for BPF monitors

This commit adds the -b flag to the rvgen monitor tool to generate BPF
monitors for deterministic automata. It updates the code generator to emit
BPF-compatible array structures and hooks while maintaining the existing
in-kernel monitor support.

> diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
> index 22938ce1bf6cb..5be9fe44a19b2 100644
> --- a/tools/verification/rvgen/rvgen/dot2c.py
> +++ b/tools/verification/rvgen/rvgen/dot2c.py
> @@ -111,10 +111,17 @@ class Dot2c(Automata):
>          min_type = self.get_minimun_type()
>          buff = []
>          buff.append(f"struct {self.struct_automaton_def} {{")
> -        buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];")
> -        buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];")
> -        if self.is_hybrid_automata():
> -            buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];")
> +        if self.bpf:
> +            # BPF struggles with non-fixed string pointers
> +            buff.append(f"\tchar state_names[state_max{self.enum_suffix}][32];")
> +            buff.append(f"\tchar event_names[event_max{self.enum_suffix}][32];")
> +            if self.is_hybrid_automata():
> +                buff.append(f"\tchar env_names[env_max{self.enum_suffix}][32];")

[Severity: Medium]
Could this lead to out-of-bounds reads in BPF trace output if the monitor
model has state or event names of 32 characters or longer?

When a fixed-size character array is initialized with a string literal equal
to or larger than its size, the null terminator is silently omitted in C.
If the names generated from the model are exactly 32 bytes or longer, these
arrays will lack a null terminator.

Since the BPF verifier permits reading .rodata, string formatting helpers
reading from these fields could run past the array bounds until a null byte
is encountered in adjacent memory. This could cause garbled trace output and
a minor info leak.

Would it make sense to enforce truncation of the source string during
generation, or explicitly ensure null termination here?

> +        else:
> +            buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];")
> +            buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];")

-- 
Sashiko AI review · https://sashiko.dev/#/patchset/20260831090524.106845-1-gmonaco@redhat.com?part=18