linux-kernel - Re: Some observations (results) on BPF acquire and release

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 for Android: free password hash cracker in your pocket

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

Message-ID: <mb61pr085bt0g.fsf@kernel.org>
Date: Thu, 24 Oct 2024 12:11:11 +0000
From: Puranjay Mohan <puranjay@...nel.org>
To: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>, Andrea Parri
 <parri.andrea@...il.com>, paulmck@...nel.org
Cc: bpf@...r.kernel.org, lkmm@...ts.linux.dev, linux-kernel@...r.kernel.org
Subject: Re: Some observations (results) on BPF acquire and release

Jonas Oberhauser <jonas.oberhauser@...weicloud.com> writes:

> Am 10/23/2024 um 7:47 PM schrieb Andrea Parri:
>> Hi Puranjay and Paul,
>> 
>> These remarks show that the proposed BPF formalization of acquire and
>> release somehow, but substantially, diverged from the corresponding
>> LKMM formalization.  My guess is that the divergences mentioned above
>> were not (fully) intentional, or I'm wondering -- why not follow the
>> latter (the LKMM's) more closely? -  This is probably the first question
>> I would need to clarify before trying/suggesting modifications to the
>> present formalizations.  ;-)  Thoughts?
>> 
>
> I'm also curious why the formalization (not just in the semantics but 
> also how it is structured) is so completely different from LKMM's.

While initially writing the cat formalization for BPF, I started with
LKMM but because BPF memory model is an instruction level memory model
and much simpler than LKMM, I wrote it from scratch. But I converted all
LKMM litmus tests to BPF and made sure that the cat model is complaint.

> At first glance there are also many semantic differences, e.g., it seems 
> coe is much weaker in eBPF and the last axiom also seems a bit like a 
> tack-on that doesn't "play well" with the previous axioms.

Yes, the last axion is a tack-on that I added to make acquire/release
work with other atomics just before the presentation at LPC. The
acquire/release part is still under development and not perfect.

If what you are saying about coe is true then it is a bug and I will try
to fix it. 

> It would make sense to me to start with the framework of LKMM and maybe 
> weaken it from there if it is really necessary. But maybe I don't know 
> enough about how eBPF atomics are intended to work...

The cat formalization for BPF is currently experimental and it would be
great if people can find bugs and contribute to it. It would be great if
people who worked on the LKMM's cat file could help building BPF's cat
file too. 

Thanks,
Puranjay

Download attachment "signature.asc" of type "application/pgp-signature" (256 bytes)