linux-kernel - Re: [RFC][PATCH 00/12] integrity: Introduce a digest cache

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] [day] [month] [year] [list]

Message-ID: <5a938ee2f56f9ccf7df82f233fcf9c7ff310b4cb.camel@huaweicloud.com>
Date:   Thu, 03 Aug 2023 18:20:47 +0200
From:   Roberto Sassu <roberto.sassu@...weicloud.com>
To:     zohar@...ux.ibm.com, dmitry.kasatkin@...il.com,
        paul@...l-moore.com, jmorris@...ei.org, serge@...lyn.com
Cc:     linux-kernel@...r.kernel.org, linux-integrity@...r.kernel.org,
        linux-security-module@...r.kernel.org, bpf@...r.kernel.org,
        jarkko@...nel.org, pbrobinson@...il.com, zbyszek@...waw.pl,
        hch@....de, mjg59@...f.ucam.org,
        Roberto Sassu <roberto.sassu@...wei.com>,
        Panu Matilainen <pmatilai@...hat.com>
Subject: Re: [RFC][PATCH 00/12] integrity: Introduce a digest cache

On Fri, 2023-07-21 at 18:33 +0200, Roberto Sassu wrote:
> From: Roberto Sassu <roberto.sassu@...wei.com>

[...]

> The last part I wanted to talk about is about the digest list parsers. This
> was a long debate. In the original proposal, Matthew Garrett and Christoph
> Hellwig said that adding parsers in the kernel is not scalable and not a
> good idea in general. While I do agree with them, I'm also thinking what
> benefits we get if we relax a bit this requirement. If we merge this patch

I tried to mitigate the risk of adding unsafe code to the kernel by
verifying the parsers with a formal verification tool, Frama-C.

The verified code can be accessed here, and contains all the necessary
dependencies (so that the kernel is not involved):

https://github.com/robertosassu/rpm-formal

I added some assertions, to ensure that for any given input, the parser
does not try to reference memory outside the assigned memory area.

I also tried to enforce finite termination by making the number of
loops dependent on the passed data length.

The output I get is the following:

[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  13 functions analyzed (out of 13): 100% coverage.
  In these functions, 232 statements reached (out of 251): 92% coverage.
  ----------------------------------------------------------------------------
  Some errors and warnings have been raised during the analysis:
    by the Eva analyzer:      0 errors    2 warnings
    by the Frama-C kernel:    0 errors    0 warnings
  ----------------------------------------------------------------------------
  0 alarms generated by the analysis.
  ----------------------------------------------------------------------------
  Evaluation of the logical properties reached by the analysis:
    Assertions        5 valid     0 unknown     0 invalid      5 total
    Preconditions    25 valid     0 unknown     0 invalid     25 total
  100% of the logical properties reached have been proven.
  ----------------------------------------------------------------------------

The warnings are:

[eva] validate_tlv.c:353: Warning: 
  this partitioning parameter cannot be evaluated safely on all states

[eva] validate_tlv.c:381: Warning: 
  this partitioning parameter cannot be evaluated safely on all states

Not sure how I can make them go away. Anyway, the assertions are
successful.

I verified the parsers with both deterministic (random but valid) and
non-deterministic (random and possibly invalid) data. For deterministic
data, I also verified that bytes at a specific location have the
expected value.

Due to the increasing complexity, the analysis was not done on
arbitrary lengths and value ranges (it would probably require a
different type of analysis).

Thanks

Roberto