Logic against Ghosts: Comparison of Two Proof Approaches for a List Module

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 functions manipulating lists. During the verification, a more efficient implementation for one function was found and verified. We compare the new approach with the previous effort based on ghost arrays, and discuss the benefits and drawbacks of both techniques.
Complete list of metadatas

https://hal.inria.fr/hal-02100515
Contributor : Allan Blanchard <>
Submitted on : Tuesday, April 16, 2019 - 8:36:22 AM
Last modification on : Thursday, May 9, 2019 - 10:43:22 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue. Logic against Ghosts: Comparison of Two Proof Approaches for a List Module. SAC 2019 - The 34th ACM/SIGAPP Symposium On Applied Computing, Apr 2019, Limassol, Cyprus. ⟨10.1145/3297280.3297495⟩. ⟨hal-02100515⟩

Share

Metrics

Record views

93

Files downloads

68