Publications

Workshops Conferences Reports Journals

2018

Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov.
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C

Abstract

Internet of Things (IoT) applications are becoming increasingly crit- ical and require rigorous formal verification. In this paper we target Contiki, a widely used open-source OS for IoT, and present a verification case study of one of its most critical modules: that of linked lists. Its API and list representation differ from the classical linked list implementations, and are particularly chal- lenging for deductive verification. The proposed verification technique relies on a parallel view of a list through a companion ghost array. This approach makes it possible to perform most proofs automatically using the Frama-C/WP tool, only a small number of auxiliary lemmas being proved interactively in the Coq proof assistant. We present an elegant segment-based reasoning over the companion ar- ray developed for the proof. Finally, we validate the proposed specification by proving a few functions manipulating lists.

In Proc. of the 10th NASA Formal Methods Symposium (NFM 2018)
Newport News, VA, USA, April 2018, LNCS, vol. XXX, pages XXX-XXX. Springer. ISBN XXX. To appear.
Available PDF is the author's final version of the work. Final publication available at http://link.springer.com. DOI XXX. To appear.

Void

2017

Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov.
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation

Abstract

Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed Conc2Seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs.

In this paper we formalize and sketch the proof of correctness of the program transformation principle behind Conc2Seq, and present an effort towards the full mechanization of both the formalization and proofs with the proof assistant Coq.

In Proc. of the 5th International Workshop on Verification and Program Transformation (VPT 2017)
ETAPS 2017 Workshops, Uppsala, Sweden, April 2017, EPTCS, vol. 253, pages 109-123.
Available PDF is the author's final version of the work. Final publication available at DOI 10.4204/EPTCS.253.9.

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
Concurrent Program Verification by Code Transformation: Correctness

Abstract

Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed Conc2Seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs.

In this paper we formalize and sketch the proof of correctness of the program transformation principle behind Conc2Seq, and present an effort towards the full mechanization of both the formalization and proofs with the proof assistant Coq.

2016

Allan Blanchard.
Aide à la vérification de programmes concurrents par transformation de code et de spécifications

Abstract

Thèse soutenue le 12 décembre 2016.
Jury composé de:

  • Sébastien Limet, Président du jury (Université d'Orléans)
  • Frédéric Loulergue, Directeur de thèse (Northern Arizona University)
  • Catherine Dubois, Rapporteur (ENSIIE)
  • Sylvain Conchon, Rapporteur (Université Paris-Sud)
  • Nikolai Kosmatov, Encadrant (CEA LIST)
  • Stephan Merz, Examinateur (INRIA)
  • Jan-Georg Smaus, Examinateur (Université de Toulouse)
  • Louis Rilling, Examinateur (DGA)
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue.
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs

Abstract

Frama-C is an extensible modular framework for analysis of C programs that offers different analyzers in the form of collaborating plugins. Currently, Frama-C does not support the proof of functional properties of concurrent code.

We present Conc2Seq, a new code transformation based tool realized as a Frama-C plugin and dedicated to the verification of concurrent C programs. Assuming the program under verification respects an interleaving semantics, Conc2Seq transforms the original concurrent C program into a sequential one in which concurrency is simulated by interleavings. User specifications are automatically reintegrated into the new code without manual intervention. The goal of the proposed code transformation technique is to allow the user to reason about a concurrent program through the interleaving semantics using existing Frama-C analyzers.

In Proc. of the 16th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2016)
Raleigh, NC, USA, October 2016, pages 67-72. IEEE. ISBN 978-1-5090-3848-0.
Available PDF is the author's final version of the work. Final publication available at http://link.springer.com. DOI 10.1007/978-3-319-47166-2_32.

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
A CHR-Based Solver for Weak Memory Behaviors

Abstract

With the wide expansion of multiprocessor architectures, the analysis and reasoning for programs under weak memory models has become an important concern. This work presents an original constraint solver for detecting program behaviors respecting a particular memory model. It is implemented in Prolog using CHR (Constraint Handling Rules). The CHR formalism provides a convenient generic solution for specifying memory models, that benefits from the existing optimized implementations of CHR and can be easily extended to new models. We briefly present the solver design, illustrate the encoding of memory model constraints in CHR and discuss the benefits and limitations of the proposal.

In Proc. of the 7th International Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA 2016)
ISSTA 2016 Workshops, Saarbruecken, Germany, July 2016, pages 15-22.
CEUR Workshop Proceedings, vol. 1639.

Void

2015

Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue.
A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C

Abstract

Cloud hypervisors are critical software whose formal verification can increase our confidence in the reliability and security of the cloud. This work presents a case study on formal verification of the virtual memory system of the cloud hypervisor Anaxagoros, a microkernel designed for resource isolation and protection. The code under verification is specified and proven in the Frama-C software verification framework, mostly using automatic theorem proving. The remaining properties are interactively proven with the Coq proof assistant. We describe in detail selected aspects of the case study, including parallel execution and counting references to pages, and discuss some lessons learned, benefits and limitations of our approach.

Slides Publi

In Proc. of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015), Oslo, Norway, June 2015, pages 15-30.
LNCS 9128. Springer. ISBN 978-3-319-19457-8.
Available PDF is the author's final version of the work. Final publication available at http://link.springer.com. DOI 10.1007/978-3-319-19458-5_2

Void