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

[Roberto Sassu <roberto.sassu@huaweicloud.com>]

On Fri, 2023-07-21 at 18:33 +0200, Roberto Sassu wrote:
> From: Roberto Sassu <roberto.sassu@huawei.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