On Sat, 14 Mar 2026 at 19:18, Jakub Kicinski [off-list ref] wrote:
On Fri, 13 Mar 2026 11:09:10 -0400 Sasha Levin wrote:
quoted
This enables static analysis tools to verify userspace API usage at compile
time, test generation based on formal specifications, consistent error handling
validation, automated documentation generation, and formal verification of
kernel interfaces.
Could you give some examples? We have machine readable descriptions for
Netlink interfaces, we approached syzbot folks and they did not really
seem to care for those.
I think our reasoning wrt syzkaller was that not all interfaces in all
relevant kernels are described with netlink yml descriptions, so we
need to continue using the extraction of interfaces from the source
code. And if we have that code, then using yml as an additional data
source only adds code/complexity. Additionally, we may extract some
extra constraints/info from code that are not present in yml.
Realistically system call descriptions may have the same problem for
us at this point, since we extract lots of info from the source code
already:
https://raw.githubusercontent.com/google/syzkaller/refs/heads/master/sys/linux/auto.txt
(and LLMs obviously can allow us to extract more)