Subj : [$] Formally verifying the BPF verifier
To   : All
From : LWN.net
Date : Fri May 23 2025 15:45:09

[$] 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)

.