Re: [PATCH 1/4] lib/crypto: Add ML-DSA verification support

["Jason A. Donenfeld" <Jason@zx2c4.com>]

Hi Hanno,

Just to add to what Eric said...

On Sat, Nov 29, 2025 at 04:19:11PM -0800, Eric Biggers wrote:
> I think you may be underestimating how much the requirements of the
> kernel differ from userspace.  Consider the following:

I've added a bit of formally verified code to the kernel, and also
ported some userspace crypto. In these cases, I wound up working with
the authors of the code to make it more suitable to the requirements of
kernel space -- even down to the formatting level. For example, the
HACL* project needed some changes to KReMLin to make the variety of code
fit into what the kernel expected. Andy Polyakov's code needed some
internal functions exposed so that the kernel could do cpu capability
based dispatch. And so on and so forth. There's always _something_.

I'd love to have a formally verified ML-DSA implementation (if we're to
have ML-DSA in the kernel anyhow, but it looks like that's happening).
But I almost guarantee that it's going to be some work to do. If those
are efforts you'd consider undertaking seriously, I'd be happy to assist
or help guide the considerations.

There's also another approach, which would be to formally verify Eric's
code, perhaps even using the same techniques as your own project, via
CBMC and such. In this case, the name of the game is usually to port the
kernel code to userspace. That generally winds up being a matter of
shimming out some headers and adding a few typedefs. There's a decent
amount of kernel test code or kernel tool code that does this, and lots
of shim headers already in the kernel that can be borrowed for this. But
usually, at least for crypto code, you can figure it out pretty quickly
by just trying to compile it and plugging the missing headers and types
as they come up.

The model checking might be more work with this latter approach, since
it's not already done like it is for the former, but the porting work is
probably much less arduous.

Anyway, the bigger picture is that I'm very enthusiastic about getting
formally verified crypto in the kernel, so these types of efforts are
really very appreciated and welcomed. But it just takes a bit more work
than usual.

Jason