[chrony-dev] Analyzing Chrony with Frama-C/Eva

[Andre Maroneze <Andre.OLIVEIRAMARONEZE@xxxxxx>]

Dear Chrony developers,

As part of an effort sponsored by Orolia, 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

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature