linux-kernel - Re: C aggregate passing (Rust kernel policy)

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <CAFJgqgTJ+GBvdkZf4bPHPoUgJj5ZzENZaLzVV2bnDOEG+3OMtw@mail.gmail.com>
Date: Wed, 26 Feb 2025 09:50:44 -0700
From: Ventura Jack <venturajack85@...il.com>
To: Ralf Jung <post@...fj.de>
Cc: Alice Ryhl <aliceryhl@...gle.com>, Linus Torvalds <torvalds@...ux-foundation.org>, 
	Kent Overstreet <kent.overstreet@...ux.dev>, Gary Guo <gary@...yguo.net>, airlied@...il.com, 
	boqun.feng@...il.com, david.laight.linux@...il.com, ej@...i.de, 
	gregkh@...uxfoundation.org, hch@...radead.org, hpa@...or.com, 
	ksummit@...ts.linux.dev, linux-kernel@...r.kernel.org, 
	miguel.ojeda.sandonis@...il.com, rust-for-linux@...r.kernel.org
Subject: Re: C aggregate passing (Rust kernel policy)

On Wed, Feb 26, 2025 at 9:10 AM Ralf Jung <post@...fj.de> wrote:
>
> Hi,
>
> >> [Omitted] (However, verification tools are
> >> in the works as well, and thanks to Miri we have a very good idea of what
> >> exactly it is that these tools have to check for.) [Omitted]
> >
> > Verification as in static verification? That is some interesting and
> > exciting stuff if so.
>
> Yes. There's various projects, from bounded model checkers (Kani) that can
> "only" statically guarantee "all executions that run loops at most N times are
> fine" to full-fledged static verification tools (Gillian-Rust, VeriFast, Verus,
> Prusti, RefinedRust -- just to mention the ones that support unsafe code). None
> of the latter tools is production-ready yet, and some will always stay research
> prototypes, but there's a lot of work going on, and having a precise model of
> the entire Abstract Machine that is blessed by the compiler devs (i.e., Miri) is
> a key part for this to work. It'll be even better when this Abstract Machine
> exists not just implicitly in Miri but explicitly in a Rust Specification, and
> is subject to stability guarantees -- and we'll get there, but it'll take some
> more time. :)
>
> Kind regards,
> Ralf
>

Thank you for the answer. Almost all of those projects look active,
though Prusti's GitHub repository has not had commit activity for many
months. Do you know if any of the projects are using stacked borrows
or tree borrows yet? Gillian-Rust does not seem to use stacked borrows
or tree borrows. Verus mentions stacked borrows in "related work" in
one paper. On the other hand, RefinedRust reuses code from Miri.

It does sound exciting. It reminds me in some ways of Scala. Though
also like advanced research where some practical goals for the
language (Rust) have not yet been reached.

Best, VJ.