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: <43074b70-c421-411f-b0bd-969c45f01466@ralfj.de>
Date: Thu, 27 Feb 2025 16:32:08 +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 VJ,

>> 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.
> 
> I see, the reason why I claimed it was because
> 
>      https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev
>          "We currently re-use code from the following projects:
>          miri: https://github.com/rust-lang/miri (under the MIT license)"
> 
> but that code might be from RustBelt as you say, or maybe some
> less relevant code, I am guessing.

Ah, there might be some of the logic for getting the MIR out of rustc, or some 
test cases. But the "core parts" of Miri (the actual UB checking and Abstract 
Machine implementation) don't have anything to do with RefinedRust.

; Ralf