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 <[email protected]> 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/[email protected]?part=18
