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

From: Roberto Sassu
Date: Thu Aug 03 2023 - 12:21:30 EST


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

[...]

> 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