Analyzing Chrony with Frama-C/Eva

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.

Scope of the analysis

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 argc and argv, to 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:

Report: Frama-C/Eva applied to the Chrony source code: a first analysis (PDF)

Do not hesitate to contact us if you have suggestions, remarks, patches, etc. You can use the Frama-C mailing list or Github’s issues page on open-source-case-studies.