Chrony is an implementation of NTP which is C99-compatible, with portable code, and thus a good candidate for an analysis with tools such as Frama-C.
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. This post summarizes some of the findings and links to the full report, in PDF format.
The analysis was performed on Chrony 3.2.
Some parts of the code were disabled via the
configure scripts, namely
IPV6, timestamping and readline. The idea is to minimize the amount of
non-POSIX code, in hopes of improving the likelihood that external functions
will have a specification in Frama-C's stdlib. Reenabling those features
requires only writing additional stubs/specifications.
The entrypoint used for the analysis was the main function in
test/unit/ntp_core.c, with a generalized state for
include possible behaviors from arbitrary command line arguments.
The Eva plug-in was iteratively parametrized to improve coverage and minimize the number of alarms, while maintaining a short execution time. Reported alarms include possible buffer overflows, uninitialized reads, and other undefined behaviors, as listed in the Eva plug-in user manual.
The analysis identified a few issues, but the overall impression was that code quality was high w.r.t. the C standard and the presence of some defensive programming patterns. However, there are still several potential alarms that need to be further investigated to ensure the absence of run-time errors.
The full report is available here: