On Mon, 12 Oct 2026 18:18:52 +0200 Tobias Schaffner <[email protected]> wrote:
> Regarding verification: > The path I verify is deliberately kept short and simple. RV fits well > because the probe is a plain function call and the state update is a > try_cmpxchg that cannot fail, so it adds very little. A BPF program > brings more machinery into the probe path doesn't it? I fear that adding > this would force me to verify that the new RV system does not change the > behavior of the system we are trying to verify, and I suspect that could > be harder than verifying the system itself. 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). 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. Maybe the safety-critical project was canceled and this is no longer needed. -- Steve
