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
