Dear Chrony developers,
As part of an effort sponsored by Orolia <https://www.orolia.com>, researchers from the List, CEA Tech laboratory applied Frama-C/Eva on the Chrony source code, in an attempt to verify the absence of run-time errors.
The main objective of the analysis is to identify possible buffer overflows, uninitialized reads, and other cases of undefined behaviors. The analysis also reports deviations from the C standard and some code portability issues.
The Frama-C blog contains a short post with more details: http://blog.frama-c.com/index.php?post/2018/06/19/Analyzing-Chrony-with-Frama-C/Eva
Overall, the analysis identified a few issues, but the general impression was that code quality was high w.r.t. the C standard and the presence of some defensive programming patterns. Further investigation is necessary to deal with the remaining /potential/ alarms, before we can ensure the absence of run-time errors.
In case you are interested, the full report (in PDF) is available at: https://blog.frama-c.com/public/chrony/report-eva-chrony.pdf
Please don't hesitate to contact us if you have questions or remarks. Best regards, -- André Maroneze Researcher/Engineer CEA/LIST Software Reliability and Security Laboratory
smime.p7s
Description: S/MIME Cryptographic Signature
