linux-kernel - Re: [PATCH] coccinelle: api: add kzfree script

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: <a188acce-348b-b106-9180-708c3050ef8d@linux.com>
Date:   Thu, 4 Jun 2020 18:39:41 +0300
From:   Denis Efremov <efremov@...ux.com>
To:     Julia Lawall <julia.lawall@...ia.fr>
Cc:     cocci@...teme.lip6.fr, linux-kernel@...r.kernel.org
Subject: Re: [PATCH] coccinelle: api: add kzfree script

On 6/4/20 5:15 PM, Julia Lawall wrote:
> Did you try ... here but find that some subexpressions of E could be
> modified in between?

Yes, I tried to use "... when != E = E1 when != &E" and results were bad.
Now, I've tried forall and when strict. Here are examples:

// forall added
// Works well, suitable for v2. One additional catch in w1 driver.
@r depends on !patch && !(file in "lib/test_kasan.c") && !(file in "mm/slab_common.c") forall@
expression *E; // pointer. Results are equal as if we use E.
position p;
@@

* memset(E, 0, ...);
  ... when != E // Is it enough to match &E, E = E1?
* kfree(E)@p;

//no forall, when strict
//results are bad, too many false positives
@r depends on !patch && !(file in "lib/test_kasan.c") && !(file in "mm/slab_common.c")@
expression *E;
position p;
@@

* memset(E, 0, ...);
  ... when != E // E is not enough here
      when strict
* kfree(E)@p;

I guess that the difference is that "forall" requires that whole pattern should occur on
every path, "when strict" states that kfree should be called on every path after memset.
This results in missed uses of E in loops and under conditions. How can I state in this
case that E should not occur at all (in all paths) in between memset, kfree even as a
subexpression?

// Doesn't work well
  ... when != E
      when != if (...) { ... E ... }
      when != for(...;...;...) { ... E ... }

Regards,
Denis