Publications

Conferences Journals Reports Tutorials Workshops

2018

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models

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 MMFilter, an original constraint solver for generating 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. It benefits from the existing optimized implementations of CHR and can be easily extended to new models. We present MMFilter design, illustrate the encoding of memory model constraints in CHR and discuss the benefits and limitations of the proposed technique.

In Computer Languages, Systems and Structures, vol. 53, pages 121-142. Elsevier.
Available PDF is the author's final version of the work. Final publication available at https://www.sciencedirect.com. DOI: 10.1016/j.cl.2018.03.002.

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
A Lesson on Verification of IoT Software with Frama-C

Abstract

This paper is a tutorial introduction to Frama-C, a framework for analysis and verification of C programs. We present value analysis, deductive verification and runtime verification of software using Frama-C and in particular its EVA, WP, and E-ACSL plugins. These techniques are illustrated on examples coming from real-life verification case studies for different modules of Contiki, a lightweight operating system for the Internet of Things.

In Proc. of the 12th International Conference on High Performance Computing & Simulation (HPCS 2018)
Orléans, France, July 2018, pages xxx-xxx. IEEE. ISBN xxx. To appear.
Available PDF is the author's final version of the work. Final publication available at http://ieeexplore.ieee.org/. DOI: 10.1007/xxx. To appear.

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. 10811, pages 37-53. Springer. ISBN 978-3-319-77934-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-77935-5_3.

Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov.
Ghosts for Lists: from Axiomatic to Executable Specifications

Abstract

Internet of Things (IoT) applications are becoming increasingly critical and require formal verification. Our recent work presented formal verification of the linked list module of Contiki, an OS for IoT. It relies on a parallel view of a linked list via a companion ghost array and uses an inductive predicate to link both views. In this work, a few interactively proved lemmas allow for the automatic verification of the list functions specifications, expressed in the ACSL specification language and proved with the Frama-C/WP tool.

In a broader verification context, especially as long as the whole system is not yet formally verified, it would be very useful to use runtime verification, in particular, to test client modules that use the list module. It is not possible with the current specifications, which include an inductive predicate and axiomatically defined functions. In this early-idea paper we show how to define a provably equivalent non-inductive predicate and a provably equivalent non-axiomatic function that belong to the executable subset E-ACSL of ACSL and can be transformed into executable C code. Finally, we propose an extension of Frama-C to handle both axiomatic specifications for deductive verification and executable specifications for runtime verification.

In Proc. of the 12th International Conference on Tests & Proofs (TAP 2018)
Toulouse, France, June 2018, pages 177-184. LNCS 10889. Springer. ISBN 978-3-319-92993-4.
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-92994-1_11.

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