linux-kernel - Re: Litmus test for question from Al Viro

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]

Date:   Sun, 4 Oct 2020 00:16:31 +0900
From:   Akira Yokosawa <akiyks@...il.com>
To:     Alan Stern <stern@...land.harvard.edu>,
        "Paul E. McKenney" <paulmck@...nel.org>
Cc:     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, dlustig@...dia.com,
        joel@...lfernandes.org, viro@...iv.linux.org.uk,
        linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org,
        Akira Yokosawa <akiyks@...il.com>
Subject: Re: Litmus test for question from Al Viro

Hi Alan,

Just a minor nit in the litmus test.

On Sat, 3 Oct 2020 09:22:12 -0400, Alan Stern wrote:
> To expand on my statement about the LKMM's weakness regarding control 
> constructs, here is a litmus test to illustrate the issue.  You might 
> want to add this to one of the archives.
> 
> Alan
> 
> C crypto-control-data
> (*
>  * LB plus crypto-control-data plus data
>  *
>  * Expected result: allowed
>  *
>  * This is an example of OOTA and we would like it to be forbidden.
>  * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
>  * control-dependent on the preceding READ_ONCE.  But the dependencies are
>  * hidden by the form of the conditional control construct, hence the 
>  * name "crypto-control-data".  The memory model doesn't recognize them.
>  *)
> 
> {}
> 
> P0(int *x, int *y)
> {
> 	int r1;
> 
> 	r1 = 1;
> 	if (READ_ONCE(*x) == 0)
> 		r1 = 0;
> 	WRITE_ONCE(*y, r1);
> }
> 
> P1(int *x, int *y)
> {
> 	WRITE_ONCE(*x, READ_ONCE(*y));

Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.

When I changed P1 to

P1(int *x, int *y)
{
	int r1;

	r1 = READ_ONCE(*y);
	WRITE_ONCE(*x, r1);
}

and replaced the WRITE_ONCE() in P0 with smp_store_release(),
I got the result of:

-----
Test crypto-control-data Allowed
States 1
0:r1=0;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (0:r1=1)
Observation crypto-control-data Never 0 3
Time crypto-control-data 0.01
Hash=9b9aebbaf945dad8183d2be0ccb88e11
-----

Restoring the WRITE_ONCE() in P0, I got the result of:

-----
Test crypto-control-data Allowed
States 2
0:r1=0;
0:r1=1;
Ok
Witnesses
Positive: 1 Negative: 4
Condition exists (0:r1=1)
Observation crypto-control-data Sometimes 1 4
Time crypto-control-data 0.01
Hash=843eaa4974cec0efae79ce3cb73a1278
-----

As this is the same as the expected result, I suppose you have missed another
limitation of herd7 + LKMM.

By the way, I think this weakness on control dependency + data dependency
deserves an entry in tools/memory-model/Documentation/litmus-tests.txt.

In the LIMITATIONS section, item #1 mentions some situation where
LKMM may not recognize possible losses of control-dependencies by
compiler optimizations.

What this litmus test demonstrates is a different class of mismatch.

Alan, can you come up with an update in this regard?

        Thanks, Akira

> }
> 
> exists (0:r1=1)
>