On Sat, Mar 14, 2026 at 11:18:22AM -0700, Jakub Kicinski wrote:
On Fri, 13 Mar 2026 11:09:10 -0400 Sasha Levin wrote:
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.
Once the API is in a machine-readable format, we can write formatters to
output whatever downstream tools need. The kapi tool in the series
already ships with plain text, JSON, and RST formatters, and adding new
output formats is straightforward. We don't need to convince the
syzkaller folks to consume our specs, we can just output them in a
format that syzkaller already understands.
For example, I have a syzlang formatter that produces the following
from the sys_read spec in this series:
# --- read ---
# Read data from a file descriptor
#
# @context process, sleepable
#
# @capability CAP_DAC_OVERRIDE: Bypass discretionary access control on read
permission
# @capability CAP_DAC_READ_SEARCH: Bypass read permission checks on regular
files
#
# @error EPERM (-1): Returned by fanotify permission events...
# @error EINTR (-4): The call was interrupted by a signal before any data was
read.
# @error EIO (-5): A low-level I/O error occurred.
# @error EBADF (-9): fd is not a valid file descriptor, or fd was not opened
for reading.
# @error EAGAIN (-11): O_NONBLOCK set and read would block.
# @error EACCES (-13): LSM denied the read operation via
security_file_permission().
# @error EFAULT (-14): buf points outside the accessible address space.
# @error EISDIR (-21): fd refers to a directory.
# @error EINVAL (-22): fd not suitable for reading, O_DIRECT misaligned,
count negative...
# @error ENODATA (-61): Data not available in cache...
# @error EOVERFLOW (-75): File position plus count would exceed LLONG_MAX.
# @error EOPNOTSUPP (-95): Read not supported for this file type...
# @error ENOBUFS (-105): Buffer too small for complete notification...
#
# @constraint MAX_RW_COUNT: actual_count = min(count, MAX_RW_COUNT)
# @constraint File must be open for reading: (file->f_mode & FMODE_READ) &&
(file->f_mode & FMODE_CAN_READ)
#
# @signal Any signal: restartable, error=-4
#
# @lock file->f_pos_lock (mutex, internal): For seekable files with
FMODE_ATOMIC_POS
# @lock Filesystem-specific locks (rwlock, internal)
# @lock RCU read-side (rwlock, internal): File descriptor lookup protection
#
# @side-effect file->f_pos: f_pos advanced by bytes read [conditional,
irreversible]
# @side-effect inode access time: atime updated unless O_NOATIME
[conditional, irreversible]
# @side-effect task I/O accounting: rchar and syscr updated [conditional,
irreversible]
# @side-effect fsnotify events: FS_ACCESS event generated [conditional,
irreversible]
#
# @return ssize_t: bytes read on success, negative errno on error
#
read(fd fd, buf ptr[out, buffer[out]], count len[buf]) intptr
That said, I don't have a strong end-to-end example with the 4 syscalls
proposed here, as open/close/read/write don't take complex structures,
and the subsystems underneath them aren't specced yet. The value becomes
clearer with richer interfaces where the gap between "we know the type
signature" and "we know the full behavioral contract" is much wider.
--
Thanks,
Sasha
