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: <CAFJgqgTeq0Zer8b1Dk0D2Cvo3t5BUTqxh_7OF7eCkLtjmm8Mcg@mail.gmail.com>
Date: Thu, 27 Feb 2025 08:11:59 -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 2:39 PM Ralf Jung <post@...fj.de> wrote:
> > 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.

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.

Best, VJ.