linux-kernel - Re: [RFC] tools/memory-model: Rule out OOTA

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: <9df85484-9a31-4682-a053-f3aaf01c0bbb@huaweicloud.com>
Date: Tue, 7 Jan 2025 16:46:35 +0100
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: paulmck@...nel.org
Cc: stern@...land.harvard.edu, parri.andrea@...il.com, will@...nel.org,
 peterz@...radead.org, boqun.feng@...il.com, npiggin@...il.com,
 dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr,
 akiyks@...il.com, dlustig@...dia.com, joel@...lfernandes.org,
 urezki@...il.com, quic_neeraju@...cinc.com, frederic@...nel.org,
 linux-kernel@...r.kernel.org, lkmm@...ts.linux.dev,
 hernan.poncedeleon@...weicloud.com
Subject: Re: [RFC] tools/memory-model: Rule out OOTA



Am 1/6/2025 um 10:40 PM schrieb Jonas Oberhauser:>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
> ---
>   tools/memory-model/linux-kernel.cat | 6 +++++-
>   1 file changed, 5 insertions(+), 1 deletion(-)
> 
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index d7e7bf13c831..180cab56729e 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -71,6 +71,10 @@ let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu |
>   		Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) |
>   	(po ; [Release]) | ([Acquire] ; po)
>   
> +let w_barrier = po? ; [F | Marked] ; po?
> +let rmb-plain = [R4rmb] ; po ; [Rmb] ; (po \ (po ; [W] ; (po-loc \ w_barrier))) ; [R4rmb & Plain]
> +let plain-wmb = [W & Plain] ; (po \ ((po-loc \ w_barrier) ; po ; [W] ; po)) ; [Wmb] ; po ; [W]
> +
>   (**********************************)
>   (* Fundamental coherence ordering *)
>   (**********************************)
> @@ -90,7 +94,7 @@ empty rmw & (fre ; coe) as atomic
>   let dep = addr | data
>   let rwdep = (dep | ctrl) ; [W]
>   let overwrite = co | fr
> -let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
> +let to-w = ((addr | rmb-plain)? ; rwdep ; plain-wmb?) | (overwrite & int) | addr ; [Plain] ; wmb
>   let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi)
>   let ppo = to-r | to-w | (fence & int) | (po-unlock-lock-po & int)
>   

I will also try to give an intuitive :) :( :) reasoning for why this 
patch rules out OOTA.

If we look at an dep ; rfe cycle

   dep ; rfe ; dep ; rfe ; ...


then because of the absence of data races, each rfe is more or less an

   w-post-bounded ; rfe ; r-pre-bounded

edge.

If we rotate the circle around we turn

   dep ; w-post-bounded ; rfe ; r-pre-bounded ; dep ; w-post-bounded ; 
rfe ; r-pre-bounded ; ...

into

    rfe ; (r-pre-bounded ; dep ; w-post-bounded) ; rfe ; (r-pre-bounded 
; dep ; w-post-bounded) ; rfe ; (r-pre-bounded ; ...


and ideally, each of these (w-pre-bounded ; dep ; r-post-bounded) would 
imply happens-before, since then the cycle would be.
    rfe ; hb+; rfe; hb+ ; ...
which is acyclic.

However, we do not get hb+ in general, in particular if the bounding is 
due to rmb/wmb. For all other cases, it is relatively easy to see that 
we get hb+, e.g., if the bound is due to an smp_mb().

Luckily, in our specific case, we can get hb+ evenfor cases where 
rmb/wmb bound these accesses, because these accesses related by the dep 
edges are known to be reading/read-from externally.
Such an external interaction would be impossible if there were another 
store to the same location between such an access and the next 
w_barrier: because of the absence of data races and the lack of 
w_barriers that would allow synchronization with the outside world, the 
external event could not "occur between" the access and such a store.

As a result, all pre-bounds caused by a rmb must have the form

[R4rmb] ; po ; [Rmb] ; (po \ (po ; [W] ; (po-loc \ w_barrier))) ; [R4rmb 
& Plain]

and similar for post-bounds caused by wmb, which means the corresponding

    r-pre-bounded ; dep ; w-post-bounded

edges must be

    rmb-plain ; dep ; plain-wmb

which is in ppo and thus also hb.

Hope that helps clarify the idea...

   jonas