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
