Abstract

Modern verification projects continue to offer new challenges for formal verification. One of them is the linked list module of Contiki, a popular open-source operating system for the Internet of Things. It has a rich API and uses a particular list representation that make it different from the classical linked list implementations. Being widely used in the OS, the list module is critical for reliability and security. A recent work verified the list module using ghost arrays.

This article reports on a new verification effort for this module. Realized in the Frama-C/Wp tool, the new approach relies on logic lists. A logic list provides a convenient high-level view of the linked list. The specifications of all functions are now proved faster and almost all automatically, only a small number of auxiliary lemmas and a couple of assertions being proved interactively in Coq. The proposed specifications are validated by proving a few client func- tions manipulating lists. During the verification, a more efficient implementation for one function was found and verified. We com- pare the new approach with the previous effort based on ghost arrays, and discuss the benefits and drawbacks of both techniques.

Best Software Development Paper Award

Award

In

Proc. of the 34th ACM/SIGAPP Symposium On Applied Computing, Software Verification and Testing (SAC-SVT 2019).

Limassol, Cyprus, April 2019, pages 2186-2195. ACM. ISBN 978-1-4503-5933-7.

The final publication will be available in SAC 2019, DOI: 10.1145/3297280.3297495.

Paper (Available PDF is the author's final version of the work). It is posted here by permission of ACM for your personal use. Not for redistribution.

Slides.