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: <6983015e-4d6a-44d4-9f2e-203688263018@ralfj.de>
Date: Wed, 26 Feb 2025 17:10:49 +0100
From: Ralf Jung <post@...fj.de>
To: Ventura Jack <venturajack85@...il.com>
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)

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