Hi Sasha,
On Sun, 15 Mar 2026 at 07:36, Sasha Levin <[email protected]> wrote:
> 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...
The actual E-values are positive, so I guess you want e.g. -EPERM?
Note that the actual errno values are architecture-specific.
E.g. EOPNOTSUPP can be 45, 95, 122, or 223.
Gr{oetje,eeting}s,
Geert
--
Geert Uytterhoeven -- There's lots of Linux beyond ia32 -- [email protected]
In personal conversations with technical people, I call myself a hacker. But
when I'm talking to journalists I just say "programmer" or something like that.
-- Linus Torvalds
