[$] Formally verifying the BPF verifier
Date:
Fri, 23 May 2025 14:34:00 +0000
Description:
The BPF verifier is an increasingly complex and security-critical piece of code.
When the kinds of people who are apt to work on BPF see a situation like that, they naturally question whether it's possible to use formal verification to ensure that the implementation of the code in question is correct. Santosh Nagarakatte led the first of two extra-long sessions in the BPF track
of the 2025 Linux Storage, Filesystem, Memory Management, and BPF Summit
about his team's work formally verifying the BPF verifier with a
custom tool called Agni .
======================================================================
Link to news story:
https://lwn.net/Articles/1020664/
--- Mystic BBS v1.12 A47 (Linux/64)
* Origin: tqwNet UK HUB @ hub.uk.erb.pw (1337:1/100)