linux-kernel - Re: [PATCH 0/2] rbtree: Test against a verified oracle

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: <20211022093206.GB12893@lespinasse.org>
Date:   Fri, 22 Oct 2021 02:32:06 -0700
From:   Michel Lespinasse <michel@...pinasse.org>
To:     Mete Polat <metepolat2000@...il.com>
Cc:     Lukas Bulwahn <lukas.bulwahn@...il.com>,
        Shuah Khan <shuah@...nel.org>,
        Michel Lespinasse <michel@...pinasse.org>,
        Andrii Nakryiko <andrii@...nel.org>,
        Alexei Starovoitov <ast@...nel.org>,
        "David S. Miller" <davem@...emloft.net>,
        Paolo Bonzini <pbonzini@...hat.com>,
        Daniel Borkmann <daniel@...earbox.net>,
        "Paul E. McKenney" <paulmck@...nel.org>,
        linux-kernel@...r.kernel.org
Subject: Re: [PATCH 0/2] rbtree: Test against a verified oracle

Hi Mete,

I have two questions regarding the approach:

- Has it been considered to compare the tools/lib/rbtree.c library
  against the oracle, instead of the lib/rbtree.c one, so that the
  test can run fully in userspace ? The two versions closely follow
  each other, is there a worry that results would vary between them ?

- lib/rbtree_test.c has code that validates the rbtree invariants
  (i.e. that all leaf paths have the same black_path_count, etc);
  is that significantly weaker than comparing the rbtree shape
  against the oracle ? My worry here is that, if one were to update
  the rbtree code in ways that preserve the design invariants, but
  result in a different tree shape, they would now have to reflect those
  changes into the oracle, which may be difficult if they are not too
  familiar with haskel ?

  (if validating rbtree invariants makes sense, it might still be
  useful to extend the lib/rbtree_test.c test case generator to cover
  more than random test cases, as you have done in your proposal...)

Thanks,

On Tue, Oct 19, 2021 at 11:13:47AM +0200, Mete Polat wrote:
> Hi,
> 
> This patch series provides a pipeline for testing the kernel Red-Black
> tree implementation against a verified oracle and is based on the work
> which we presented on the LPC [1]. A verified oracle is an equivalent
> algorithm that is proven to be mathematically correct. The testing
> pipeline consists of a kernel module that exposes the core rbtree
> functions to userspace using debugfs, and a testing harness that
> implements two strategies to generate test cases which are then applied
> on the kernel rbtree and the verified rbtree (the oracle). After
> executing an operation on both versions, the harness checks if the
> kernel rbtree is valid by partially comparing it to the verified oracle.
> 
> See the second patch for a description of how to use the harness.
> 
> Some notes:
> 
> The verified rbtree was verified in the proof assistant Isabelle [2] and
> is written in a functional programming language. That's why I also wrote
> the testing harness in the functional programming Haskell.
> 
> I decided to not try to integrate this work into kselftests because
> (1) Haskell (obviously) has another build system
> (2) The tests can run several minutes and would just slow down the
>     execution of all kselftests
> 
> There already is a decent rbtree testing module in the kernel. This work
> tries to address the issue of functional correctness using a more formal
> method and can be seen as an baseline for future (more complex) testing
> against verified oracles.
> 
> Regards,
> 
> Mete
> 
> [1] https://linuxplumbersconf.org/event/11/contributions/1036/
> [2] https://isabelle.in.tum.de/
> 
> Mete Polat (2):
>   rbtree: Expose a test tree to userspace
>   rbtree: add verified oracle with testing harness
> 
>  lib/Kconfig.debug                             |  19 ++
>  lib/Makefile                                  |   1 +
>  lib/test_rbtree_interface.c                   | 161 +++++++++++
>  tools/testing/rbtree_oracle/.gitignore        |   1 +
>  tools/testing/rbtree_oracle/Main.hs           | 128 +++++++++
>  tools/testing/rbtree_oracle/RBT/Kernel.hs     |  64 +++++
>  tools/testing/rbtree_oracle/RBT/Verified.hs   | 253 ++++++++++++++++++
>  tools/testing/rbtree_oracle/RBT_export.thy    |  41 +++
>  tools/testing/rbtree_oracle/Setup.hs          |   2 +
>  tools/testing/rbtree_oracle/Strategy.hs       |  72 +++++
>  .../rbtree_oracle/rbtTestHarness.cabal        |  15 ++
>  11 files changed, 757 insertions(+)
>  create mode 100644 lib/test_rbtree_interface.c
>  create mode 100644 tools/testing/rbtree_oracle/.gitignore
>  create mode 100644 tools/testing/rbtree_oracle/Main.hs
>  create mode 100644 tools/testing/rbtree_oracle/RBT/Kernel.hs
>  create mode 100644 tools/testing/rbtree_oracle/RBT/Verified.hs
>  create mode 100644 tools/testing/rbtree_oracle/RBT_export.thy
>  create mode 100644 tools/testing/rbtree_oracle/Setup.hs
>  create mode 100644 tools/testing/rbtree_oracle/Strategy.hs
>  create mode 100644 tools/testing/rbtree_oracle/rbtTestHarness.cabal
> 
> -- 
> 2.33.1
>