Re: [PATCH 0/9] Kernel API Specification Framework

[Sasha Levin <sashal@kernel.org>]

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