Re: [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors

[Gabriele Monaco <gmonaco@redhat.com>]

On Mon, 2026-10-12 at 15:21 -0400, Steven Rostedt wrote:
> This brings back memories of conversations I had with Daniel. When asked
> about how this is being used in formal verification of safety critical
> systems, he told me that only the RV verifier itself needed to be verified
> and to show what it is verifying can be verified via it. For example,
> running Linux in autonomous vehicles handling critical systems the watchdog
> had to be verified that it could catch lockups. As the watchdog would
> trigger fail-safe mode if something went wrong. RV would be monitoring the
> watchdog and if RV detected something it would panic the machine, which
> would immediately force the vehicle into fail-safe mode (stop lots of
> features and only keep those that can stop the vehicle safely).

Yeah I talked to the same people working on that project, eventually there were
more problems like verifying RV can't be affected by the code it's verifying.
This is still an open problem though.

> Can using BPF as the RV verifier be formally verified? As verification for
> RV monitors did look at the binary. Is BPF optimized to machine language
> before it enters the kernel? If not, can we formally verify the BPF
> verifier created the correct binary? Maybe, I don't know.

As far as I understand, verifying the BPF verifier would take an insane amount
of work, the go-to approach is manually validating only the code you know you
are running. Let's say up to a point where you can realistically say it behaves
like you want it to.
In short, having a verifier doesn't add much value here, at least until someone
verifies that too.

Then there are the levels of indirection, BPF C code gets compiled to BPF
bytecode and that gets JIT compiled inside the kernel. Now it's machine code.

If people are normally not validating clang/gcc produce machine code consistent
to the verified source code, this case should be equivalent, but I'm just
speculating here.

Gabriele