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: <7ab2de35-8fc8-42cf-9464-81384e227dba@ralfj.de>
Date: Wed, 26 Feb 2025 22:39:28 +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,

>> 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.

VeriFast people are working on Tree Borrows integration, and Gillian-Rust people 
also have some plans if I remember correctly. For the rest, I am not aware of 
plans, but that doesn't mean there aren't any. :)

> On the other hand, RefinedRust reuses code from Miri.

No, it does not use code from Miri, it is based on RustBelt -- my PhD thesis 
where I formalized a (rather abstract) version of the borrow checker in Coq/Rocq 
(i.e., in a tool for machine-checked proofs) and manually proved some pieces of 
small but tricky unsafe code to be sound.

> 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.

Yeah it's all very much work-in-progress research largely driven by small 
academic groups, and at some point industry collaboration will become crucial to 
actually turn these into usable products, but there's at least a lot of exciting 
starting points. :)

Kind regards,
Ralf